Job 1784

CakeML:2f7d092124c1ac800cd551423e5c942a4e14723c
  Revert "Make translator use new lookup_indn from DefnBase" [Feb 21 21:14:20]
HOL:b46e29d269344e1d2981f1c850969b4f6ff7a0ac
  Delete unused code; improve error messages in RealArith.sml [Feb 18 04:44:09]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Feb 21 21:51:00 Claimed job
Feb 21 21:51:01 Reusing HOL
Feb 21 21:51:14 Starting developers
Feb 21 21:51:18 Finished developers                                               4s 120MB
Feb 21 21:51:18 Starting developers/bin
Feb 21 21:51:23 Finished developers/bin                                           4s 675MB
Feb 21 21:51:23 Starting semantics/ffi
Feb 21 21:51:32 Finished semantics/ffi                                            9s 249MB
Feb 21 21:51:32 Starting semantics
Feb 21 21:53:37 Finished semantics                                             2m04s   1GB
Feb 21 21:53:37 Starting semantics/proofs
Feb 21 21:57:17 Finished semantics/proofs                                      3m40s   1GB
Feb 21 21:57:17 Starting semantics/alt_semantics
Feb 21 21:57:34 Finished semantics/alt_semantics                                 16s 613MB
Feb 21 21:57:34 Starting semantics/alt_semantics/proofs
Feb 21 22:00:05 Finished semantics/alt_semantics/proofs                        2m29s   1GB
Feb 21 22:00:06 Starting basis/pure
Feb 21 22:01:08 Finished basis/pure                                            1m02s 931MB
Feb 21 22:01:08 Starting translator
Feb 21 22:04:10 Finished translator                                            3m01s   1GB
Feb 21 22:04:10 Starting compiler/parsing
Feb 21 22:05:24 Finished compiler/parsing                                      1m14s   2GB
Feb 21 22:05:25 Starting characteristic
Feb 21 22:11:56 Finished characteristic                                        6m31s   2GB
Feb 21 22:11:56 Starting translator/monadic
Feb 21 22:13:52 Finished translator/monadic                                    1m55s   1GB
Feb 21 22:13:52 Starting basis
Feb 21 22:15:55 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                                                                                                                                                                (10s)     OK
Starting work on fsFFITheory
runtimeFFITheory                                                                                                                                                                 (12s)     OK
Starting work on basis_ffi.o
basis_ffi.o                                                                                                                                                                       (0s)     OK
clFFITheory                                                                                                                                                                      (14s)     OK
RuntimeProgTheory                                                                                                                                                                (27s)     OK
Starting work on OptionProgTheory
Starting work on RuntimeProofTheory
fsFFITheory                                                                                                                                                                      (22s)     OK
Starting work on fsFFIPropsTheory
OptionProgTheory                                                                                                                                                                 (17s)     OK
Starting work on ListProgTheory
RuntimeProofTheory                                                                                                                                                               (26s)     OK
fsFFIPropsTheory                                                                                                                                                                 (55s)     OK
ListProgTheory                                                                                                                                                                   (46s)     OK
Starting work on VectorProgTheory
Starting work on ListProofTheory
VectorProgTheory                                                                                                                                                                 (22s)FAIL<1>
 <<HOL message: Created theory "VectorProg">>
 Loading translation: ListProg ... error in quse /home/cug/hk324/cml-regression/cakeml-1784/basis/VectorProgScript.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-1784/basis/VectorProgScript : 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"}
ListProofTheory                                                                                                                                                                  (23s)MKILLED