Job 1237

CakeML:600dfab04fac08dc249d0a4196c612de28735fd6
  Fix a broken proof [May 29 18:29:10]
HOL:16a774456e43bd29a9b94ee31e24f17e059e771f
  Implement a unification-based version of mp_then with similar API [May 20 07:12:37]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

May 29 18:42:28 Claimed job
May 29 18:42:34 Reusing HOL
May 29 18:43:21 Starting developers
May 29 18:43:25 Finished developers                                               4s 116MB
May 29 18:43:25 Starting developers/bin
May 29 18:43:33 Finished developers/bin                                           7s   1GB
May 29 18:43:33 Starting semantics/ffi
May 29 18:43:44 Finished semantics/ffi                                           10s 231MB
May 29 18:43:44 Starting semantics
May 29 18:45:06 Finished semantics                                             1m21s   1GB
May 29 18:45:06 Starting semantics/proofs
May 29 18:48:35 Finished semantics/proofs                                      3m29s 892MB
May 29 18:48:36 Starting semantics/alt_semantics
May 29 18:48:44 Finished semantics/alt_semantics                                  8s 282MB
May 29 18:48:44 Starting semantics/alt_semantics/proofs
May 29 18:50:56 Finished semantics/alt_semantics/proofs                        2m11s 975MB
May 29 18:50:56 Starting basis/pure
May 29 18:51:47 Finished basis/pure                                              50s 670MB
May 29 18:51:47 Starting translator
May 29 18:54:28 Finished translator                                            2m40s   1GB
May 29 18:54:28 Starting compiler/parsing
May 29 18:55:41 Finished compiler/parsing                                      1m12s   2GB
May 29 18:55:41 Starting characteristic
May 29 19:01:47 Finished characteristic                                        6m05s   2GB
May 29 19:01:47 Starting translator/monadic
May 29 19:03:25 Finished translator/monadic                                    1m37s   1GB
May 29 19:03:25 Starting basis
May 29 19:37:23 Finished basis                                                33m57s  14GB
May 29 19:37:23 Starting compiler/inference
May 29 19:38:25 Finished compiler/inference                                    1m01s   1GB
May 29 19:38:25 Starting compiler/backend/reg_alloc
May 29 19:39:28 Finished compiler/backend/reg_alloc                            1m02s   1GB
May 29 19:39:28 Starting compiler/backend/gc
May 29 19:42:49 Finished compiler/backend/gc                                   3m20s   2GB
May 29 19:42:49 Starting compiler/backend
May 30 11:47:40 Resuming compiler/backend
May 30 11:47:41 Finished compiler/backend                                         1s  22MB
May 30 11:47:41 Starting compiler/encoders/asm
May 30 11:48:03 Finished compiler/encoders/asm                                   22s 831MB
May 30 11:48:04 Starting compiler/encoders/x64
May 30 11:48:29 Finished compiler/encoders/x64                                   25s 981MB
May 30 11:48:29 Starting compiler/encoders/arm7
May 30 11:49:20 Finished compiler/encoders/arm7                                  50s 742MB
May 30 11:49:20 Starting compiler/encoders/arm8
May 30 11:49:33 Finished compiler/encoders/arm8                                  12s 886MB
May 30 11:49:34 Starting compiler/encoders/mips
May 30 11:49:51 Finished compiler/encoders/mips                                  16s   1GB
May 30 11:49:51 Starting compiler/encoders/riscv
May 30 11:50:07 Finished compiler/encoders/riscv                                 15s 739MB
May 30 11:50:07 Starting compiler/encoders/ag32
May 30 11:50:25 Finished compiler/encoders/ag32                                  18s 753MB
May 30 11:50:26 Starting compiler/backend/x64
May 30 11:50:44 Finished compiler/backend/x64                                    18s   1GB
May 30 11:50:44 Starting compiler/backend/arm7
May 30 11:51:05 Finished compiler/backend/arm7                                   20s   1GB
May 30 11:51:05 Starting compiler/backend/arm8
May 30 11:51:23 Finished compiler/backend/arm8                                   18s   1GB
May 30 11:51:23 Starting compiler/backend/mips
May 30 11:51:43 Finished compiler/backend/mips                                   19s   1GB
May 30 11:51:43 Starting compiler/backend/riscv
May 30 11:52:02 Finished compiler/backend/riscv                                  18s   1GB
May 30 11:52:02 Starting compiler/backend/ag32
May 30 11:53:14 Finished compiler/backend/ag32                                 1m11s   1GB
May 30 11:53:14 Starting compiler/parsing/proofs
May 30 11:59:04 Finished compiler/parsing/proofs                               5m49s   1GB
May 30 11:59:04 Starting compiler/inference/proofs
May 30 12:01:38 Finished compiler/inference/proofs                             2m33s   1GB
May 30 12:01:38 Starting compiler/backend/semantics
May 30 12:32:18 Finished compiler/backend/semantics                           30m39s   2GB
May 30 12:32:18 Starting compiler/backend/reg_alloc/proofs
May 30 12:36:03 Finished compiler/backend/reg_alloc/proofs                     3m44s 964MB
May 30 12:36:03 Starting compiler/backend/proofs
May 30 12:56:55 FAILED: compiler/backend/proofs
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)/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)/compiler/backend/reachability[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)/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/backend/reachability/proofs[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
Starting work on reachable_sptProofTheory
Starting work on README.md
Starting work on bvi_tailrecProofTheory
Starting work on data_liveProofTheory
README.md                                       real:    1s  user:    0s     OK
Starting work on data_simpProofTheory
reachable_sptProofTheory                        real:   12s  user:   11s     OK
Starting work on data_spaceProofTheory
data_simpProofTheory                            real:   14s  user:   13s     OK
Starting work on bvl_constProofTheory
data_spaceProofTheory                           real:   27s  user:   26s     OK
Starting work on bvi_letProofTheory
bvi_letProofTheory                              real:   20s  user:   18s     OK
Starting work on clos_annotateProofTheory
bvl_constProofTheory                            real:   53s  user:   52s     OK
Starting work on bvl_handleProofTheory
data_liveProofTheory                            real:   72s  user:   71s     OK
Starting work on bvi_to_dataProofTheory
clos_annotateProofTheory                        real:   27s  user:   26s     OK
Starting work on clos_callProofTheory
bvl_handleProofTheory                           real:   20s  user:   19s     OK
Starting work on bvl_inlineProofTheory
bvl_inlineProofTheory                           real:   34s  user:   32s     OK
Starting work on clos_fvsProofTheory
clos_fvsProofTheory                             real:   17s  user:   16s     OK
Starting work on clos_knownPropsTheory
clos_knownPropsTheory                           real:   11s  user:   10s     OK
Starting work on clos_letopProofTheory
clos_letopProofTheory                           real:   19s  user:   18s     OK
Starting work on clos_ticksProofTheory
bvi_tailrecProofTheory                          real:  191s  user:  188s     OK
Starting work on bvl_to_bviProofTheory
clos_ticksProofTheory                           real:   25s  user:   24s     OK
Starting work on clos_knownProofTheory
bvi_to_dataProofTheory                          real:  138s  user:  136s     OK
Starting work on clos_mtiProofTheory
clos_mtiProofTheory                             real:   37s  user:   35s     OK
Starting work on clos_numberProofTheory
clos_callProofTheory                            real:  185s  user:  181s     OK
Starting work on bvl_jumpProofTheory
clos_numberProofTheory                          real:   26s  user:   25s     OK
Starting work on word_simpProofTheory
bvl_jumpProofTheory                             real:   10s  user:    9s     OK
Starting work on word_bignumProofTheory
word_simpProofTheory                            real:   56s  user:   55s     OK
Starting work on word_gcFunctionsTheory
clos_knownProofTheory                           real:  136s  user:  133s     OK
Starting work on clos_to_bvlProofTheory
word_gcFunctionsTheory                          real:   28s  user:   26s     OK
Starting work on data_to_word_memoryProofTheory
bvl_to_bviProofTheory                           real:  198s  user:  195s     OK
Starting work on word_allocProofTheory
word_bignumProofTheory                          real:  216s  user:  212s     OK
Starting work on word_instProofTheory
word_instProofTheory                            real:   53s  user:   51s     OK
Starting work on word_removeProofTheory
clos_to_bvlProofTheory                          real:  220s  user:  215s     OK
Starting work on word_depthProofTheory
word_removeProofTheory                          real:   30s  user:   29s     OK
Starting work on flat_patternProofTheory
word_depthProofTheory                           real:   72s  user:   71s     OK
Starting work on flat_to_closProofTheory
flat_patternProofTheory                         real:   51s  user:   50s     OK
Starting work on lab_filterProofTheory
flat_to_closProofTheory                         real:   59s  user:   57s     OK
Starting work on stack_removeProofTheory
lab_filterProofTheory                           real:   60s  user:   58s     OK
Starting work on flat_elimProofTheory
flat_elimProofTheory                            real:   67s  user:   66s     OK
Starting work on source_to_flatProofTheory
source_to_flatProofTheory                       real:  110s  user:  107s     OK
Starting work on stack_allocProofTheory
stack_removeProofTheory                         real:  271s  user:  267s     OK
Starting work on lab_to_targetProofTheory
word_allocProofTheory                           real:  646s  user:  638s     OK
Starting work on word_to_wordProofTheory
data_to_word_memoryProofTheory                  real:  741s  user:  734s     OK
Starting work on stack_namesProofTheory
word_to_wordProofTheory                         real:   70s  user:   68s     OK
Starting work on data_to_word_gcProofTheory
stack_namesProofTheory                          real:   32s  user:   31s     OK
Starting work on stack_rawcallProofTheory
lab_to_targetProofTheory                        real:  242s  user:  238s     OK
Starting work on word_to_stackProofTheory
stack_rawcallProofTheory                        real:   75s  user:   72s     OK
Starting work on word_elimProofTheory
data_to_word_gcProofTheory                      real:  141s  user:  138sFAIL<1>
 error in load /home/cake/oven/regression/cakeml-1237/compiler/backend/proofs/data_to_word_gcProofScript : HOL_ERR {message = "goal completely solved by first tactic (THEN1 on line 4260) (THEN1 on line 4261)", origin_function = "THEN1", origin_structure = "Tactical"}
 Proof of 
 
 alloc_size k  bytes_in_word * n2w sp1 
 sp1 * (dimindex (:) DIV 8) < dimword (:)  good_dimindex (:) 
 k <= sp1
 
 failed.
 Failed to prove theorem alloc_size_LEQ_IMP.
 Uncaught exception: HOL_ERR {message = "goal completely solved by first tactic (THEN1 on line 4260) (THEN1 on line 4261)", origin_function = "THEN1", origin_structure = "Tactical"}
stack_allocProofTheory                                                  M-KILLED
word_to_stackProofTheory                                                M-KILLED
word_elimProofTheory                                                    M-KILLED