Overview

Job 329

CakeML:4a58d73e99e866304d818b7d4713beab86e6b921
  Fix some compiler proofs for irule change
HOL:1c2f967871ae1f61f75a30d037a4100413700554
  Fix pretty-printing bug for large-if-exprs in rator position
Machine:cakeml1798 4.4.0-98-generic x86_64 GNU/Linux

 Claimed job
 Reusing HOL
 Starting developers/bin
 Finished developers/bin                                           8s 224MB
 Starting semantics/ffi
 Finished semantics/ffi                                           16s 249MB
 Starting semantics
 Finished semantics                                             1m57s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      3m12s   1GB
 Starting basis/pure
 Finished basis/pure                                            1m23s 588MB
 Starting translator
 Finished translator                                            6m41s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                      2m08s   2GB
 Starting characteristic
 Finished characteristic                                        4m25s   1GB
 Starting basis
 Finished basis                                                28m30s   3GB
 Starting translator/monadic
 Finished translator/monadic                                       2s  11MB
 Starting compiler/inference
 Finished compiler/inference                                    2m33s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                              54s   1GB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                  15m04s   2GB
 Starting compiler/backend
 Finished compiler/backend                                         3s  15MB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                    0s  11MB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                 1m26s 568MB
 Starting compiler/encoders/arm6
 Finished compiler/encoders/arm6                                2m59s   1GB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                  44s 396MB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                1m35s 769MB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                               1m34s 494MB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    33s 919MB
 Starting compiler/backend/arm6
 Finished compiler/backend/arm6                                   34s   1GB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   31s 856MB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   34s   1GB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  32s   1GB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                               4m00s 927MB
 Starting compiler/inference/proofs
 Finished compiler/inference/proofs                             4m01s 996MB
 Starting compiler/backend/semantics
 Finished compiler/backend/semantics                           18m15s   3GB
 Starting compiler/backend/reg_alloc/proofs
 Finished compiler/backend/reg_alloc/proofs                     1m23s 483MB
 Starting compiler/backend/proofs
 FAILED: compiler/backend/proofs
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/machine-code/multiword]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/machine-code/multiwordWorking in $(HOLDIR)/examples/machine-code/multiword
]0;Holmake: .]0;Holmake: ..]0;Holmake: ../../../basis/pure]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/balanced_bstWorking in $(HOLDIR)/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../misc]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../../../misc]0;Holmake: ../../../developers]0;Holmake: ../../../developersWorking in ../../../developers
]0;Holmake: ../../../misc]0;Holmake: ../../../misc/lem_lib_stub]0;Holmake: ../../../misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ../../../misc]0;Holmake: ../../../miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: ..]0;Holmake: ../reg_alloc]0;Holmake: ../../../translator/monadic]0;Holmake: ../../../characteristic]0;Holmake: ../../../compiler/parsing]0;Holmake: ../../../semantics]0;Holmake: ../../../semantics/ffi]0;Holmake: ../../../semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ../../../semantics]0;Holmake: ../../../semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ../../../compiler/parsing]0;Holmake: ../../../compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: ../../../characteristic]0;Holmake: ../../../semantics/alt_semantics/proofs]0;Holmake: ../../../semantics/alt_semantics]0;Holmake: ../../../semantics/alt_semanticsWorking in $(CAKEMLDIR)/semantics/alt_semantics
]0;Holmake: ../../../semantics/alt_semantics/proofs]0;Holmake: ../../../semantics/proofs]0;Holmake: ../../../semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ../../../semantics/alt_semantics/proofs]0;Holmake: ../../../semantics/alt_semantics/proofsWorking in $(CAKEMLDIR)/semantics/alt_semantics/proofs
]0;Holmake: ../../../characteristic]0;Holmake: ../../../translator]0;Holmake: ../../../translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: ../../../characteristic]0;Holmake: ../../../characteristicWorking in $(CAKEMLDIR)/characteristic
]0;Holmake: ../../../translator/monadic]0;Holmake: ../../../translator/monadicWorking in $(CAKEMLDIR)/translator/monadic
]0;Holmake: ../reg_alloc]0;Holmake: ../../../unverified/reg_alloc]0;Holmake: ../../../unverified/reg_allocWorking in $(CAKEMLDIR)/unverified/reg_alloc
]0;Holmake: ../reg_alloc]0;Holmake: ../reg_allocWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc
]0;Holmake: ..]0;Holmake: ../../encoders/asm]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/l3-machine-code/common]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/l3-machine-code/commonWorking in $(HOLDIR)/examples/l3-machine-code/common
]0;Holmake: ../../encoders/asm]0;Holmake: ../../encoders/asmWorking in $(CAKEMLDIR)/compiler/encoders/asm
]0;Holmake: ..]0;Holmake: ..Working in $(CAKEMLDIR)/compiler/backend
]0;Holmake: .]0;Holmake: ../gc]0;Holmake: ../gcWorking in $(CAKEMLDIR)/compiler/backend/gc
]0;Holmake: .]0;Holmake: ../reg_alloc/proofs]0;Holmake: ../reg_alloc/proofsWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
]0;Holmake: .]0;Holmake: ../semantics]0;Holmake: ../semanticsWorking in $(CAKEMLDIR)/compiler/backend/semantics
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/compiler/backend/proofs
Starting work on heap
heap                                                                                            OK
Starting work on data_liveProofTheory
Starting work on data_simpProofTheory
Starting work on data_spaceProofTheory
Starting work on bvi_letProofTheory
data_simpProofTheory                                                                            OK
Starting work on bvi_tailrecProofTheory
data_spaceProofTheory                                                                           OK
Starting work on bvl_constProofTheory
bvi_letProofTheory                                                                              OK
Starting work on bvl_jumpProofTheory
bvl_jumpProofTheory                                                                             OK
Starting work on clos_annotateProofTheory
data_liveProofTheory                                                                            OK
Starting work on bvi_to_dataProofTheory
clos_annotateProofTheory                                                                        OK
Starting work on clos_callProofTheory
bvl_constProofTheory                                                                            OK
Starting work on bvl_handleProofTheory
bvl_handleProofTheory                                                                           OK
Starting work on bvl_inlineProofTheory
bvi_to_dataProofTheory                                                                          OK
Starting work on clos_knownPropsTheory
clos_knownPropsTheory                                                                           OK
Starting work on clos_knownProofTheory
bvl_inlineProofTheory                                                                           OK
Starting work on clos_mtiProofTheory
clos_mtiProofTheory                                                                             OK
Starting work on clos_numberProofTheory
clos_numberProofTheory                                                                          OK
Starting work on con_to_decProofTheory
con_to_decProofTheory                                                                           OK
Starting work on word_simpProofTheory
clos_knownProofTheory                                                                      CHEATED
Starting work on word_bignumProofTheory
bvi_tailrecProofTheory                                                                          OK
Starting work on bvl_to_bviProofTheory
word_simpProofTheory                                                                            OK
Starting work on word_gcFunctionsTheory
clos_callProofTheory                                                                       CHEATED
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
word_instProofTheory                                                                            OK
Starting work on word_removeProofTheory
clos_to_bvlProofTheory                                                                     CHEATED
Starting work on exh_reorderProofTheory
word_removeProofTheory                                                                          OK
Starting work on exh_to_patProofTheory
exh_reorderProofTheory                                                                          OK
Starting work on dec_to_exhProofTheory
dec_to_exhProofTheory                                                                           OK
Starting work on lab_filterProofTheory
data_to_word_memoryProofTheory                                                                  OK
Starting work on stack_removeProofTheory
lab_filterProofTheory                                                                           OK
Starting work on mod_to_conProofTheory
exh_to_patProofTheory                                                                           OK
Starting work on pat_to_closProofTheory
pat_to_closProofTheory                                                                          OK
Starting work on source_to_modProofTheory
source_to_modProofTheory                                                                        OK
Starting work on stack_allocProofTheory
mod_to_conProofTheory                                                                           OK
Starting work on stack_namesProofTheory
stack_removeProofTheory                                                                         OK
Starting work on lab_to_targetProofTheory
stack_namesProofTheory                                                                          OK
Starting work on word_to_stackProofTheory
word_allocProofTheory                                                                           OK
Starting work on word_to_wordProofTheory
word_to_wordProofTheory                                                                         OK
Starting work on data_to_word_gcProofTheory
lab_to_targetProofTheory                                                                   CHEATED
Starting work on clos_letopProofTheory
clos_letopProofTheory                                                                           OK
Starting work on clos_ticksProofTheory
clos_ticksProofTheory                                                                  FAILED! <1>
 loc_opt f2 args2 t1 res2 t2 f1 args1 s1.
     evaluate_app loc_opt f2 args2 t1 = (res2,t2)  v_rel f1 f2 
     LIST_REL v_rel args1 args2  state_rel s1 t1 
     ck res1 s2.
         evaluate_app loc_opt f1 args1 (s1 with clock := s1.clock + ck) =
         (res1,s2)  result_rel (LIST_REL v_rel) v_rel res1 res2 
         state_rel s2 t2
 
 failed.
 Failed to prove theorem evaluate_remove_ticks.
stack_allocProofTheory                                                                    M-KILLED
word_to_stackProofTheory                                                                  M-KILLED
data_to_word_gcProofTheory                                                                M-KILLED