Overview

Job 1237

CakeML:600dfab04fac08dc249d0a4196c612de28735fd6
  Fix a broken proof
HOL:16a774456e43bd29a9b94ee31e24f17e059e771f
  Implement a unification-based version of mp_then with similar API
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

 Claimed job
 Reusing HOL
 Starting developers
 Finished developers                                               4s 116MB
 Starting developers/bin
 Finished developers/bin                                           7s   1GB
 Starting semantics/ffi
 Finished semantics/ffi                                           10s 231MB
 Starting semantics
 Finished semantics                                             1m21s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      3m29s 892MB
 Starting semantics/alt_semantics
 Finished semantics/alt_semantics                                  8s 282MB
 Starting semantics/alt_semantics/proofs
 Finished semantics/alt_semantics/proofs                        2m11s 975MB
 Starting basis/pure
 Finished basis/pure                                              50s 670MB
 Starting translator
 Finished translator                                            2m40s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                      1m12s   2GB
 Starting characteristic
 Finished characteristic                                        6m05s   2GB
 Starting translator/monadic
 Finished translator/monadic                                    1m37s   1GB
 Starting basis
 Finished basis                                                33m57s  14GB
 Starting compiler/inference
 Finished compiler/inference                                    1m01s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                            1m02s   1GB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                   3m20s   2GB
 Starting compiler/backend
 Resuming compiler/backend
 Finished compiler/backend                                         1s  22MB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                   22s 831MB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                   25s 981MB
 Starting compiler/encoders/arm7
 Finished compiler/encoders/arm7                                  50s 742MB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                  12s 886MB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                  16s   1GB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                                 15s 739MB
 Starting compiler/encoders/ag32
 Finished compiler/encoders/ag32                                  18s 753MB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    18s   1GB
 Starting compiler/backend/arm7
 Finished compiler/backend/arm7                                   20s   1GB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   18s   1GB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   19s   1GB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  18s   1GB
 Starting compiler/backend/ag32
 Finished compiler/backend/ag32                                 1m11s   1GB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                               5m49s   1GB
 Starting compiler/inference/proofs
 Finished compiler/inference/proofs                             2m33s   1GB
 Starting compiler/backend/semantics
 Finished compiler/backend/semantics                           30m39s   2GB
 Starting compiler/backend/reg_alloc/proofs
 Finished compiler/backend/reg_alloc/proofs                     3m44s 964MB
 Starting compiler/backend/proofs
 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