Job 1781

CakeML:3f7667f80ca4cd62a1f592b30bb4b266ae3fa963
  Update unifyTheory for HOL changes to Define [Feb 20 15:05:55]
HOL:52eeaf3318cb6512881f389d6c992b1949b376e9
  vimhol: revoke key shortcut for loading of HOL_CONFIG file (486e33c7b [Feb 17 20:53:06]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Feb 20 15:20:33 Claimed job
Feb 20 15:20:34 Reusing HOL
Feb 20 15:20:47 Starting developers
Feb 20 15:20:52 Finished developers                                               4s 159MB
Feb 20 15:20:52 Starting developers/bin
Feb 20 15:20:56 Finished developers/bin                                           4s 674MB
Feb 20 15:20:56 Starting semantics/ffi
Feb 20 15:21:07 Finished semantics/ffi                                           10s 233MB
Feb 20 15:21:07 Starting semantics
Feb 20 15:23:09 Finished semantics                                             2m02s   1GB
Feb 20 15:23:09 Starting semantics/proofs
Feb 20 15:26:48 Finished semantics/proofs                                      3m38s   1GB
Feb 20 15:26:48 Starting semantics/alt_semantics
Feb 20 15:27:04 Finished semantics/alt_semantics                                 16s 497MB
Feb 20 15:27:04 Starting semantics/alt_semantics/proofs
Feb 20 15:29:33 Finished semantics/alt_semantics/proofs                        2m28s 884MB
Feb 20 15:29:33 Starting basis/pure
Feb 20 15:30:35 Finished basis/pure                                            1m02s 839MB
Feb 20 15:30:35 Starting translator
Feb 20 15:33:37 Finished translator                                            3m01s   1GB
Feb 20 15:33:37 Starting compiler/parsing
Feb 20 15:34:52 Finished compiler/parsing                                      1m14s   2GB
Feb 20 15:34:52 Starting characteristic
Feb 20 15:41:15 Finished characteristic                                        6m23s   1GB
Feb 20 15:41:15 Starting translator/monadic
Feb 20 15:43:09 Finished translator/monadic                                    1m53s   1GB
Feb 20 15:43:09 Starting basis
Feb 20 15:45:15 FAILED: basis
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanned 28 directories
Starting work on RuntimeProgTheory
Starting work on clFFITheory
Starting work on MarshallingTheory
Starting work on README.md
README.md                                                                                                                                                                         (0s)     OK
Starting work on runtimeFFITheory
MarshallingTheory                                                                                                                                                                (11s)     OK
Starting work on fsFFITheory
runtimeFFITheory                                                                                                                                                                 (12s)     OK
Starting work on basis_ffi.o
basis_ffi.o                                                                                                                                                                       (0s)     OK
clFFITheory                                                                                                                                                                      (14s)     OK
RuntimeProgTheory                                                                                                                                                                (26s)     OK
Starting work on OptionProgTheory
Starting work on RuntimeProofTheory
fsFFITheory                                                                                                                                                                      (22s)     OK
Starting work on fsFFIPropsTheory
OptionProgTheory                                                                                                                                                                 (16s)     OK
Starting work on ListProgTheory
RuntimeProofTheory                                                                                                                                                               (26s)     OK
fsFFIPropsTheory                                                                                                                                                                 (54s)     OK
ListProgTheory                                                                                                                                                                   (50s)     OK
Starting work on VectorProgTheory
Starting work on ListProofTheory
ListProofTheory                                                                                                                                                                  (23s)FAIL<1>
 <<HOL message: Created theory "ListProof">>
 Loading translation: ListProg ... error in quse /home/cug/hk324/cml-regression/cakeml-1781/basis/ListProofScript.sml : HOL_ERR {message = "No translator data in theory ListProg", origin_function = "translation_extends", origin_structure = "ml_translatorLib"}
 error in load /home/cug/hk324/cml-regression/cakeml-1781/basis/ListProofScript : HOL_ERR {message = "No translator data in theory ListProg", origin_function = "translation_extends", origin_structure = "ml_translatorLib"}
 Uncaught exception: HOL_ERR {message = "No translator data in theory ListProg", origin_function = "translation_extends", origin_structure = "ml_translatorLib"}
VectorProgTheory                                                                                                                                                                 (24s)MKILLED