Job 1771

CakeML:18dda4f8186adc43fd0cb0290ee815b212ad66a7
  Change monad constructors in candle/overloading [Feb 14 09:37:28]
#863 (repl)
Merging into:67b312862a2b9919d20a41b16a6599ef4a7635fe
  Merge pull request #855 from CakeML/minor-reheapification [Feb 14 13:06:51]
HOL:7d8123fd0cb1e8c2b7e3fffb337516da7cb7c9df
  Reinstate sptreeTheory.lrnext_def, which 8247e5e3a465 had deleted [Feb 10 23:16:16]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Feb 14 20:53:57 Claimed job
Feb 14 20:53:59 Reusing HOL
Feb 14 20:54:13 Starting developers
Feb 14 20:54:17 Finished developers                                               4s  78MB
Feb 14 20:54:17 Starting developers/bin
Feb 14 20:54:22 Finished developers/bin                                           4s 674MB
Feb 14 20:54:22 Starting semantics/ffi
Feb 14 20:54:31 Finished semantics/ffi                                            9s 242MB
Feb 14 20:54:31 Starting semantics
Feb 14 20:56:12 Finished semantics                                             1m40s 963MB
Feb 14 20:56:12 Starting semantics/proofs
Feb 14 20:59:48 Finished semantics/proofs                                      3m35s   1GB
Feb 14 20:59:48 Starting semantics/alt_semantics
Feb 14 21:00:02 Finished semantics/alt_semantics                                 13s 407MB
Feb 14 21:00:02 Starting semantics/alt_semantics/proofs
Feb 14 21:02:30 Finished semantics/alt_semantics/proofs                        2m28s   1GB
Feb 14 21:02:31 Starting basis/pure
Feb 14 21:03:28 Finished basis/pure                                              57s 755MB
Feb 14 21:03:28 Starting translator
Feb 14 21:06:14 Finished translator                                            2m46s   1GB
Feb 14 21:06:15 Starting compiler/parsing
Feb 14 21:07:28 Finished compiler/parsing                                      1m13s   2GB
Feb 14 21:07:28 Starting characteristic
Feb 14 21:13:17 Finished characteristic                                        5m48s   2GB
Feb 14 21:13:17 Starting translator/monadic
Feb 14 21:15:05 Finished translator/monadic                                    1m47s   1GB
Feb 14 21:15:05 Starting basis
Feb 14 22:01:15 Finished basis                                                46m07s  11GB
Feb 14 22:01:15 Starting compiler/inference
Feb 14 22:02:24 Finished compiler/inference                                    1m09s   1GB
Feb 14 22:02:24 Starting compiler/backend/reg_alloc
Feb 14 22:03:31 Finished compiler/backend/reg_alloc                            1m06s   1GB
Feb 14 22:03:31 Starting compiler/backend/gc
Feb 14 22:07:02 Finished compiler/backend/gc                                   3m30s   2GB
Feb 14 22:07:02 Starting compiler/backend
Feb 14 22:12:14 Finished compiler/backend                                      5m12s   2GB
Feb 14 22:12:14 Starting compiler/encoders/asm
Feb 14 22:12:38 Finished compiler/encoders/asm                                   24s 728MB
Feb 14 22:12:39 Starting compiler/encoders/x64
Feb 14 22:13:06 Finished compiler/encoders/x64                                   27s   1GB
Feb 14 22:13:06 Starting compiler/encoders/arm7
Feb 14 22:13:58 Finished compiler/encoders/arm7                                  51s 672MB
Feb 14 22:13:58 Starting compiler/encoders/arm8
Feb 14 22:14:12 Finished compiler/encoders/arm8                                  14s 825MB
Feb 14 22:14:12 Starting compiler/encoders/arm8_asl
Feb 14 22:16:45 Finished compiler/encoders/arm8_asl                            2m32s 867MB
Feb 14 22:16:45 Starting compiler/encoders/mips
Feb 14 22:17:04 Finished compiler/encoders/mips                                  18s   1GB
Feb 14 22:17:04 Starting compiler/encoders/riscv
Feb 14 22:17:21 Finished compiler/encoders/riscv                                 16s 730MB
Feb 14 22:17:21 Starting compiler/encoders/ag32
Feb 14 22:17:40 Finished compiler/encoders/ag32                                  19s 648MB
Feb 14 22:17:40 Starting compiler/backend/x64
Feb 14 22:18:02 Finished compiler/backend/x64                                    21s   1GB
Feb 14 22:18:02 Starting compiler/backend/arm7
Feb 14 22:18:26 Finished compiler/backend/arm7                                   23s   1GB
Feb 14 22:18:26 Starting compiler/backend/arm8
Feb 14 22:18:47 Finished compiler/backend/arm8                                   21s   1GB
Feb 14 22:18:47 Starting compiler/backend/mips
Feb 14 22:19:10 Finished compiler/backend/mips                                   22s   1GB
Feb 14 22:19:10 Starting compiler/backend/riscv
Feb 14 22:19:31 Finished compiler/backend/riscv                                  21s   1GB
Feb 14 22:19:31 Starting compiler/backend/ag32
Feb 14 22:20:43 Finished compiler/backend/ag32                                 1m11s   1GB
Feb 14 22:20:43 Starting compiler/parsing/proofs
Feb 14 22:24:26 Finished compiler/parsing/proofs                               3m42s   1GB
Feb 14 22:24:26 Starting compiler/inference/proofs
Feb 14 22:26:56 Finished compiler/inference/proofs                             2m30s   1GB
Feb 14 22:26:56 Starting compiler/backend/semantics
Feb 14 22:55:31 Finished compiler/backend/semantics                           28m34s   2GB
Feb 14 22:55:31 Starting compiler/backend/reg_alloc/proofs
Feb 14 22:58:58 Finished compiler/backend/reg_alloc/proofs                     3m27s 860MB
Feb 14 22:58:58 Starting compiler/backend/proofs
Feb 14 23:07:28 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/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/algorithms[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[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/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[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)/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/hol88[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
Scanned 46 directories
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 (16s)     OK
Starting work on bvl_constProofTheory
data_spaceProofTheory                                                                                                                                    compiler/backend/proofs (27s)     OK
Starting work on bvi_letProofTheory
bvi_letProofTheory                                                                                                                                       compiler/backend/proofs (20s)     OK
Starting work on clos_annotateProofTheory
data_liveProofTheory                                                                                                                                     compiler/backend/proofs (70s)     OK
Starting work on bvi_to_dataProofTheory
clos_annotateProofTheory                                                                                                                                 compiler/backend/proofs (26s)     OK
Starting work on clos_callProofTheory
bvl_constProofTheory                                                                                                                                     compiler/backend/proofs (97s)     OK
Starting work on bvl_handleProofTheory
bvl_handleProofTheory                                                                                                                                    compiler/backend/proofs (21s)     OK
Starting work on bvl_inlineProofTheory
bvi_tailrecProofTheory                                                                                                                                   compiler/backend/proofs(168s)     OK
Starting work on clos_fvsProofTheory
bvl_inlineProofTheory                                                                                                                                    compiler/backend/proofs (31s)     OK
Starting work on bvl_to_bviProofTheory
clos_fvsProofTheory                                                                                                                                      compiler/backend/proofs (18s)     OK
Starting work on clos_knownPropsTheory
bvi_to_dataProofTheory                                                                                                                                   compiler/backend/proofs(129s)     OK
Starting work on clos_letopProofTheory
clos_knownPropsTheory                                                                                                                                    compiler/backend/proofs (13s)     OK
Starting work on clos_opProofTheory
clos_letopProofTheory                                                                                                                                    compiler/backend/proofs (20s)     OK
Starting work on clos_ticksProofTheory
clos_opProofTheory                                                                                                                                       compiler/backend/proofs (24s)     OK
Starting work on clos_mtiProofTheory
clos_callProofTheory                                                                                                                                     compiler/backend/proofs(158s)     OK
Starting work on clos_numberProofTheory
clos_ticksProofTheory                                                                                                                                    compiler/backend/proofs (25s)     OK
Starting work on clos_knownProofTheory
clos_mtiProofTheory                                                                                                                                      compiler/backend/proofs (33s)     OK
Starting work on bvl_jumpProofTheory
clos_numberProofTheory                                                                                                                                   compiler/backend/proofs (27s)     OK
Starting work on word_simpProofTheory
bvl_jumpProofTheory                                                                                                                                      compiler/backend/proofs (12s)     OK
Starting work on word_bignumProofTheory
word_simpProofTheory                                                                                                                                     compiler/backend/proofs (53s)     OK
Starting work on word_gcFunctionsTheory
bvl_to_bviProofTheory                                                                                                                                    compiler/backend/proofs(177s)     OK
Starting work on word_allocProofTheory
word_gcFunctionsTheory                                                                                                                                   compiler/backend/proofs (32s)     OK
Starting work on data_to_word_memoryProofTheory
clos_knownProofTheory                                                                                                                                    compiler/backend/proofs(126s)     OK
Starting work on clos_to_bvlProofTheory
word_bignumProofTheory                                                                                                                                   compiler/backend/proofs(191s)     OK
Starting work on word_instProofTheory
word_allocProofTheory                                                                                                                                    compiler/backend/proofs(147s)FAIL<1>
 Proved triviality _ "get_clash_sets_tl"
 Saved theorem _______ "colouring_ok_alt_thm"
 Saved theorem _______ "check_col_INJ"
 Saved theorem _______ "check_partial_col_INJ"
 Saved theorem _______ "IMAGE_DIFF"
 Saved theorem _______ "clash_tree_colouring_ok"
 Saved definition ____ "even_starting_locals_def"
 error in quse /home/cug/hk324/cml-regression/cakeml-1771/compiler/backend/proofs/word_allocProofScript.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-1771/compiler/backend/proofs/word_allocProofScript : 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"}
data_to_word_memoryProofTheory                                                                                                                           compiler/backend/proofs(142s)MKILLED
clos_to_bvlProofTheory                                                                                                                                   compiler/backend/proofs(120s)MKILLED
word_instProofTheory                                                                                                                                     compiler/backend/proofs (24s)MKILLED