CakeML Regression Test

Job 329

CakeML:4a58d73e99e866304d818b7d4713beab86e6b921
  Fix some compiler proofs for irule change [May 29 20:16:14]
HOL:1c2f967871ae1f61f75a30d037a4100413700554
  Fix pretty-printing bug for large-if-exprs in rator position [May 28 08:02:00]
Machine:cakeml1798 4.4.0-98-generic x86_64 GNU/Linux

May 29 21:01:49 Claimed job
May 29 21:01:56 Reusing HOL
May 29 21:02:11 Starting developers/bin
May 29 21:02:22 Finished developers/bin                                           8s 224MB
May 29 21:02:24 Starting semantics/ffi
May 29 21:02:42 Finished semantics/ffi                                           16s 249MB
May 29 21:02:44 Starting semantics
May 29 21:04:44 Finished semantics                                             1m57s   1GB
May 29 21:04:46 Starting semantics/proofs
May 29 21:08:00 Finished semantics/proofs                                      3m12s   1GB
May 29 21:08:02 Starting basis/pure
May 29 21:09:28 Finished basis/pure                                            1m23s 588MB
May 29 21:09:30 Starting translator
May 29 21:16:14 Finished translator                                            6m41s   1GB
May 29 21:16:16 Starting compiler/parsing
May 29 21:18:27 Finished compiler/parsing                                      2m08s   2GB
May 29 21:18:29 Starting characteristic
May 29 21:22:56 Finished characteristic                                        4m25s   1GB
May 29 21:22:58 Starting basis
May 29 21:51:30 Finished basis                                                28m30s   3GB
May 29 21:51:32 Starting translator/monadic
May 29 21:51:36 Finished translator/monadic                                       2s  11MB
May 29 21:51:38 Starting compiler/inference
May 29 21:54:14 Finished compiler/inference                                    2m33s   1GB
May 29 21:54:16 Starting compiler/backend/reg_alloc
May 29 21:55:12 Finished compiler/backend/reg_alloc                              54s   1GB
May 29 21:55:14 Starting compiler/backend/gc
May 29 22:10:21 Finished compiler/backend/gc                                  15m04s   2GB
May 29 22:10:23 Starting compiler/backend
May 29 22:10:28 Finished compiler/backend                                         3s  15MB
May 29 22:10:30 Starting compiler/encoders/asm
May 29 22:10:33 Finished compiler/encoders/asm                                    0s  11MB
May 29 22:10:35 Starting compiler/encoders/x64
May 29 22:12:04 Finished compiler/encoders/x64                                 1m26s 568MB
May 29 22:12:06 Starting compiler/encoders/arm6
May 29 22:15:08 Finished compiler/encoders/arm6                                2m59s   1GB
May 29 22:15:10 Starting compiler/encoders/arm8
May 29 22:15:56 Finished compiler/encoders/arm8                                  44s 396MB
May 29 22:15:58 Starting compiler/encoders/mips
May 29 22:17:35 Finished compiler/encoders/mips                                1m35s 769MB
May 29 22:17:37 Starting compiler/encoders/riscv
May 29 22:19:13 Finished compiler/encoders/riscv                               1m34s 494MB
May 29 22:19:15 Starting compiler/backend/x64
May 29 22:19:50 Finished compiler/backend/x64                                    33s 919MB
May 29 22:19:52 Starting compiler/backend/arm6
May 29 22:20:29 Finished compiler/backend/arm6                                   34s   1GB
May 29 22:20:31 Starting compiler/backend/arm8
May 29 22:21:04 Finished compiler/backend/arm8                                   31s 856MB
May 29 22:21:06 Starting compiler/backend/mips
May 29 22:21:42 Finished compiler/backend/mips                                   34s   1GB
May 29 22:21:44 Starting compiler/backend/riscv
May 29 22:22:19 Finished compiler/backend/riscv                                  32s   1GB
May 29 22:22:21 Starting compiler/parsing/proofs
May 29 22:26:23 Finished compiler/parsing/proofs                               4m00s 927MB
May 29 22:26:25 Starting compiler/inference/proofs
May 29 22:30:29 Finished compiler/inference/proofs                             4m01s 996MB
May 29 22:30:31 Starting compiler/backend/semantics
May 29 22:48:48 Finished compiler/backend/semantics                           18m15s   3GB
May 29 22:48:50 Starting compiler/backend/reg_alloc/proofs
May 29 22:50:15 Finished compiler/backend/reg_alloc/proofs                     1m23s 483MB
May 29 22:50:17 Starting compiler/backend/proofs
May 29 23:19:12 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