Job 1633

CakeML:229c835e825726f411c2e6587b7c96a17af936f7
  Merge pull request #841 from CakeML/eval [Nov 11 21:14:45]
HOL:983ad16de2900b7594b122057fffd04bd606b23c
  Remove some unused or redundant theorems from algebra/lib/helperNum [Nov 11 06:42:10]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Nov 12 10:23:52 Claimed job
Nov 12 10:23:53 Reusing HOL
Nov 12 10:24:30 Starting developers
Nov 12 10:24:35 Finished developers                                               4s  91MB
Nov 12 10:24:35 Starting developers/bin
Nov 12 10:24:42 Finished developers/bin                                           6s   1GB
Nov 12 10:24:42 Starting semantics/ffi
Nov 12 10:24:53 Finished semantics/ffi                                           10s 264MB
Nov 12 10:24:53 Starting semantics
Nov 12 10:26:18 Finished semantics                                             1m24s   1GB
Nov 12 10:26:18 Starting semantics/proofs
Nov 12 10:29:55 Finished semantics/proofs                                      3m36s   1GB
Nov 12 10:29:55 Starting semantics/alt_semantics
Nov 12 10:30:09 Finished semantics/alt_semantics                                 13s 359MB
Nov 12 10:30:10 Starting semantics/alt_semantics/proofs
Nov 12 10:32:37 Finished semantics/alt_semantics/proofs                        2m27s 858MB
Nov 12 10:32:37 Starting basis/pure
Nov 12 10:33:28 Finished basis/pure                                              50s 951MB
Nov 12 10:33:28 Starting translator
Nov 12 10:36:44 Finished translator                                            3m15s   1GB
Nov 12 10:36:44 Starting compiler/parsing
Nov 12 10:37:54 Finished compiler/parsing                                      1m10s   2GB
Nov 12 10:37:55 Starting characteristic
Nov 12 10:43:34 Finished characteristic                                        5m39s   2GB
Nov 12 10:43:34 Starting translator/monadic
Nov 12 10:45:19 Finished translator/monadic                                    1m44s   1GB
Nov 12 10:45:19 Starting basis
Nov 12 11:30:24 Finished basis                                                45m03s  14GB
Nov 12 11:30:24 Starting compiler/inference
Nov 12 11:31:32 Finished compiler/inference                                    1m08s   1GB
Nov 12 11:31:32 Starting compiler/backend/reg_alloc
Nov 12 11:32:40 Finished compiler/backend/reg_alloc                            1m07s   1GB
Nov 12 11:32:40 Starting compiler/backend/gc
Nov 12 11:36:03 Finished compiler/backend/gc                                   3m22s   2GB
Nov 12 11:36:03 Starting compiler/backend
Nov 12 11:40:58 Finished compiler/backend                                      4m55s   3GB
Nov 12 11:40:58 Starting compiler/encoders/asm
Nov 12 11:41:22 Finished compiler/encoders/asm                                   23s 675MB
Nov 12 11:41:22 Starting compiler/encoders/x64
Nov 12 11:41:47 Finished compiler/encoders/x64                                   25s 616MB
Nov 12 11:41:48 Starting compiler/encoders/arm7
Nov 12 11:42:39 Finished compiler/encoders/arm7                                  51s 742MB
Nov 12 11:42:39 Starting compiler/encoders/arm8
Nov 12 11:42:53 Finished compiler/encoders/arm8                                  13s 975MB
Nov 12 11:42:53 Starting compiler/encoders/mips
Nov 12 11:43:11 Finished compiler/encoders/mips                                  18s   1GB
Nov 12 11:43:11 Starting compiler/encoders/riscv
Nov 12 11:43:28 Finished compiler/encoders/riscv                                 16s   1GB
Nov 12 11:43:28 Starting compiler/encoders/ag32
Nov 12 11:43:46 Finished compiler/encoders/ag32                                  18s 857MB
Nov 12 11:43:47 Starting compiler/backend/x64
Nov 12 11:44:06 Finished compiler/backend/x64                                    19s   1GB
Nov 12 11:44:06 Starting compiler/backend/arm7
Nov 12 11:44:27 Finished compiler/backend/arm7                                   20s   1GB
Nov 12 11:44:27 Starting compiler/backend/arm8
Nov 12 11:44:48 Finished compiler/backend/arm8                                   20s   1GB
Nov 12 11:44:48 Starting compiler/backend/mips
Nov 12 11:45:08 Finished compiler/backend/mips                                   20s   1GB
Nov 12 11:45:08 Starting compiler/backend/riscv
Nov 12 11:45:28 Finished compiler/backend/riscv                                  19s   1GB
Nov 12 11:45:28 Starting compiler/backend/ag32
Nov 12 11:46:38 Finished compiler/backend/ag32                                 1m09s   1GB
Nov 12 11:46:38 Starting compiler/parsing/proofs
Nov 12 11:53:27 Finished compiler/parsing/proofs                               6m48s 920MB
Nov 12 11:53:27 Starting compiler/inference/proofs
Nov 12 11:55:58 Finished compiler/inference/proofs                             2m30s   1GB
Nov 12 11:55:58 Starting compiler/backend/semantics
Nov 12 12:23:47 Finished compiler/backend/semantics                           27m49s   2GB
Nov 12 12:23:47 Starting compiler/backend/reg_alloc/proofs
Nov 12 12:27:15 Finished compiler/backend/reg_alloc/proofs                     3m27s   1GB
Nov 12 12:27:15 Starting compiler/backend/proofs
Nov 12 12:28:33 FAILED: compiler/backend/proofs
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/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[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/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/topology[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/src/floating-point[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/update[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/gc[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Finished $(CAKEMLDIR)/misc                                                                                     (0.000s) 
Starting work on README.md
Starting work on bvi_tailrecProofTheory
Starting work on data_liveProofTheory
Starting work on data_simpProofTheory
README.md                                                                          compiler/backend/proofs  (1s)     OK
Starting work on data_spaceProofTheory
data_simpProofTheory                                                               compiler/backend/proofs (14s)     OK
Starting work on bvl_constProofTheory
data_spaceProofTheory                                                              compiler/backend/proofs (25s)     OK
Starting work on bvi_letProofTheory
bvi_letProofTheory                                                                 compiler/backend/proofs (18s)     OK
Starting work on clos_annotateProofTheory
data_liveProofTheory                                                               compiler/backend/proofs (66s)     OK
Starting work on bvi_to_dataProofTheory
clos_annotateProofTheory                                                           compiler/backend/proofs (25s)     OK
Starting work on clos_callProofTheory
bvi_tailrecProofTheory                                                             compiler/backend/proofs (73s)FAIL<1>
 Saved definition __ "state_rel_def"
 Saved theorem _____ "state_rel_const"
 Saved theorem _____ "state_rel_with_clock"
 Saved theorem _____ "state_rel_code_rel"
 Saved theorem _____ "code_rel_union"
 Saved theorem _____ "namespace_rel_union"
 Saved theorem _____ "compile_prog_namespace_rel"
 error in quse /home/cug/hk324/cml-regression/cakeml-1633/compiler/backend/proofs/bvi_tailrecProofScript.sml : HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}
 error in load /home/cug/hk324/cml-regression/cakeml-1633/compiler/backend/proofs/bvi_tailrecProofScript : HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}
 Uncaught exception: HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}
bvl_constProofTheory                                                               compiler/backend/proofs (58s)MKILLED
bvi_to_dataProofTheory                                                             compiler/backend/proofs  (6s)MKILLED
clos_callProofTheory                                                               compiler/backend/proofs  (0s)MKILLED