Job 326

CakeML:e7b7b8392c3dabd2637a6c6d4550ec9fc92a93a5
  Tweak links in README [May 29 10:01:50]
HOL:1c2f967871ae1f61f75a30d037a4100413700554
  Fix pretty-printing bug for large-if-exprs in rator position [May 28 08:02:00]
Machine:cakeml1795 4.4.0-98-generic x86_64 GNU/Linux

May 29 10:23:25 Claimed job
May 29 10:23:33 Reusing HOL
May 29 10:23:48 Starting developers/bin
May 29 10:23:58 Finished developers/bin                                           8s 224MB
May 29 10:24:00 Starting semantics/ffi
May 29 10:24:19 Finished semantics/ffi                                           16s 242MB
May 29 10:24:21 Starting semantics
May 29 10:26:17 Finished semantics                                             1m54s   1GB
May 29 10:26:19 Starting semantics/proofs
May 29 10:29:31 Finished semantics/proofs                                      3m10s   1GB
May 29 10:29:33 Starting basis/pure
May 29 10:35:15 Finished basis/pure                                            5m40s 768MB
May 29 10:35:17 Starting translator
May 29 10:41:52 Finished translator                                            6m32s   1GB
May 29 10:41:53 Starting compiler/parsing
May 29 10:44:04 Finished compiler/parsing                                      2m08s   2GB
May 29 10:44:06 Starting characteristic
May 29 10:48:29 Finished characteristic                                        4m21s   1GB
May 29 10:48:31 Starting basis
May 29 10:53:34 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
OptionProgTheory                                                                                OK
Starting work on ListProgTheory
fsFFITheory                                                                                     OK
Starting work on fsFFIPropsTheory
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