Job 1628

CakeML:13eb6f5aa6a5bb9c159b02dfa1cc8c1d7bfc4d3a
  Fix a mistake [Nov 09 13:44:27]
#842 (ramsey)
Merging into:2bdfb3baf85901465a77aabbe9b75af1d4696c45
  Update Lem definition of locn to match latest in HOL [Nov 08 21:22:53]
HOL:d2dbcbe459dd2f033f1843fbc065e419634d1314
  Reenable selftests src/{prekernel,parse} after 9aae9d6d5a [Nov 10 23:52:08]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Nov 11 19:17:41 Claimed job
Nov 11 19:17:46 Building HOL
Nov 11 19:27:07 Starting developers
Nov 11 19:27:11 Finished developers                                               4s 104MB
Nov 11 19:27:12 Starting developers/bin
Nov 11 19:27:18 Finished developers/bin                                           6s   1GB
Nov 11 19:27:19 Starting semantics/ffi
Nov 11 19:27:30 Finished semantics/ffi                                           11s 258MB
Nov 11 19:27:30 Starting semantics
Nov 11 19:29:03 Finished semantics                                             1m32s   1GB
Nov 11 19:29:03 Starting semantics/proofs
Nov 11 19:32:36 Finished semantics/proofs                                      3m32s   1GB
Nov 11 19:32:36 Starting semantics/alt_semantics
Nov 11 19:32:50 Finished semantics/alt_semantics                                 14s 362MB
Nov 11 19:32:50 Starting semantics/alt_semantics/proofs
Nov 11 19:35:19 Finished semantics/alt_semantics/proofs                        2m28s   1GB
Nov 11 19:35:19 Starting basis/pure
Nov 11 19:38:08 Finished basis/pure                                            2m48s 905MB
Nov 11 19:38:08 Starting translator
Nov 11 19:41:22 Finished translator                                            3m14s   1GB
Nov 11 19:41:22 Starting compiler/parsing
Nov 11 19:42:33 Finished compiler/parsing                                      1m10s   1GB
Nov 11 19:42:33 Starting characteristic
Nov 11 19:48:15 Finished characteristic                                        5m42s   1GB
Nov 11 19:48:16 Starting translator/monadic
Nov 11 19:49:59 Finished translator/monadic                                    1m43s   1GB
Nov 11 19:49:59 Starting basis
Nov 11 20:35:13 Finished basis                                                45m10s  16GB
Nov 11 20:35:14 Starting compiler/inference
Nov 11 20:36:29 Finished compiler/inference                                    1m15s   1GB
Nov 11 20:36:30 Starting compiler/backend/reg_alloc
Nov 11 20:37:37 Finished compiler/backend/reg_alloc                            1m07s   1GB
Nov 11 20:37:38 Starting compiler/backend/gc
Nov 11 20:41:09 Finished compiler/backend/gc                                   3m31s   2GB
Nov 11 20:41:09 Starting compiler/backend
Nov 11 20:46:07 Finished compiler/backend                                      4m57s   4GB
Nov 11 20:46:07 Starting compiler/encoders/asm
Nov 11 20:46:30 Finished compiler/encoders/asm                                   22s 700MB
Nov 11 20:46:30 Starting compiler/encoders/x64
Nov 11 20:47:33 Finished compiler/encoders/x64                                 1m02s 735MB
Nov 11 20:47:33 Starting compiler/encoders/arm7
Nov 11 20:49:34 Finished compiler/encoders/arm7                                2m01s   1GB
Nov 11 20:49:35 Starting compiler/encoders/arm8
Nov 11 20:50:12 Finished compiler/encoders/arm8                                  37s 848MB
Nov 11 20:50:13 Starting compiler/encoders/mips
Nov 11 20:51:40 Finished compiler/encoders/mips                                1m27s 923MB
Nov 11 20:51:41 Starting compiler/encoders/riscv
Nov 11 20:53:26 Finished compiler/encoders/riscv                               1m44s   1GB
Nov 11 20:53:26 Starting compiler/encoders/ag32
Nov 11 20:53:44 Finished compiler/encoders/ag32                                  18s 719MB
Nov 11 20:53:44 Starting compiler/backend/x64
Nov 11 20:54:04 Finished compiler/backend/x64                                    19s   1GB
Nov 11 20:54:04 Starting compiler/backend/arm7
Nov 11 20:54:26 Finished compiler/backend/arm7                                   21s   1GB
Nov 11 20:54:26 Starting compiler/backend/arm8
Nov 11 20:54:47 Finished compiler/backend/arm8                                   20s   1GB
Nov 11 20:54:47 Starting compiler/backend/mips
Nov 11 20:55:07 Finished compiler/backend/mips                                   19s   1GB
Nov 11 20:55:07 Starting compiler/backend/riscv
Nov 11 20:55:27 Finished compiler/backend/riscv                                  20s   1GB
Nov 11 20:55:27 Starting compiler/backend/ag32
Nov 11 20:56:39 Finished compiler/backend/ag32                                 1m11s   1GB
Nov 11 20:56:39 Starting compiler/parsing/proofs
Nov 11 21:03:26 Finished compiler/parsing/proofs                               6m47s   1GB
Nov 11 21:03:26 Starting compiler/inference/proofs
Nov 11 21:05:54 Finished compiler/inference/proofs                             2m27s   1GB
Nov 11 21:05:55 Starting compiler/backend/semantics
Nov 11 21:34:00 Finished compiler/backend/semantics                           28m05s   2GB
Nov 11 21:34:01 Starting compiler/backend/reg_alloc/proofs
Nov 11 21:37:32 Finished compiler/backend/reg_alloc/proofs                     3m27s   1GB
Nov 11 21:37:32 Starting compiler/backend/proofs
Nov 11 21:38:49 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  (0s)     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 (19s)     OK
Starting work on clos_annotateProofTheory
data_liveProofTheory                                                                                                                                   compiler/backend/proofs (69s)     OK
Starting work on bvi_to_dataProofTheory
bvi_tailrecProofTheory                                                                                                                                 compiler/backend/proofs (72s)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-1628/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-1628/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 (57s)MKILLED
clos_annotateProofTheory                                                                                                                               compiler/backend/proofs (24s)MKILLED
bvi_to_dataProofTheory                                                                                                                                 compiler/backend/proofs  (2s)MKILLED