Job 797

CakeML:84be3269450a8eb815bcc20e0dd686f66ca21fea
  Update backendComputeLib use of ThmSetData. [Apr 12 13:44:08]
#630 (compute-thmset)
Merging into:b2c1007e2e54c223bcc1b1cb29e00c496a52e275
  Find and fix more definition-saves that cause loss of "compute" [Apr 15 05:40:26]
HOL:a083c115f48c74233904c5c3e8fa848239e6ab9c
  Deal with rebindings of ptree_{size,fringe}_def in grammarScript [Apr 13 11:02:48]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Apr 15 13:09:49 Claimed job
Apr 15 13:09:54 Reusing HOL
Apr 15 13:09:59 Starting developers
Apr 15 13:09:59 Finished developers                                               0s  36MB
Apr 15 13:10:00 Starting developers/bin
Apr 15 13:10:30 Finished developers/bin                                          29s 204MB
Apr 15 13:10:30 Starting semantics/ffi
Apr 15 13:10:38 Finished semantics/ffi                                            7s 218MB
Apr 15 13:10:39 Starting semantics
Apr 15 13:11:58 Finished semantics                                             1m18s   1GB
Apr 15 13:11:58 Starting semantics/proofs
Apr 15 13:14:58 Finished semantics/proofs                                      2m59s   1GB
Apr 15 13:14:59 Starting basis/pure
Apr 15 13:15:43 Finished basis/pure                                              44s 657MB
Apr 15 13:15:44 Starting translator
Apr 15 13:17:23 Finished translator                                            1m38s   1GB
Apr 15 13:17:23 Starting compiler/parsing
Apr 15 13:18:21 Finished compiler/parsing                                        58s   2GB
Apr 15 13:18:22 Starting characteristic
Apr 15 13:23:32 Finished characteristic                                        5m09s   1GB
Apr 15 13:23:32 Starting translator/monadic
Apr 15 13:24:57 Finished translator/monadic                                    1m24s   1GB
Apr 15 13:24:57 Starting basis
Apr 15 13:41:21 Finished basis                                                16m24s   2GB
Apr 15 13:41:22 Starting compiler/inference
Apr 15 13:42:53 Finished compiler/inference                                    1m30s   1GB
Apr 15 13:42:53 Starting compiler/backend/reg_alloc
Apr 15 13:43:45 Finished compiler/backend/reg_alloc                              51s   1GB
Apr 15 13:43:45 Starting compiler/backend/gc
Apr 15 13:51:48 Finished compiler/backend/gc                                   8m02s   1GB
Apr 15 13:51:49 Starting compiler/backend
Apr 15 13:51:50 Finished compiler/backend                                         0s  42MB
Apr 15 13:51:50 Starting compiler/encoders/asm
Apr 15 13:51:51 Finished compiler/encoders/asm                                    0s  32MB
Apr 15 13:51:51 Starting compiler/encoders/x64
Apr 15 13:52:14 Finished compiler/encoders/x64                                   22s 941MB
Apr 15 13:52:14 Starting compiler/encoders/arm6
Apr 15 13:52:59 Finished compiler/encoders/arm6                                  44s 669MB
Apr 15 13:53:00 Starting compiler/encoders/arm8
Apr 15 13:53:12 Finished compiler/encoders/arm8                                  11s 551MB
Apr 15 13:53:12 Starting compiler/encoders/mips
Apr 15 13:53:27 Finished compiler/encoders/mips                                  15s 765MB
Apr 15 13:53:28 Starting compiler/encoders/riscv
Apr 15 13:53:41 Finished compiler/encoders/riscv                                 13s   1GB
Apr 15 13:53:42 Starting compiler/encoders/ag32
Apr 15 13:53:57 Finished compiler/encoders/ag32                                  15s 755MB
Apr 15 13:53:57 Starting compiler/backend/x64
Apr 15 13:54:14 Finished compiler/backend/x64                                    16s   1GB
Apr 15 13:54:14 Starting compiler/backend/arm6
Apr 15 13:54:31 Finished compiler/backend/arm6                                   16s   1GB
Apr 15 13:54:31 Starting compiler/backend/arm8
Apr 15 13:54:48 Finished compiler/backend/arm8                                   16s   1GB
Apr 15 13:54:48 Starting compiler/backend/mips
Apr 15 13:55:05 Finished compiler/backend/mips                                   16s   1GB
Apr 15 13:55:05 Starting compiler/backend/riscv
Apr 15 13:55:22 Finished compiler/backend/riscv                                  17s   1GB
Apr 15 13:55:23 Starting compiler/backend/ag32
Apr 15 13:56:30 Finished compiler/backend/ag32                                 1m06s   1GB
Apr 15 13:56:30 Starting compiler/parsing/proofs
Apr 15 14:02:12 Finished compiler/parsing/proofs                               5m41s 791MB
Apr 15 14:02:13 Starting compiler/inference/proofs
Apr 15 14:04:52 Finished compiler/inference/proofs                             2m38s   1GB
Apr 15 14:04:52 Starting compiler/backend/semantics
Apr 15 14:12:00 Finished compiler/backend/semantics                            7m07s   2GB
Apr 15 14:12:01 Starting compiler/backend/reg_alloc/proofs
Apr 15 14:14:40 Finished compiler/backend/reg_alloc/proofs                     2m39s   1GB
Apr 15 14:14:41 Starting compiler/backend/proofs
Apr 15 14:48:50 FAILED: compiler/backend/proofs
]0;Holmake: .]0;Holmake: ~/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/machine-code/multiword]0;Holmake: ~/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: .]0;Holmake: ..]0;Holmake: ~/regression/cakeml-797/basis/pure]0;Holmake: ~/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/balanced_bst]0;Holmake: ~/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression/cakeml-797/basis/pure]0;Holmake: ~/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/formal-languages]0;Holmake: ~/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/regression/cakeml-797/basis/pure]0;Holmake: ~/regression/cakeml-797/misc]0;Holmake: ~/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-797/misc]0;Holmake: ~/regression/cakeml-797/developers]0;Holmake: ~/regression/cakeml-797/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-797/misc]0;Holmake: ~/regression/cakeml-797/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-797/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-797/misc]0;Holmake: ~/regression/cakeml-797/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-797/basis/pure]0;Holmake: ~/regression/cakeml-797/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ..]0;Holmake: ../reg_alloc]0;Holmake: ~/regression/cakeml-797/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-797/semantics]0;Holmake: ~/regression/cakeml-797/semantics/ffi]0;Holmake: ~/regression/cakeml-797/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-797/semantics]0;Holmake: ~/regression/cakeml-797/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-797/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-797/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ../reg_alloc]0;Holmake: ~/regression/cakeml-797/unverified/reg_alloc]0;Holmake: ~/regression/cakeml-797/unverified/reg_alloc[1mWorking in $(CAKEMLDIR)/unverified/reg_alloc[0m
]0;Holmake: ../reg_alloc]0;Holmake: ../reg_alloc[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc[0m
]0;Holmake: ..]0;Holmake: ../../encoders/asm]0;Holmake: ~/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: ../../encoders/asm]0;Holmake: ../../encoders/asm[1mWorking in $(CAKEMLDIR)/compiler/encoders/asm[0m
]0;Holmake: ..]0;Holmake: ~/regression/cakeml-797/semantics/proofs]0;Holmake: ~/regression/cakeml-797/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ..]0;Holmake: ..[1mWorking in $(CAKEMLDIR)/compiler/backend[0m
]0;Holmake: .]0;Holmake: ../gc]0;Holmake: ../gc[1mWorking in $(CAKEMLDIR)/compiler/backend/gc[0m
]0;Holmake: .]0;Holmake: ../reg_alloc/proofs]0;Holmake: ~/regression/cakeml-797/translator/monadic]0;Holmake: ~/regression/cakeml-797/characteristic]0;Holmake: ~/regression/cakeml-797/compiler/parsing]0;Holmake: ~/regression/cakeml-797/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-797/characteristic]0;Holmake: ~/regression/cakeml-797/translator]0;Holmake: ~/regression/cakeml-797/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-797/characteristic]0;Holmake: ~/regression/cakeml-797/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/regression/cakeml-797/translator/monadic]0;Holmake: ~/regression/cakeml-797/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ../reg_alloc/proofs]0;Holmake: ../reg_alloc/proofs[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
]0;Holmake: .]0;Holmake: ../semantics]0;Holmake: ../semantics[1mWorking in $(CAKEMLDIR)/compiler/backend/semantics[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/backend/proofs[0m
Starting work on bvi_tailrecProofTheory
Starting work on data_liveProofTheory
Starting work on data_simpProofTheory
Starting work on data_spaceProofTheory
data_simpProofTheory                                                                                       OK
Starting work on bvl_constProofTheory
data_spaceProofTheory                                                                                      OK
Starting work on bvl_jumpProofTheory
bvl_jumpProofTheory                                                                                        OK
Starting work on bvi_letProofTheory
data_liveProofTheory                                                                                       OK
Starting work on bvi_to_dataProofTheory
bvi_letProofTheory                                                                                         OK
Starting work on clos_annotateProofTheory
bvl_constProofTheory                                                                                       OK
Starting work on bvl_handleProofTheory
clos_annotateProofTheory                                                                                   OK
Starting work on clos_callProofTheory
bvl_handleProofTheory                                                                                      OK
Starting work on bvl_inlineProofTheory
bvl_inlineProofTheory                                                                                      OK
Starting work on clos_fvsProofTheory
clos_fvsProofTheory                                                                                        OK
Starting work on clos_knownPropsTheory
clos_knownPropsTheory                                                                                      OK
Starting work on clos_letopProofTheory
bvi_to_dataProofTheory                                                                                     OK
Starting work on clos_ticksProofTheory
clos_letopProofTheory                                                                                      OK
Starting work on clos_labelsProofTheory
clos_ticksProofTheory                                                                                      OK
Starting work on clos_knownProofTheory
bvi_tailrecProofTheory                                                                                     OK
Starting work on bvl_to_bviProofTheory
clos_labelsProofTheory                                                                                     OK
Starting work on clos_mtiProofTheory
clos_mtiProofTheory                                                                                        OK
Starting work on clos_numberProofTheory
clos_numberProofTheory                                                                                     OK
Starting work on word_simpProofTheory
clos_knownProofTheory                                                                                      OK
Starting work on word_bignumProofTheory
word_simpProofTheory                                                                                       OK
Starting work on word_gcFunctionsTheory
clos_callProofTheory                                                                                       OK
Starting work on clos_to_bvlProofTheory
word_gcFunctionsTheory                                                                                     OK
Starting work on data_to_word_memoryProofTheory
bvl_to_bviProofTheory                                                                                      OK
Starting work on word_allocProofTheory
word_bignumProofTheory                                                                                     OK
Starting work on word_instProofTheory
clos_to_bvlProofTheory                                                                                     OK
Starting work on word_removeProofTheory
word_removeProofTheory                                                                                     OK
Starting work on flat_elimProofTheory
word_instProofTheory                                                                                       OK
Starting work on flat_exh_matchProofTheory
flat_exh_matchProofTheory                                                                                  OK
Starting work on flat_reorder_matchProofTheory
flat_elimProofTheory                                                                                       OK
Starting work on flat_to_patProofTheory
flat_reorder_matchProofTheory                                                                              OK
Starting work on flat_uncheck_ctorsProofTheory
flat_uncheck_ctorsProofTheory                                                                              OK
Starting work on lab_filterProofTheory
flat_to_patProofTheory                                                                                     OK
Starting work on stack_removeProofTheory
lab_filterProofTheory                                                                                      OK
Starting work on pat_to_closProofTheory
pat_to_closProofTheory                                                                                     OK
Starting work on source_to_flatProofTheory
data_to_word_memoryProofTheory                                                                             OK
Starting work on stack_allocProofTheory
source_to_flatProofTheory                                                                                  OK
Starting work on stack_namesProofTheory
word_allocProofTheory                                                                                      OK
Starting work on word_to_wordProofTheory
stack_namesProofTheory                                                                                     OK
Starting work on word_to_stackProofTheory
word_to_wordProofTheory                                                                                    OK
Starting work on data_to_word_gcProofTheory
stack_removeProofTheory                                                                                    OK
Starting work on lab_to_targetProofTheory
data_to_word_gcProofTheory                                                                                 OK
Starting work on data_to_word_bignumProofTheory
lab_to_targetProofTheory                                                                                   OK
Starting work on word_elimProofTheory
stack_allocProofTheory                                                                                     OK
Starting work on README.md
README.md                                                                                                  OK
word_elimProofTheory                                                                                       OK
data_to_word_bignumProofTheory                                                                             OK
Starting work on data_to_word_assignProofTheory
word_to_stackProofTheory                                                                                   OK
Starting work on stack_to_labProofTheory
stack_to_labProofTheory                                                                                    OK
data_to_word_assignProofTheory                                                                             OK
Starting work on data_to_wordProofTheory
data_to_wordProofTheory                                                                           FAILED! <1>
          | SOME (Rerr (Rabort (Rffi_error f))) => res1 = SOME (FinalFFI f))
 
 failed.
 Failed to prove theorem compile_correct.
 
 Exception raised at Tactical.THEN1:
 first subgoal not solved by second tactic (THEN1 on line 486) (THEN1 on line 483) (THEN1 on line 491) (THEN1 on line 470) (THEN1 on line 515) (THEN1 on line 522)
 error in quse /home/myreen/regression/cakeml-797/compiler/backend/proofs/data_to_wordProofScript.sml : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 486) (THEN1 on line 483) (THEN1 on line 491) (THEN1 on line 470) (THEN1 on line 515) (THEN1 on line 522)", origin_function = "THEN1", origin_structure = "Tactical"}
 error in load data_to_wordProofScript : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 486) (THEN1 on line 483) (THEN1 on line 491) (THEN1 on line 470) (THEN1 on line 515) (THEN1 on line 522)", origin_function = "THEN1", origin_structure = "Tactical"}
 Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 486) (THEN1 on line 483) (THEN1 on line 491) (THEN1 on line 470) (THEN1 on line 515) (THEN1 on line 522)", origin_function = "THEN1", origin_structure = "Tactical"}