Job 1916

CakeML:86b62101fdc21bd9864f672361d78fd39d184801
  Merge remote-tracking branch 'origin/master' into let-lift [Jun 10 13:52:37]
#884 (let-lift)
Merging into:f7195c3d29d6bd5f389a7ff307f998a45d56552f
  Merge pull request #888 from CakeML/deflate [Jun 09 07:20:45]
HOL:48bc6e3fcf4f5c1a81a122354d8838d83bbce3ef
  Re-organise Holmake code to isolate some "file-system" code [Jun 07 01:51:29]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Jun 10 13:55:20 Claimed job
Jun 10 13:55:22 Reusing HOL
Jun 10 13:55:34 Starting developers
Jun 10 13:55:39 Finished developers                                               4s 134MB
Jun 10 13:55:39 Starting developers/bin
Jun 10 13:55:46 Finished developers/bin                                           6s   1GB
Jun 10 13:55:46 Starting semantics/ffi
Jun 10 13:55:56 Finished semantics/ffi                                            9s 261MB
Jun 10 13:55:56 Starting semantics
Jun 10 13:58:21 Finished semantics                                             2m25s   1GB
Jun 10 13:58:22 Starting semantics/proofs
Jun 10 14:05:24 Finished semantics/proofs                                      7m02s   1GB
Jun 10 14:05:24 Starting semantics/alt_semantics
Jun 10 14:05:52 Finished semantics/alt_semantics                                 27s 567MB
Jun 10 14:05:52 Starting semantics/alt_semantics/proofs
Jun 10 14:17:14 Finished semantics/alt_semantics/proofs                       11m21s   1GB
Jun 10 14:17:14 Starting basis/pure
Jun 10 14:18:21 Finished basis/pure                                            1m06s 907MB
Jun 10 14:18:21 Starting translator
Jun 10 14:22:03 Finished translator                                            3m42s   1GB
Jun 10 14:22:03 Starting compiler/parsing
Jun 10 14:23:26 Finished compiler/parsing                                      1m22s   3GB
Jun 10 14:23:26 Starting characteristic
Jun 10 14:30:30 Finished characteristic                                        7m04s   1GB
Jun 10 14:30:30 Starting translator/monadic
Jun 10 14:32:29 Finished translator/monadic                                    1m59s   1GB
Jun 10 14:32:29 Starting basis
Jun 10 15:23:30 Finished basis                                                50m59s  13GB
Jun 10 15:23:30 Starting compiler/inference
Jun 10 15:25:01 Finished compiler/inference                                    1m30s   1GB
Jun 10 15:25:01 Starting compiler/backend/reg_alloc
Jun 10 15:26:46 Finished compiler/backend/reg_alloc                            1m45s   1GB
Jun 10 15:26:46 Starting compiler/backend/gc
Jun 10 15:31:13 Finished compiler/backend/gc                                   4m26s   1GB
Jun 10 15:31:13 Starting compiler/backend
Jun 10 15:37:16 Finished compiler/backend                                      6m02s   2GB
Jun 10 15:37:16 Starting compiler/encoders/asm
Jun 10 15:37:47 Finished compiler/encoders/asm                                   30s 759MB
Jun 10 15:37:47 Starting compiler/encoders/x64
Jun 10 15:38:17 Finished compiler/encoders/x64                                   29s   1GB
Jun 10 15:38:17 Starting compiler/encoders/arm7
Jun 10 15:39:11 Finished compiler/encoders/arm7                                  53s   1GB
Jun 10 15:39:11 Starting compiler/encoders/arm8
Jun 10 15:39:28 Finished compiler/encoders/arm8                                  17s 670MB
Jun 10 15:39:29 Starting compiler/encoders/arm8_asl
Jun 10 15:42:02 Finished compiler/encoders/arm8_asl                            2m33s   1GB
Jun 10 15:42:02 Starting compiler/encoders/mips
Jun 10 15:42:23 Finished compiler/encoders/mips                                  21s   1GB
Jun 10 15:42:23 Starting compiler/encoders/riscv
Jun 10 15:42:42 Finished compiler/encoders/riscv                                 18s   1GB
Jun 10 15:42:43 Starting compiler/encoders/ag32
Jun 10 15:43:05 Finished compiler/encoders/ag32                                  22s   1GB
Jun 10 15:43:05 Starting compiler/backend/x64
Jun 10 15:43:28 Finished compiler/backend/x64                                    22s   1GB
Jun 10 15:43:28 Starting compiler/backend/arm7
Jun 10 15:43:52 Finished compiler/backend/arm7                                   24s   1GB
Jun 10 15:43:52 Starting compiler/backend/arm8
Jun 10 15:44:14 Finished compiler/backend/arm8                                   21s   1GB
Jun 10 15:44:14 Starting compiler/backend/mips
Jun 10 15:44:38 Finished compiler/backend/mips                                   23s   1GB
Jun 10 15:44:38 Starting compiler/backend/riscv
Jun 10 15:45:01 Finished compiler/backend/riscv                                  22s   1GB
Jun 10 15:45:01 Starting compiler/backend/ag32
Jun 10 15:46:29 Finished compiler/backend/ag32                                 1m27s   1GB
Jun 10 15:46:29 Starting compiler/parsing/proofs
Jun 10 15:50:14 Finished compiler/parsing/proofs                               3m44s   1GB
Jun 10 15:50:14 Starting compiler/inference/proofs
Jun 10 15:53:01 Finished compiler/inference/proofs                             2m47s 998MB
Jun 10 15:53:01 Starting compiler/backend/semantics
Jun 10 16:25:24 Finished compiler/backend/semantics                           32m22s   1GB
Jun 10 16:25:24 Starting compiler/backend/reg_alloc/proofs
Jun 10 16:28:57 Finished compiler/backend/reg_alloc/proofs                     3m32s   1GB
Jun 10 16:28:57 Starting compiler/backend/proofs
Jun 10 16:43:08 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)/semantics/alt_semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Scanned 48 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 (18s)     OK
Starting work on bvl_constProofTheory
data_spaceProofTheory                                                              compiler/backend/proofs (30s)     OK
Starting work on bvi_letProofTheory
bvi_letProofTheory                                                                 compiler/backend/proofs (22s)     OK
Starting work on clos_annotateProofTheory
data_liveProofTheory                                                               compiler/backend/proofs (80s)     OK
Starting work on bvi_to_dataProofTheory
clos_annotateProofTheory                                                           compiler/backend/proofs (29s)     OK
Starting work on clos_callProofTheory
bvl_constProofTheory                                                               compiler/backend/proofs (99s)     OK
Starting work on bvl_handleProofTheory
bvl_handleProofTheory                                                              compiler/backend/proofs (23s)     OK
Starting work on bvl_inlineProofTheory
bvi_tailrecProofTheory                                                             compiler/backend/proofs(171s)     OK
Starting work on clos_fvsProofTheory
bvl_inlineProofTheory                                                              compiler/backend/proofs (35s)     OK
Starting work on bvl_to_bviProofTheory
clos_fvsProofTheory                                                                compiler/backend/proofs (19s)     OK
Starting work on clos_knownPropsTheory
clos_knownPropsTheory                                                              compiler/backend/proofs (15s)     OK
Starting work on clos_letopProofTheory
bvi_to_dataProofTheory                                                             compiler/backend/proofs(139s)     OK
Starting work on clos_opProofTheory
clos_letopProofTheory                                                              compiler/backend/proofs (21s)     OK
Starting work on clos_ticksProofTheory
clos_opProofTheory                                                                 compiler/backend/proofs (25s)     OK
Starting work on clos_mtiProofTheory
clos_callProofTheory                                                               compiler/backend/proofs(164s)     OK
Starting work on clos_numberProofTheory
clos_ticksProofTheory                                                              compiler/backend/proofs (27s)     OK
Starting work on clos_knownProofTheory
clos_numberProofTheory                                                             compiler/backend/proofs (29s)     OK
Starting work on bvl_jumpProofTheory
clos_mtiProofTheory                                                                compiler/backend/proofs (35s)     OK
Starting work on word_simpProofTheory
bvl_jumpProofTheory                                                                compiler/backend/proofs (13s)     OK
Starting work on word_bignumProofTheory
word_simpProofTheory                                                               compiler/backend/proofs (58s)     OK
Starting work on word_gcFunctionsTheory
bvl_to_bviProofTheory                                                              compiler/backend/proofs(180s)     OK
Starting work on word_allocProofTheory
word_gcFunctionsTheory                                                             compiler/backend/proofs (43s)     OK
Starting work on data_to_word_memoryProofTheory
clos_knownProofTheory                                                              compiler/backend/proofs(134s)     OK
Starting work on clos_to_bvlProofTheory
word_bignumProofTheory                                                             compiler/backend/proofs(211s)     OK
Starting work on word_instProofTheory
word_instProofTheory                                                               compiler/backend/proofs (56s)     OK
Starting work on word_removeProofTheory
clos_to_bvlProofTheory                                                             compiler/backend/proofs(207s)     OK
Starting work on word_depthProofTheory
word_removeProofTheory                                                             compiler/backend/proofs (34s)     OK
Starting work on flat_patternProofTheory
flat_patternProofTheory                                                            compiler/backend/proofs (45s)     OK
Starting work on flat_to_closProofTheory
word_depthProofTheory                                                              compiler/backend/proofs (64s)     OK
Starting work on lab_filterProofTheory
flat_to_closProofTheory                                                            compiler/backend/proofs (85s)     OK
Starting work on stack_removeProofTheory
lab_filterProofTheory                                                              compiler/backend/proofs (68s)     OK
Starting work on source_evalProofTheory
source_evalProofTheory                                                             compiler/backend/proofs (92s)FAIL<1>
   (s' with eval_state updated_by adjust_oracle ci (compile_decs  f),res)
 
 failed.
 Failed to prove theorem adjust_oracle_evaluate.
 
 Exception raised at Tactical.THEN1:
 first subgoal not solved by second tactic (THEN1 on line 2334) (THEN1 on line 2330) (THEN1 on line 2357)
 error in quse /home/cug/hk324/cml-regression/cakeml-1916/compiler/backend/proofs/source_evalProofScript.sml : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 2334) (THEN1 on line 2330) (THEN1 on line 2357)", origin_function = "THEN1", origin_structure = "Tactical"}
 error in load /home/cug/hk324/cml-regression/cakeml-1916/compiler/backend/proofs/source_evalProofScript : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 2334) (THEN1 on line 2330) (THEN1 on line 2357)", origin_function = "THEN1", origin_structure = "Tactical"}
 Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 2334) (THEN1 on line 2330) (THEN1 on line 2357)", origin_function = "THEN1", origin_structure = "Tactical"}
word_allocProofTheory                                                              compiler/backend/proofs(473s)MKILLED
data_to_word_memoryProofTheory                                                     compiler/backend/proofs(446s)MKILLED
stack_removeProofTheory                                                            compiler/backend/proofs (94s)MKILLED