Job 297

CakeML:6660ae7384f92ec36b9ba75f2dbf09a068ea96cb
  Add PrettyPrinter module to the stdlib [Apr 13 13:44:09]
#482 (pp)
Merging into:ffce1e98edd43af5f177e1c1cdb612e8c4ac7f29
  Merge pull request #481 from CakeML/install-and-run [Apr 14 06:53:45]
HOL:689b9eb3eccdebc314664a6e583c8d8bc76c0591
  Fix terrible performance when reading large strings with Coding [Apr 14 09:47:40]
Machine:cakeml1796 4.4.0-22-generic x86_64 GNU/Linux

Apr 15 17:39:37 Claimed job
Apr 15 17:39:46 Building HOL
Apr 15 17:51:35 Starting developers/bin
Apr 15 17:51:47 Finished developers/bin                                           9s 136MB
Apr 15 17:51:49 Starting semantics/ffi
Apr 15 17:52:57 Finished semantics/ffi                                         1m06s 448MB
Apr 15 17:52:59 Starting semantics
Apr 15 17:56:05 Finished semantics                                             3m03s   1GB
Apr 15 17:56:07 Starting semantics/proofs
Apr 15 17:59:38 Finished semantics/proofs                                      3m29s 999MB
Apr 15 17:59:40 Starting basis/pure
Apr 15 18:06:01 Finished basis/pure                                            6m18s 732MB
Apr 15 18:06:03 Starting translator
Apr 15 18:13:16 Finished translator                                            7m11s 988MB
Apr 15 18:13:18 Starting compiler/parsing
Apr 15 18:15:44 Finished compiler/parsing                                      2m24s   2GB
Apr 15 18:15:46 Starting characteristic
Apr 15 18:20:28 Finished characteristic                                        4m40s   1GB
Apr 15 18:20:30 Starting basis
Apr 15 18:52:12 FAILED: basis
]0;Holmake: /scratch/cakeml/regression/HOL-689b9eb3eccdebc314664a6e583c8d8bc76c0591/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-689b9eb3eccdebc314664a6e583c8d8bc76c0591/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-689b9eb3eccdebc314664a6e583c8d8bc76c0591/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-689b9eb3eccdebc314664a6e583c8d8bc76c0591/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-689b9eb3eccdebc314664a6e583c8d8bc76c0591/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-689b9eb3eccdebc314664a6e583c8d8bc76c0591/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-689b9eb3eccdebc314664a6e583c8d8bc76c0591/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-689b9eb3eccdebc314664a6e583c8d8bc76c0591/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: pure]0;Holmake: ../misc]0;Holmake: /scratch/cakeml/regression/HOL-689b9eb3eccdebc314664a6e583c8d8bc76c0591/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-689b9eb3eccdebc314664a6e583c8d8bc76c0591/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../misc]0;Holmake: /scratch/cakeml/regression/HOL-689b9eb3eccdebc314664a6e583c8d8bc76c0591/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-689b9eb3eccdebc314664a6e583c8d8bc76c0591/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
VectorProgTheory                                                             OK
Starting work on StringProgTheory
ListProofTheory                                                              OK
StringProgTheory                                                             OK
Starting work on mlbasicsProgTheory
mlbasicsProgTheory                                                           OK
Starting work on IntProgTheory
IntProgTheory                                                                OK
Starting work on NumProgTheory
NumProgTheory                                                                OK
Starting work on RatProgTheory
RatProgTheory                                                                OK
Starting work on CharProgTheory
CharProgTheory                                                               OK
Starting work on Word64ProgTheory
Word64ProgTheory                                                             OK
Starting work on Word8ProgTheory
Word8ProgTheory                                                              OK
Starting work on Word8ArrayProgTheory
Word8ArrayProgTheory                                                         OK
Starting work on ArrayProgTheory
Starting work on Word8ArrayProofTheory
Word8ArrayProofTheory                                                        OK
ArrayProgTheory                                                              OK
Starting work on ArrayProofTheory
Starting work on CompareProgTheory
CompareProgTheory                                                            OK
Starting work on MapProgTheory
MapProgTheory                                                                OK
Starting work on CommandLineProgTheory
ArrayProofTheory                                                             OK
CommandLineProgTheory                                                        OK
Starting work on CommandLineProofTheory
Starting work on MarshallingProgTheory
MarshallingProgTheory                                                        OK
Starting work on TextIOProgTheory
CommandLineProofTheory                                                       OK
TextIOProgTheory                                                             OK
Starting work on PrettyPrinterProgTheory
Starting work on TextIOProofTheory
PrettyPrinterProgTheory                                                      OK
TextIOProofTheory                                                            OK
Starting work on basisProgTheory
Starting work on basis_ffiTheory
basisProgTheory                                                     FAILED! <1>
 error in quse /scratch/cakeml/regression/cakeml-297/basis/basisProgScript.sml : HOL_ERR {message = "no such theory: PrettyPrinterProg", origin_function = "fetch", origin_structure = "DB"}
 error in load basisProgScript : HOL_ERR {message = "no such theory: PrettyPrinterProg", origin_function = "fetch", origin_structure = "DB"}
 Uncaught exception: HOL_ERR {message = "no such theory: PrettyPrinterProg", origin_function = "fetch", origin_structure = "DB"}
 <<HOL message: Created theory "basisProg">>
 Loading translation: PrettyPrinterProg ... 
basis_ffiTheory                                                        M-KILLED