OverviewCakeML:ac281b612346d6f60294cff5550d2edf14434b08
Fix more confusion caused by two script files with same name
#884 (let-lift)
Merging into:eb790298e00c580a9e04859097bb496681cb60ba
Merge pull request #889 from CakeML/consts
HOL:55691be292491aef452ee5e7c56e67b02601f669
Holmake: fix mlton build
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux
Claimed job
Reusing HOL
Starting developers
Finished developers 5s 89MB
Starting developers/bin
Finished developers/bin 12s 1GB
Starting semantics/ffi
Finished semantics/ffi 18s 293MB
Starting semantics
Finished semantics 4m55s 1GB
Starting semantics/proofs
Finished semantics/proofs 13m23s 1GB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 50s 530MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 16m21s 2GB
Starting basis/pure
Finished basis/pure 1m09s 1GB
Starting translator
Finished translator 3m41s 2GB
Starting compiler/parsing
Finished compiler/parsing 1m31s 6GB
Starting characteristic
Finished characteristic 6m59s 3GB
Starting translator/monadic
Finished translator/monadic 2m04s 1GB
Starting basis
Finished basis 51m42s 26GB
Starting compiler/inference
Finished compiler/inference 1m30s 2GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 1m42s 2GB
Starting compiler/backend/gc
Finished compiler/backend/gc 4m33s 2GB
Starting compiler/backend
Finished compiler/backend 6m30s 4GB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 30s 1GB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 30s 1GB
Starting compiler/encoders/arm7
Finished compiler/encoders/arm7 54s 1GB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 17s 1GB
Starting compiler/encoders/arm8_asl
Finished compiler/encoders/arm8_asl 2m37s 1GB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 22s 1GB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 20s 1GB
Starting compiler/encoders/ag32
Finished compiler/encoders/ag32 22s 1GB
Starting compiler/backend/x64
Finished compiler/backend/x64 23s 1GB
Starting compiler/backend/arm7
Finished compiler/backend/arm7 23s 1GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 22s 1GB
Starting compiler/backend/mips
Finished compiler/backend/mips 24s 1GB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 23s 1GB
Starting compiler/backend/ag32
Finished compiler/backend/ag32 1m23s 1GB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 2m39s 1GB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 2m40s 1GB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 24m45s 4GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 3m21s 1GB
Starting compiler/backend/proofs
Finished compiler/backend/proofs 55m00s 16GB
Starting compiler/backend/serialiser
Finished compiler/backend/serialiser 1m41s 2GB
Starting compiler/encoders/x64/proofs
Finished compiler/encoders/x64/proofs 9m26s 6GB
Starting compiler/encoders/arm7/proofs
Finished compiler/encoders/arm7/proofs 12m49s 6GB
Starting compiler/encoders/arm8/proofs
Finished compiler/encoders/arm8/proofs 6m39s 3GB
Starting compiler/encoders/arm8_asl/proofs
Finished compiler/encoders/arm8_asl/proofs 14m29s 3GB
Starting compiler/encoders/mips/proofs
Finished compiler/encoders/mips/proofs 9m48s 6GB
Starting compiler/encoders/riscv/proofs
Finished compiler/encoders/riscv/proofs 8m29s 3GB
Starting compiler/encoders/ag32/proofs
Finished compiler/encoders/ag32/proofs 2m23s 1GB
Starting compiler/backend/x64/proofs
Finished compiler/backend/x64/proofs 28s 2GB
Starting compiler/backend/arm7/proofs
Finished compiler/backend/arm7/proofs 28s 1GB
Starting compiler/backend/arm8/proofs
Finished compiler/backend/arm8/proofs 28s 2GB
Starting compiler/backend/arm8_asl
Finished compiler/backend/arm8_asl 22s 1GB
Starting compiler/backend/mips/proofs
Finished compiler/backend/mips/proofs 28s 1GB
Starting compiler/backend/riscv/proofs
Finished compiler/backend/riscv/proofs 30s 2GB
Starting compiler/backend/ag32/proofs
Finished compiler/backend/ag32/proofs 12m41s 3GB
Starting compiler/proofs
Finished compiler/proofs 2m11s 6GB
Starting candle/set-theory
Finished candle/set-theory 35s 1GB
Starting candle/syntax-lib
Finished candle/syntax-lib 13s 937MB
Starting candle/standard/syntax
Finished candle/standard/syntax 2m02s 1GB
Starting candle/standard/semantics
Finished candle/standard/semantics 1m49s 1GB
Starting candle/standard/monadic
Finished candle/standard/monadic 1m54s 1GB
Starting candle/standard/ml_kernel
Finished candle/standard/ml_kernel 6m10s 4GB
Starting candle/overloading/syntax
Finished candle/overloading/syntax 3m08s 1GB
Starting candle/overloading/semantics
Finished candle/overloading/semantics 10m41s 3GB
Starting candle/overloading/monadic
Finished candle/overloading/monadic 2m26s 2GB
Starting candle/overloading/ml_kernel
Finished candle/overloading/ml_kernel 7m13s 5GB
Starting candle/overloading/ml_checker
Finished candle/overloading/ml_checker 2m23s 5GB
Starting candle/prover
FAILED: candle/prover
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/ml_kernel/lisp[0m
Scanning [1m$(CAKEMLDIR)/candle/syntax-lib[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/syntax[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/monadic[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/ml_kernel[0m
Scanning [1m$(CAKEMLDIR)/candle/set-theory[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/semantics[0m
Scanned 36 directories
Starting work on README.md
Starting work on ast_extrasTheory
README.md (0s) OK
ast_extrasTheory (11s) OK
Starting work on permsTheory
permsTheory (83s) OK
Starting work on candle_kernel_valsTheory
candle_kernel_valsTheory (96s) OK
Starting work on candle_kernel_permsTheory
Starting work on candle_prover_invTheory
candle_kernel_permsTheory (17s)FAIL<1>
Run out of store - interrupting threads
Failed to recover - exiting
candle_prover_invTheory (21s)MKILLED