OverviewCakeML:348a74050804214128ce62f0274f4443cc6730dd
Remove exhProps
HOL:1804892e96b43f86eb0367ed958278fc00dfbdf4
Use polyscripter on LLIST_BISIMULATION and LLIST_TAKE_EQ
Machine:cakeml1795 4.4.0-98-generic x86_64 GNU/Linux
Claimed job
Building HOL
Starting developers/bin
Finished developers/bin 7s 143MB
Starting semantics/ffi
Finished semantics/ffi 57s 280MB
Starting semantics
Finished semantics 2m21s 787MB
Starting semantics/proofs
Finished semantics/proofs 5m08s 911MB
Starting basis/pure
Finished basis/pure 5m41s 690MB
Starting translator
Finished translator 2m47s 936MB
Starting compiler/parsing
Finished compiler/parsing 2m17s 2GB
Starting characteristic
Finished characteristic 4m21s 1GB
Starting translator/monadic
Finished translator/monadic 2m33s 1GB
Starting basis
Finished basis 26m30s 2GB
Starting compiler/inference
Finished compiler/inference 2m48s 2GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 53s 1GB
Starting compiler/backend/gc
Finished compiler/backend/gc 14m34s 3GB
Starting compiler/backend
Finished compiler/backend 3s 16MB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 0s 11MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 1m24s 575MB
Starting compiler/encoders/arm6
Finished compiler/encoders/arm6 3m00s 1GB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 42s 398MB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 1m33s 767MB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 1m33s 489MB
Starting compiler/backend/x64
Finished compiler/backend/x64 29s 963MB
Starting compiler/backend/arm6
Finished compiler/backend/arm6 34s 1GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 33s 991MB
Starting compiler/backend/mips
Finished compiler/backend/mips 28s 897MB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 28s 774MB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 4m03s 763MB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 4m47s 1GB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 14m15s 2GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 1m24s 406MB
Starting compiler/backend/proofs
Finished compiler/backend/proofs 54m27s 3GB
Starting compiler/encoders/x64/proofs
Finished compiler/encoders/x64/proofs 11m37s 2GB
Starting compiler/encoders/arm6/proofs
Finished compiler/encoders/arm6/proofs 12m06s 2GB
Starting compiler/encoders/arm8/proofs
Finished compiler/encoders/arm8/proofs 8m21s 1GB
Starting compiler/encoders/mips/proofs
Finished compiler/encoders/mips/proofs 11m40s 1GB
Starting compiler/encoders/riscv/proofs
Finished compiler/encoders/riscv/proofs 12m29s 918MB
Starting compiler/backend/x64/proofs
Finished compiler/backend/x64/proofs 32s 1GB
Starting compiler/backend/arm6/proofs
Finished compiler/backend/arm6/proofs 36s 857MB
Starting compiler/backend/arm8/proofs
Finished compiler/backend/arm8/proofs 33s 1GB
Starting compiler/backend/mips/proofs
Finished compiler/backend/mips/proofs 35s 1GB
Starting compiler/backend/riscv/proofs
Finished compiler/backend/riscv/proofs 31s 1GB
Starting compiler/proofs
Finished compiler/proofs 2m21s 2GB
Starting candle/set-theory
Finished candle/set-theory 54s 568MB
Starting candle/syntax-lib
Finished candle/syntax-lib 16s 560MB
Starting candle/standard/syntax
Finished candle/standard/syntax 2m41s 1GB
Starting candle/standard/semantics
Finished candle/standard/semantics 2m13s 894MB
Starting candle/standard/monadic
Finished candle/standard/monadic 2m20s 928MB
Starting candle/standard/ml_kernel
Finished candle/standard/ml_kernel 5m50s 2GB
Starting candle/standard/opentheory
Finished candle/standard/opentheory 24s 635MB
Starting characteristic/examples
Finished characteristic/examples 2m35s 1GB
Starting tutorial/solutions
Finished tutorial/solutions 20m25s 8GB
Starting translator/monadic/examples
Finished translator/monadic/examples 2m51s 2GB
Starting examples
Finished examples 7m51s 4GB
Starting examples/compilation
Finished examples/compilation 2h50m56s 12GB
Starting examples/compilation/proofs
Finished examples/compilation/proofs 3m23s 3GB
Starting compiler/benchmarks
Finished compiler/benchmarks 0s 4MB
Starting translator/okasaki-examples
Finished translator/okasaki-examples 6m27s 1GB
Starting translator/other-examples
Finished translator/other-examples 6m33s 997MB
Starting compiler/parsing/tests
Finished compiler/parsing/tests 39s 333MB
Starting compiler/inference/tests
Finished compiler/inference/tests 6m05s 4GB
Starting compiler/bootstrap/translation
FAILED: compiler/bootstrap/translation
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/l3-machine-code/common]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/l3-machine-code/common]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/l3-machine-code/lib]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/l3-machine-code/lib[1mWorking in $(HOLDIR)/examples/l3-machine-code/lib[0m
]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/l3-machine-code/arm/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/l3-machine-code/arm8/model]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/l3-machine-code/arm8/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm8/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/l3-machine-code/mips/model]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/l3-machine-code/mips/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/mips/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/l3-machine-code/riscv/model]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/l3-machine-code/riscv/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/l3-machine-code/x64/model]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/l3-machine-code/x64/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/x64/model[0m
]0;Holmake: .]0;Holmake: ../../../basis]0;Holmake: ../../../basis/pure]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../misc]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/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: ../../../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: ../../../basis/pure]0;Holmake: ../../../basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ../../../basis]0;Holmake: ../../../characteristic]0;Holmake: ../../../compiler/parsing]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: ../../../compiler/parsing]0;Holmake: ../../../compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ../../../characteristic]0;Holmake: ../../../translator]0;Holmake: ../../../semantics/proofs]0;Holmake: ../../../semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ../../../translator]0;Holmake: ../../../translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ../../../characteristic]0;Holmake: ../../../characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ../../../basis]0;Holmake: ../../../translator/monadic]0;Holmake: ../../../translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ../../../basis]0;Holmake: ../../../basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: .]0;Holmake: ../..]0;Holmake: ../../backend]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/machine-code/multiword]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: ../../backend]0;Holmake: ../../backend/reg_alloc]0;Holmake: ../../../unverified/reg_alloc]0;Holmake: ../../../unverified/reg_alloc[1mWorking in $(CAKEMLDIR)/unverified/reg_alloc[0m
]0;Holmake: ../../backend/reg_alloc]0;Holmake: ../../backend/reg_alloc[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc[0m
]0;Holmake: ../../backend]0;Holmake: ../../encoders/asm]0;Holmake: ../../encoders/asm[1mWorking in $(CAKEMLDIR)/compiler/encoders/asm[0m
]0;Holmake: ../../backend]0;Holmake: ../../backend[1mWorking in $(CAKEMLDIR)/compiler/backend[0m
]0;Holmake: ../..]0;Holmake: ../../backend/arm6]0;Holmake: ../../encoders/arm6]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/l3-machine-code/arm/step]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/l3-machine-code]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/machine-code/decompiler]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/machine-code/decompiler[1mWorking in $(HOLDIR)/examples/machine-code/decompiler[0m
]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/l3-machine-code]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/l3-machine-code[1mWorking in $(HOLDIR)/examples/l3-machine-code[0m
]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/l3-machine-code/arm/step]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/l3-machine-code/arm/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/step[0m
]0;Holmake: ../../encoders/arm6]0;Holmake: ../../encoders/arm6[1mWorking in $(CAKEMLDIR)/compiler/encoders/arm6[0m
]0;Holmake: ../../backend/arm6]0;Holmake: ../../backend/arm6[1mWorking in $(CAKEMLDIR)/compiler/backend/arm6[0m
]0;Holmake: ../..]0;Holmake: ../../backend/arm8]0;Holmake: ../../encoders/arm8]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/l3-machine-code/arm8/step]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/l3-machine-code/arm8/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm8/step[0m
]0;Holmake: ../../encoders/arm8]0;Holmake: ../../encoders/arm8[1mWorking in $(CAKEMLDIR)/compiler/encoders/arm8[0m
]0;Holmake: ../../backend/arm8]0;Holmake: ../../backend/arm8[1mWorking in $(CAKEMLDIR)/compiler/backend/arm8[0m
]0;Holmake: ../..]0;Holmake: ../../backend/mips]0;Holmake: ../../encoders/mips]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/l3-machine-code/mips/step]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/l3-machine-code/mips/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/mips/step[0m
]0;Holmake: ../../encoders/mips]0;Holmake: ../../encoders/mips[1mWorking in $(CAKEMLDIR)/compiler/encoders/mips[0m
]0;Holmake: ../../backend/mips]0;Holmake: ../../backend/mips[1mWorking in $(CAKEMLDIR)/compiler/backend/mips[0m
]0;Holmake: ../..]0;Holmake: ../../backend/riscv]0;Holmake: ../../encoders/riscv]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/l3-machine-code/riscv/step]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/l3-machine-code/riscv/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/step[0m
]0;Holmake: ../../encoders/riscv]0;Holmake: ../../encoders/riscv[1mWorking in $(CAKEMLDIR)/compiler/encoders/riscv[0m
]0;Holmake: ../../backend/riscv]0;Holmake: ../../backend/riscv[1mWorking in $(CAKEMLDIR)/compiler/backend/riscv[0m
]0;Holmake: ../..]0;Holmake: ../../backend/x64]0;Holmake: ../../encoders/x64]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/l3-machine-code/x64/step]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/l3-machine-code/x64/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/x64/step[0m
]0;Holmake: ../../encoders/x64]0;Holmake: ../../encoders/x64[1mWorking in $(CAKEMLDIR)/compiler/encoders/x64[0m
]0;Holmake: ../../backend/x64]0;Holmake: ../../backend/x64[1mWorking in $(CAKEMLDIR)/compiler/backend/x64[0m
]0;Holmake: ../..]0;Holmake: ../../inference]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/unification/triangular/first-order]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/unification/triangular]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/unification/triangular[1mWorking in $(HOLDIR)/examples/unification/triangular[0m
]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/unification/triangular/first-order]0;Holmake: /scratch/cakeml/regression/HOL-1804892e96b43f86eb0367ed958278fc00dfbdf4/examples/unification/triangular/first-order[1mWorking in $(HOLDIR)/examples/unification/triangular/first-order[0m
]0;Holmake: ../../inference]0;Holmake: ../../inference[1mWorking in $(CAKEMLDIR)/compiler/inference[0m
]0;Holmake: ../..]0;Holmake: ../..[1mWorking in $(CAKEMLDIR)/compiler[0m
]0;Holmake: .]0;Holmake: ../../backend/reg_alloc/proofs]0;Holmake: ../../backend/reg_alloc/proofs[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
]0;Holmake: .]0;Holmake: ../../inference/proofs]0;Holmake: ../../inference/proofs[1mWorking in $(CAKEMLDIR)/compiler/inference/proofs[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/bootstrap/translation[0m
Starting work on heap
heap OK
Starting work on to_dataProgTheory
to_dataProgTheory OK
Starting work on lexerProgTheory
lexerProgTheory OK
Starting work on parserProgTheory
parserProgTheory OK
Starting work on reg_allocProgTheory
reg_allocProgTheory OK
Starting work on inferProgTheory
inferProgTheory OK
Starting work on explorerProgTheory
explorerProgTheory OK
Starting work on sexp_parserProgTheory
sexp_parserProgTheory OK
Starting work on to_word32ProgTheory
Starting work on to_word64ProgTheory
to_word64ProgTheory OK
Starting work on to_target64ProgTheory
to_word32ProgTheory OK
Starting work on to_target32ProgTheory
to_target64ProgTheory OK
Starting work on x64ProgTheory
to_target32ProgTheory OK
Starting work on arm6ProgTheory
x64ProgTheory OK
Starting work on arm8ProgTheory
arm6ProgTheory OK
Starting work on compiler32ProgTheory
arm8ProgTheory OK
Starting work on riscvProgTheory
riscvProgTheory OK
Starting work on mipsProgTheory
mipsProgTheory OK
Starting work on compiler64ProgTheory
compiler32ProgTheory FAILED! <Signal 9>
Translating compiler_find_num
Saved theorem _____ "nsLookup_auto_env_60"
Saved theorem _____ "compiler_find_num_v_thm"
Translating compiler_get_err_str
Saved theorem _____ "nsLookup_auto_env_61"
Saved theorem _____ "compiler_get_err_str_v_thm"
Translating compiler_parse_num_list
Saved theorem _____ "nsLookup_auto_env_62"
Saved theorem _____ "compiler_parse_num_list_v_thm"
Translating compiler_comma_tokens
compiler64ProgTheory M-KILLED