Job 325

CakeML:effd84cbe5aa3794a48b8960c317dc5b5a4dd938
  Fix translator/monadic proof broken by irule change [May 29 06:39:03]
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 07:13:10 Claimed job
May 29 07:13:20 Building HOL
May 29 07:24:51 Starting developers/bin
May 29 07:25:01 Finished developers/bin                                           8s 224MB
May 29 07:25:03 Starting semantics/ffi
May 29 07:26:08 Finished semantics/ffi                                         1m02s 360MB
May 29 07:26:10 Starting semantics
May 29 07:28:34 Finished semantics                                             2m22s   1GB
May 29 07:28:36 Starting semantics/proofs
May 29 07:31:51 Finished semantics/proofs                                      3m13s   1GB
May 29 07:31:53 Starting basis/pure
May 29 07:37:37 Finished basis/pure                                            5m41s 690MB
May 29 07:37:39 Starting translator
May 29 07:44:13 Finished translator                                            6m32s   1GB
May 29 07:44:15 Starting compiler/parsing
May 29 07:46:24 Finished compiler/parsing                                      2m06s   2GB
May 29 07:46:26 Starting characteristic
May 29 07:50:51 Finished characteristic                                        4m23s   1GB
May 29 07:50:53 Starting basis
May 29 07:56:03 FAILED: basis
]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: 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: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]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: pure]0;Holmake: pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: .]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: .]0;Holmake: ../translator/monadic]0;Holmake: ../translator/monadicWorking in $(CAKEMLDIR)/translator/monadic
Starting work on ml_monadBaseTheory
ml_monadBaseTheory                                                                              OK
Starting work on ml_monad_translatorBaseTheory
ml_monad_translatorBaseTheory                                                                   OK
Starting work on ml_monad_translatorTheory
Starting work on ml_monadStoreTheory
ml_monadStoreTheory                                                                             OK
ml_monad_translatorTheory                                                                       OK
Starting work on cfMonadTheory
cfMonadTheory                                                                                   OK
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/basis
Starting work on RuntimeProgTheory
Starting work on clFFITheory
Starting work on MarshallingTheory
Starting work on basis_ffi.o
basis_ffi.o                                                                                     OK
MarshallingTheory                                                                               OK
Starting work on fsFFITheory
clFFITheory                                                                                     OK
RuntimeProgTheory                                                                               OK
Starting work on OptionProgTheory
fsFFITheory                                                                                     OK
Starting work on fsFFIPropsTheory
OptionProgTheory                                                                                OK
Starting work on ListProgTheory
ListProgTheory                                                                                  OK
Starting work on VectorProgTheory
Starting work on ListProofTheory
fsFFIPropsTheory                                                                                OK
ListProofTheory                                                                        FAILED! <1>
 l start lv A.
     LIST_TYPE A l lv 
     (n xv.
          n < LENGTH l  A (EL n l) xv 
          app p fv [xv] (eff (start + n))
            (POSTv v. &UNIT_TYPE () v * eff (start + n + 1))) 
     app p List_app_v [fv; lv] (eff start)
       (POSTv v. &UNIT_TYPE () v * eff (start + LENGTH l))
 
 failed.
VectorProgTheory                                                                          M-KILLED