Job 1726

CakeML:196f1ac90a3720559f4e8047199cb161eefc1ccd
  Explicitly make shift_seq visible to get source_evalProof to build [Jan 19 03:37:05]
#855 (minor-reheapification)
Merging into:f51c690f1561377c251920f988e41104f70f3f36
  Fix a proof broken by recent HOL change [Jan 19 06:22:51]
HOL:27accc7f32d82c0cdc10754fd834b339ec17021f
  Tidy up some floating point proofs and extend bounds thms for sqrt [Jan 18 06:17:24]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Jan 19 17:56:29 Claimed job
Jan 19 17:56:34 Building HOL
Jan 19 18:05:48 Starting developers
Jan 19 18:05:52 Finished developers                                               4s 130MB
Jan 19 18:05:52 Starting developers/bin
Jan 19 18:05:56 Finished developers/bin                                           4s 675MB
Jan 19 18:05:57 Starting semantics/ffi
Jan 19 18:06:05 Finished semantics/ffi                                            8s 215MB
Jan 19 18:06:05 Starting semantics
Jan 19 18:07:50 Finished semantics                                             1m45s   1GB
Jan 19 18:07:50 Starting semantics/proofs
Jan 19 18:11:23 Finished semantics/proofs                                      3m32s   1GB
Jan 19 18:11:23 Starting semantics/alt_semantics
Jan 19 18:11:36 Finished semantics/alt_semantics                                 12s 399MB
Jan 19 18:11:36 Starting semantics/alt_semantics/proofs
Jan 19 18:14:02 Finished semantics/alt_semantics/proofs                        2m26s 744MB
Jan 19 18:14:02 Starting basis/pure
Jan 19 18:17:03 Finished basis/pure                                            3m00s 656MB
Jan 19 18:17:03 Starting translator
Jan 19 18:19:47 Finished translator                                            2m43s   1GB
Jan 19 18:19:47 Starting compiler/parsing
Jan 19 18:20:58 Finished compiler/parsing                                      1m11s   2GB
Jan 19 18:20:59 Starting characteristic
Jan 19 18:26:41 Finished characteristic                                        5m42s   1GB
Jan 19 18:26:41 Starting translator/monadic
Jan 19 18:28:23 Finished translator/monadic                                    1m41s   2GB
Jan 19 18:28:23 Starting basis
Jan 19 19:13:59 Finished basis                                                45m35s  13GB
Jan 19 19:13:59 Starting compiler/inference
Jan 19 19:15:14 Finished compiler/inference                                    1m14s   1GB
Jan 19 19:15:14 Starting compiler/backend/reg_alloc
Jan 19 19:16:20 Finished compiler/backend/reg_alloc                            1m06s   1GB
Jan 19 19:16:20 Starting compiler/backend/gc
Jan 19 19:19:49 Finished compiler/backend/gc                                   3m28s   1GB
Jan 19 19:19:49 Starting compiler/backend
Jan 19 19:24:25 Finished compiler/backend                                      4m36s   2GB
Jan 19 19:24:25 Starting compiler/encoders/asm
Jan 19 19:24:48 Finished compiler/encoders/asm                                   22s 702MB
Jan 19 19:24:48 Starting compiler/encoders/x64
Jan 19 19:25:48 Finished compiler/encoders/x64                                   59s 989MB
Jan 19 19:25:48 Starting compiler/encoders/arm7
Jan 19 19:27:45 Finished compiler/encoders/arm7                                1m57s   1GB
Jan 19 19:27:45 Starting compiler/encoders/arm8
Jan 19 19:28:24 Finished compiler/encoders/arm8                                  38s 882MB
Jan 19 19:28:24 Starting compiler/encoders/mips
Jan 19 19:29:48 Finished compiler/encoders/mips                                1m24s 890MB
Jan 19 19:29:48 Starting compiler/encoders/riscv
Jan 19 19:31:31 Finished compiler/encoders/riscv                               1m42s   1GB
Jan 19 19:31:31 Starting compiler/encoders/ag32
Jan 19 19:31:49 Finished compiler/encoders/ag32                                  18s 797MB
Jan 19 19:31:49 Starting compiler/backend/x64
Jan 19 19:32:09 Finished compiler/backend/x64                                    19s   1GB
Jan 19 19:32:09 Starting compiler/backend/arm7
Jan 19 19:32:30 Finished compiler/backend/arm7                                   21s   1GB
Jan 19 19:32:30 Starting compiler/backend/arm8
Jan 19 19:32:50 Finished compiler/backend/arm8                                   19s   1GB
Jan 19 19:32:50 Starting compiler/backend/mips
Jan 19 19:33:10 Finished compiler/backend/mips                                   19s   1GB
Jan 19 19:33:10 Starting compiler/backend/riscv
Jan 19 19:33:30 Finished compiler/backend/riscv                                  19s   1GB
Jan 19 19:33:30 Starting compiler/backend/ag32
Jan 19 19:34:37 Finished compiler/backend/ag32                                 1m07s   1GB
Jan 19 19:34:37 Starting compiler/parsing/proofs
Jan 19 19:38:19 Finished compiler/parsing/proofs                               3m41s   1GB
Jan 19 19:38:19 Starting compiler/inference/proofs
Jan 19 19:40:40 Finished compiler/inference/proofs                             2m20s   1GB
Jan 19 19:40:40 Starting compiler/backend/semantics
Jan 19 20:09:27 Finished compiler/backend/semantics                           28m46s   2GB
Jan 19 20:09:27 Starting compiler/backend/reg_alloc/proofs
Jan 19 20:12:55 Finished compiler/backend/reg_alloc/proofs                     3m27s 751MB
Jan 19 20:12:55 Starting compiler/backend/proofs
Jan 19 20:32:09 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)/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)/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/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 (13s)     OK
Starting work on bvl_constProofTheory
data_spaceProofTheory                                    compiler/backend/proofs (24s)     OK
Starting work on bvi_letProofTheory
bvi_letProofTheory                                       compiler/backend/proofs (18s)     OK
Starting work on clos_annotateProofTheory
data_liveProofTheory                                     compiler/backend/proofs (68s)     OK
Starting work on bvi_to_dataProofTheory
clos_annotateProofTheory                                 compiler/backend/proofs (24s)     OK
Starting work on clos_callProofTheory
bvl_constProofTheory                                     compiler/backend/proofs (94s)     OK
Starting work on bvl_handleProofTheory
bvl_handleProofTheory                                    compiler/backend/proofs (18s)     OK
Starting work on bvl_inlineProofTheory
bvl_inlineProofTheory                                    compiler/backend/proofs (29s)     OK
Starting work on clos_fvsProofTheory
bvi_tailrecProofTheory                                   compiler/backend/proofs(165s)     OK
Starting work on bvl_to_bviProofTheory
clos_fvsProofTheory                                      compiler/backend/proofs (14s)     OK
Starting work on clos_knownPropsTheory
clos_knownPropsTheory                                    compiler/backend/proofs (10s)     OK
Starting work on clos_letopProofTheory
bvi_to_dataProofTheory                                   compiler/backend/proofs(126s)     OK
Starting work on clos_opProofTheory
clos_letopProofTheory                                    compiler/backend/proofs (17s)     OK
Starting work on clos_ticksProofTheory
clos_opProofTheory                                       compiler/backend/proofs (21s)     OK
Starting work on clos_mtiProofTheory
clos_callProofTheory                                     compiler/backend/proofs(153s)     OK
Starting work on clos_numberProofTheory
clos_ticksProofTheory                                    compiler/backend/proofs (22s)     OK
Starting work on clos_knownProofTheory
clos_numberProofTheory                                   compiler/backend/proofs (23s)     OK
Starting work on bvl_jumpProofTheory
clos_mtiProofTheory                                      compiler/backend/proofs (31s)     OK
Starting work on word_simpProofTheory
bvl_jumpProofTheory                                      compiler/backend/proofs  (9s)     OK
Starting work on word_bignumProofTheory
word_simpProofTheory                                     compiler/backend/proofs (50s)     OK
Starting work on word_gcFunctionsTheory
word_gcFunctionsTheory                                   compiler/backend/proofs (28s)     OK
Starting work on data_to_word_memoryProofTheory
bvl_to_bviProofTheory                                    compiler/backend/proofs(174s)     OK
Starting work on word_allocProofTheory
clos_knownProofTheory                                    compiler/backend/proofs(123s)     OK
Starting work on clos_to_bvlProofTheory
word_bignumProofTheory                                   compiler/backend/proofs(187s)     OK
Starting work on word_instProofTheory
word_instProofTheory                                     compiler/backend/proofs (48s)     OK
Starting work on word_removeProofTheory
word_removeProofTheory                                   compiler/backend/proofs (28s)     OK
Starting work on word_depthProofTheory
clos_to_bvlProofTheory                                   compiler/backend/proofs(188s)     OK
Starting work on flat_patternProofTheory
flat_patternProofTheory                                  compiler/backend/proofs (38s)     OK
Starting work on flat_to_closProofTheory
word_depthProofTheory                                    compiler/backend/proofs (59s)     OK
Starting work on lab_filterProofTheory
lab_filterProofTheory                                    compiler/backend/proofs (55s)     OK
Starting work on stack_removeProofTheory
flat_to_closProofTheory                                  compiler/backend/proofs (74s)     OK
Starting work on source_evalProofTheory
source_evalProofTheory                                   compiler/backend/proofs (61s)     OK
Starting work on flat_elimProofTheory
flat_elimProofTheory                                     compiler/backend/proofs (34s)     OK
Starting work on source_to_flatProofTheory
source_to_flatProofTheory                                compiler/backend/proofs (98s)     OK
Starting work on stack_allocProofTheory
stack_removeProofTheory                                  compiler/backend/proofs(239s)     OK
Starting work on lab_to_targetProofTheory
word_allocProofTheory                                    compiler/backend/proofs(573s)     OK
Starting work on word_to_wordProofTheory
data_to_word_memoryProofTheory                           compiler/backend/proofs(604s)     OK
Starting work on stack_namesProofTheory
stack_namesProofTheory                                   compiler/backend/proofs (29s)     OK
Starting work on stack_rawcallProofTheory
word_to_wordProofTheory                                  compiler/backend/proofs (53s)     OK
Starting work on data_to_word_gcProofTheory
stack_rawcallProofTheory                                 compiler/backend/proofs (61s)     OK
Starting work on word_to_stackProofTheory
lab_to_targetProofTheory                                 compiler/backend/proofs(214s)     OK
Starting work on word_elimProofTheory
word_elimProofTheory                                     compiler/backend/proofs (33s)FAIL<1>
   n  domain (get_memory mem mdom)  k n1. k  mdom  mem k = Loc n n1
 
 failed.
 Failed to prove theorem domain_get_memory.
 
 Exception raised at BasicProvers.by:
 by's tactic failed to prove subgoal on line 389 (THEN1 on line 393) (THEN1 on line 394)
 error in quse /home/cug/hk324/cml-regression/cakeml-1726/compiler/backend/proofs/word_elimProofScript.sml : HOL_ERR {message = "by's tactic failed to prove subgoal on line 389 (THEN1 on line 393) (THEN1 on line 394)", origin_function = "by", origin_structure = "BasicProvers"}
 error in load /home/cug/hk324/cml-regression/cakeml-1726/compiler/backend/proofs/word_elimProofScript : HOL_ERR {message = "by's tactic failed to prove subgoal on line 389 (THEN1 on line 393) (THEN1 on line 394)", origin_function = "by", origin_structure = "BasicProvers"}
 Uncaught exception: HOL_ERR {message = "by's tactic failed to prove subgoal on line 389 (THEN1 on line 393) (THEN1 on line 394)", origin_function = "by", origin_structure = "BasicProvers"}
stack_allocProofTheory                                   compiler/backend/proofs(279s)MKILLED
data_to_word_gcProofTheory                               compiler/backend/proofs(165s)MKILLED
word_to_stackProofTheory                                 compiler/backend/proofs(107s)MKILLED