Overview

Job 422

CakeML: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