Job 1289

CakeML:107033ffe631f1bc87118d7432c551699eabff59
  update several makefiles [Jun 23 05:23:40]
#738 (export_update)
Merging into:31cf1e91d1619efb58727dc9f0b85abac809d44d
  Open BasicProvers to get scripts to build [Jun 23 09:46:49]
HOL:de873d08971c87bcfbbce86cdcd59909ef803929
  Remove some Unicode in src [Jun 22 00:09:18]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jun 23 09:47:12 Claimed job
Jun 23 09:47:14 Reusing HOL
Jun 23 09:47:19 Starting developers
Jun 23 09:47:19 Finished developers                                               0s  30MB
Jun 23 09:47:20 Starting developers/bin
Jun 23 09:47:26 Finished developers/bin                                           6s   1GB
Jun 23 09:47:26 Starting semantics/ffi
Jun 23 09:47:35 Finished semantics/ffi                                            8s 255MB
Jun 23 09:47:35 Starting semantics
Jun 23 09:48:56 Finished semantics                                             1m20s   1GB
Jun 23 09:48:56 Starting semantics/proofs
Jun 23 09:52:12 Finished semantics/proofs                                      3m16s   1GB
Jun 23 09:52:12 Starting semantics/alt_semantics
Jun 23 09:52:20 Finished semantics/alt_semantics                                  7s 332MB
Jun 23 09:52:20 Starting semantics/alt_semantics/proofs
Jun 23 09:54:23 Finished semantics/alt_semantics/proofs                        2m02s 915MB
Jun 23 09:54:23 Starting basis/pure
Jun 23 09:57:17 Finished basis/pure                                            2m53s 842MB
Jun 23 09:57:17 Starting translator
Jun 23 09:59:53 Finished translator                                            2m35s   1GB
Jun 23 09:59:53 Starting compiler/parsing
Jun 23 10:01:01 Finished compiler/parsing                                      1m07s   2GB
Jun 23 10:01:01 Starting characteristic
Jun 23 10:06:44 Finished characteristic                                        5m42s   1GB
Jun 23 10:06:44 Starting translator/monadic
Jun 23 10:08:19 Finished translator/monadic                                    1m35s   1GB
Jun 23 10:08:20 Starting basis
Jun 23 10:11:19 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)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[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:   10s  user:   10s     OK
Starting work on fsFFITheory
runtimeFFITheory                                                              real:   11s  user:   11s     OK
Starting work on basis_ffi.o
basis_ffi.o                                                                   real:    0s  user:    0s     OK
clFFITheory                                                                   real:   12s  user:   11s     OK
RuntimeProgTheory                                                             real:   25s  user:   25s     OK
Starting work on OptionProgTheory
Starting work on RuntimeProofTheory
fsFFITheory                                                                   real:   16s  user:   15s     OK
Starting work on fsFFIPropsTheory
OptionProgTheory                                                              real:   14s  user:   14s     OK
Starting work on ListProgTheory
RuntimeProofTheory                                                            real:   25s  user:   25s     OK
ListProgTheory                                                                real:   46s  user:   45s     OK
Starting work on VectorProgTheory
Starting work on ListProofTheory
fsFFIPropsTheory                                                              real:   61s  user:   60s     OK
ListProofTheory                                                               real:   25s  user:   24s     OK
VectorProgTheory                                                              real:   31s  user:   30s     OK
Starting work on StringProgTheory
StringProgTheory                                                              real:   34s  user:   33s     OK
Starting work on mlbasicsProgTheory
mlbasicsProgTheory                                                            real:   26s  user:   24sFAIL<1>
 Saved definition __ "lt_def"
 Translating lt
 Saved theorem _____ "nsLookup_mlbasicsProg_env_4_pfun_eqs"
 Saved theorem _____ "lt_v_thm"
 Saved theorem _____ "lt_v_thm"
 /home/myreen/regression/cakeml-1289/basis/mlbasicsProgScript.sml:44: error: Value or constructor (great_tm) has not been declared in structure intSyntax
 Found near trans ">" intSyntax.great_tm
 error in quse /home/myreen/regression/cakeml-1289/basis/mlbasicsProgScript.sml : Fail "Static Errors"
 error in load /home/myreen/regression/cakeml-1289/basis/mlbasicsProgScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"