Overview

Job 563

CakeML:24050da03e4c1412a0aa8207562fc97f06aff0b9
  Merge branch 'master' into flat-elim-cleanup
#553 (flat-elim-cleanup)
Merging into:8ee5d433f5e6a93e9a41ea5e46b961c65130c2ef
  Merge pull request #551 from CakeML/translator-alist-tree
HOL:57ef4df497757f622a7fe2bfeda16116585da6d4
  Update experimental kernel for world free of Globals.priming
Machine:demi

 Claimed job
 Building HOL
 Starting developers/bin
 Finished developers/bin                                           6s 920MB
 Starting semantics/ffi
 Finished semantics/ffi                                           56s 763MB
 Starting semantics
 Finished semantics                                             1m59s 966MB
 Starting semantics/proofs
 Finished semantics/proofs                                      3m56s   1GB
 Starting basis/pure
 Finished basis/pure                                            5m03s 639MB
 Starting translator
 Finished translator                                            4m13s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                      1m43s   2GB
 Starting characteristic
 Finished characteristic                                        3m34s   2GB
 Starting translator/monadic
 Finished translator/monadic                                    2m01s   1GB
 Starting basis
 Finished basis                                                21m52s   2GB
 Starting compiler/inference
 Finished compiler/inference                                    2m18s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                            1m03s 937MB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                  10m04s   1GB
 Starting compiler/backend
 Finished compiler/backend                                         3s  47MB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                    1s  23MB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                 1m15s 628MB
 Starting compiler/encoders/arm6
 Finished compiler/encoders/arm6                                2m35s   1GB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                  37s 464MB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                1m27s 842MB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                               1m27s 975MB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    25s   1GB
 Starting compiler/backend/arm6
 Finished compiler/backend/arm6                                   27s   1GB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   25s   1GB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   24s   1GB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  26s   1GB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                               9m24s 861MB
 Starting compiler/inference/proofs
 Finished compiler/inference/proofs                             3m55s   1GB
 Starting compiler/backend/semantics
 Finished compiler/backend/semantics                           11m52s   2GB
 Starting compiler/backend/reg_alloc/proofs
 Finished compiler/backend/reg_alloc/proofs                     3m45s 566MB
 Starting compiler/backend/proofs
 Finished compiler/backend/proofs                              57m49s   3GB
 Starting compiler/encoders/x64/proofs
 Finished compiler/encoders/x64/proofs                         10m17s   4GB
 Starting compiler/encoders/arm6/proofs
 Finished compiler/encoders/arm6/proofs                        10m09s   2GB
 Starting compiler/encoders/arm8/proofs
 Finished compiler/encoders/arm8/proofs                         7m18s   1GB
 Starting compiler/encoders/mips/proofs
 Finished compiler/encoders/mips/proofs                         9m44s   3GB
 Starting compiler/encoders/riscv/proofs
 FAILED: compiler/encoders/riscv/proofs
]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/common]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/riscv/prog]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/riscv/step]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/machine-code/decompiler]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/machine-code/decompiler[1mWorking in $(HOLDIR)/examples/machine-code/decompiler[0m
]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code[1mWorking in $(HOLDIR)/examples/l3-machine-code[0m
]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/riscv/step]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/riscv/model]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/lib]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/lib[1mWorking in $(HOLDIR)/examples/l3-machine-code/lib[0m
]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/riscv/model]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/riscv/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model[0m
]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/riscv/step]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/riscv/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/step[0m
]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/riscv/prog]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/riscv/prog[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/prog[0m
Starting work on riscv-step-heap
riscv-step-heap                                                                                                                                                                                                                                                                        OK
Starting work on riscv_progTheory
riscv_progTheory                                                                                                                                                                                                                                                                       OK
]0;Holmake: .]0;Holmake: ../../asm]0;Holmake: ../../../../misc]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ../../../../misc]0;Holmake: ../../../../developers]0;Holmake: ../../../../developers[1mWorking in ../../../../developers[0m
]0;Holmake: ../../../../misc]0;Holmake: ../../../../misc/lem_lib_stub]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/formal-languages/context-free]0;Holmake: ~/cakeml/regression-worker/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ../../../../misc/lem_lib_stub]0;Holmake: ../../../../misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ../../../../misc]0;Holmake: ../../../../misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ../../asm]0;Holmake: ../../../../semantics]0;Holmake: ../../../../semantics/ffi]0;Holmake: ../../../../semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ../../../../semantics]0;Holmake: ../../../../semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ../../asm]0;Holmake: ../../asm[1mWorking in $(CAKEMLDIR)/compiler/encoders/asm[0m
]0;Holmake: .]0;Holmake: ..]0;Holmake: ..[1mWorking in $(CAKEMLDIR)/compiler/encoders/riscv[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/encoders/riscv/proofs[0m
Starting work on riscv_targetProofTheory
riscv_targetProofTheory                                                                                                                                                                                                                                                       FAILED! <1>
 error in quse /usr/local/google/home/ramanakumar/cakeml/regression-worker/cakeml-563/compiler/encoders/riscv/proofs/riscv_targetProofScript.sml : Fail "Static Errors"
 error in load riscv_targetProofScript : Fail "Static Errors"
 /usr/local/google/home/ramanakumar/cakeml/regression-worker/cakeml-563/compiler/encoders/riscv/proofs/riscv_targetProofScript.sml:188: error: Value or constructor (priming) has not been declared in structure Globals
 Found near
   Lib.with_flag (Globals.priming, ... ...)
   (Term.variant (List.concat (... ... l))) ms
 Uncaught exception: Fail "Static Errors"