Overview

Job 1784

CakeML:2f7d092124c1ac800cd551423e5c942a4e14723c
  Revert "Make translator use new lookup_indn from DefnBase"
HOL:b46e29d269344e1d2981f1c850969b4f6ff7a0ac
  Delete unused code; improve error messages in RealArith.sml
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

 Claimed job
 Reusing HOL
 Starting developers
 Finished developers                                               4s 120MB
 Starting developers/bin
 Finished developers/bin                                           4s 675MB
 Starting semantics/ffi
 Finished semantics/ffi                                            9s 249MB
 Starting semantics
 Finished semantics                                             2m04s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      3m40s   1GB
 Starting semantics/alt_semantics
 Finished semantics/alt_semantics                                 16s 613MB
 Starting semantics/alt_semantics/proofs
 Finished semantics/alt_semantics/proofs                        2m29s   1GB
 Starting basis/pure
 Finished basis/pure                                            1m02s 931MB
 Starting translator
 Finished translator                                            3m01s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                      1m14s   2GB
 Starting characteristic
 Finished characteristic                                        6m31s   2GB
 Starting translator/monadic
 Finished translator/monadic                                    1m55s   1GB
 Starting basis
 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