Job 1782

CakeML:e14025c3399762fc3f74f7f12240d03afaa4b32f
  Fixes given HOL's addition of an auto rwt for DIV [Feb 21 02:32:08]
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 02:45:42 Claimed job
Feb 21 02:45:46 Building HOL
Feb 21 02:55:16 Starting developers
Feb 21 02:55:20 Finished developers                                               4s 120MB
Feb 21 02:55:20 Starting developers/bin
Feb 21 02:55:25 Finished developers/bin                                           4s 675MB
Feb 21 02:55:25 Starting semantics/ffi
Feb 21 02:55:34 Finished semantics/ffi                                            9s 242MB
Feb 21 02:55:34 Starting semantics
Feb 21 02:57:49 Finished semantics                                             2m14s 994MB
Feb 21 02:57:49 Starting semantics/proofs
Feb 21 03:01:33 Finished semantics/proofs                                      3m43s 943MB
Feb 21 03:01:33 Starting semantics/alt_semantics
Feb 21 03:01:49 Finished semantics/alt_semantics                                 16s 580MB
Feb 21 03:01:50 Starting semantics/alt_semantics/proofs
Feb 21 03:04:17 Finished semantics/alt_semantics/proofs                        2m27s   1GB
Feb 21 03:04:17 Starting basis/pure
Feb 21 03:07:10 Finished basis/pure                                            2m52s 801MB
Feb 21 03:07:11 Starting translator
Feb 21 03:10:15 Finished translator                                            3m04s   2GB
Feb 21 03:10:15 Starting compiler/parsing
Feb 21 03:11:30 Finished compiler/parsing                                      1m15s   2GB
Feb 21 03:11:30 Starting characteristic
Feb 21 03:17:52 Finished characteristic                                        6m21s   2GB
Feb 21 03:17:52 Starting translator/monadic
Feb 21 03:19:47 Finished translator/monadic                                    1m54s   1GB
Feb 21 03:19:47 Starting basis
Feb 21 03:21:51 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
clFFITheory                                                                                                                                                                      (13s)     OK
Starting work on basis_ffi.o
basis_ffi.o                                                                                                                                                                       (0s)     OK
runtimeFFITheory                                                                                                                                                                 (13s)     OK
RuntimeProgTheory                                                                                                                                                                (29s)     OK
Starting work on OptionProgTheory
Starting work on RuntimeProofTheory
fsFFITheory                                                                                                                                                                      (22s)     OK
Starting work on fsFFIPropsTheory
OptionProgTheory                                                                                                                                                                 (15s)     OK
Starting work on ListProgTheory
RuntimeProofTheory                                                                                                                                                               (28s)     OK
fsFFIPropsTheory                                                                                                                                                                 (57s)     OK
ListProgTheory                                                                                                                                                                   (47s)     OK
Starting work on VectorProgTheory
Starting work on ListProofTheory
ListProofTheory                                                                                                                                                                  (24s)FAIL<1>
 <<HOL message: Created theory "ListProof">>
 Loading translation: ListProg ... error in quse /home/cug/hk324/cml-regression/cakeml-1782/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-1782/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