Job 1532

CakeML:995ec1eda215e008c6ecebacdd6a33f7e4c70094
  Fix a typo in a name [May 20 12:12:11]
HOL:fe4634b86ea93f927bb796c73b7f77e15362962e
  Universally quantify statements [May 17 23:32:35]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

May 20 12:12:37 Claimed job
May 20 12:12:39 Reusing HOL
May 20 12:12:45 Starting developers
May 20 12:12:45 Finished developers                                               0s  33MB
May 20 12:12:46 Starting developers/bin
May 20 12:12:52 Finished developers/bin                                           5s   1GB
May 20 12:12:52 Starting semantics/ffi
May 20 12:13:02 Finished semantics/ffi                                           10s 284MB
May 20 12:13:02 Starting semantics
May 20 12:14:31 Finished semantics                                             1m28s   2GB
May 20 12:14:32 Starting semantics/proofs
May 20 12:18:11 Finished semantics/proofs                                      3m39s   2GB
May 20 12:18:11 Starting semantics/alt_semantics
May 20 12:18:20 Finished semantics/alt_semantics                                  8s 391MB
May 20 12:18:20 Starting semantics/alt_semantics/proofs
May 20 12:20:35 Finished semantics/alt_semantics/proofs                        2m15s   1GB
May 20 12:20:36 Starting basis/pure
May 20 12:21:36 Finished basis/pure                                            1m00s   1GB
May 20 12:21:36 Starting translator
May 20 12:25:12 Finished translator                                            3m35s   2GB
May 20 12:25:12 Starting compiler/parsing
May 20 12:26:30 Finished compiler/parsing                                      1m17s   2GB
May 20 12:26:30 Starting characteristic
May 20 12:33:37 Finished characteristic                                        7m06s   4GB
May 20 12:33:37 Starting translator/monadic
May 20 12:35:41 Finished translator/monadic                                    2m03s   3GB
May 20 12:35:42 Starting basis
May 20 12:38:23 FAILED: basis
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)/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/lem_lib_stub[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
Starting work on RuntimeProgTheory
Starting work on clFFITheory
Starting work on MarshallingTheory
Starting work on runtimeFFITheory
MarshallingTheory                                                                                                                                    real:   16s  user:   15s     OK
Starting work on fsFFITheory
runtimeFFITheory                                                                                                                                     real:   17s  user:   16s     OK
Starting work on basis_ffi.o
basis_ffi.o                                                                                                                                          real:    0s  user:    0s     OK
clFFITheory                                                                                                                                          real:   19s  user:   18s     OK
RuntimeProgTheory                                                                                                                                    real:   37s  user:   35s     OK
Starting work on OptionProgTheory
Starting work on RuntimeProofTheory
fsFFITheory                                                                                                                                          real:   23s  user:   22s     OK
Starting work on fsFFIPropsTheory
OptionProgTheory                                                                                                                                     real:   25s  user:   23s     OK
Starting work on ListProgTheory
RuntimeProofTheory                                                                                                                                   real:   38s  user:   36s     OK
fsFFIPropsTheory                                                                                                                                     real:   61s  user:   59s     OK
ListProgTheory                                                                                                                                       real:   60s  user:   58s     OK
Starting work on VectorProgTheory
Starting work on ListProofTheory
ListProofTheory                                                                                                                                      real:   35s  user:   34s     OK
VectorProgTheory                                                                                                                                     real:   36s  user:   34sFAIL<1>
 Saved theorem _____ "foldli_aux_v_thm"
 Translating foldli_1
 Saved theorem _____ "nsLookup_VectorProg_env_10_pfun_eqs"
 
 WARNING: foldli has a precondition.
 
 Saved theorem _____ "foldli_1_v_thm"
 error in quse /home/myreen/regression/cakeml-1532/basis/VectorProgScript.sml : HOL_ERR {message = "theorem VectorProg$foldli_side_def not found", origin_function = "definition", origin_structure = "DB"}
 error in load /home/myreen/regression/cakeml-1532/basis/VectorProgScript : HOL_ERR {message = "theorem VectorProg$foldli_side_def not found", origin_function = "definition", origin_structure = "DB"}
 Uncaught exception: HOL_ERR {message = "theorem VectorProg$foldli_side_def not found", origin_function = "definition", origin_structure = "DB"}