Job 1290

CakeML: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 10:11:20 Claimed job
Jun 23 10:11:22 Reusing HOL
Jun 23 10:11:27 Starting developers
Jun 23 10:11:27 Finished developers                                               0s  30MB
Jun 23 10:11:27 Starting developers/bin
Jun 23 10:11:35 Finished developers/bin                                           7s   1GB
Jun 23 10:11:35 Starting semantics/ffi
Jun 23 10:11:45 Finished semantics/ffi                                            8s 254MB
Jun 23 10:11:45 Starting semantics
Jun 23 10:13:17 Finished semantics                                             1m31s 914MB
Jun 23 10:13:17 Starting semantics/proofs
Jun 23 10:16:46 Finished semantics/proofs                                      3m28s   1GB
Jun 23 10:16:46 Starting semantics/alt_semantics
Jun 23 10:16:54 Finished semantics/alt_semantics                                  8s 334MB
Jun 23 10:16:54 Starting semantics/alt_semantics/proofs
Jun 23 10:19:09 Finished semantics/alt_semantics/proofs                        2m14s 783MB
Jun 23 10:19:10 Starting basis/pure
Jun 23 10:20:02 Finished basis/pure                                              52s 678MB
Jun 23 10:20:02 Starting translator
Jun 23 10:22:51 Finished translator                                            2m48s   1GB
Jun 23 10:22:51 Starting compiler/parsing
Jun 23 10:23:57 Finished compiler/parsing                                      1m06s   2GB
Jun 23 10:23:57 Starting characteristic
Jun 23 10:29:44 Finished characteristic                                        5m46s   1GB
Jun 23 10:29:44 Starting translator/monadic
Jun 23 10:31:22 Finished translator/monadic                                    1m37s   1GB
Jun 23 10:31:22 Starting basis
Jun 23 10:34:30 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:   10s  user:   10s     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:   24s     OK
Starting work on OptionProgTheory
Starting work on RuntimeProofTheory
fsFFITheory                                                                                                                                   real:   16s  user:   15s     OK
Starting work on fsFFIPropsTheory
OptionProgTheory                                                                                                                              real:   14s  user:   13s     OK
Starting work on ListProgTheory
RuntimeProofTheory                                                                                                                            real:   25s  user:   24s     OK
fsFFIPropsTheory                                                                                                                              real:   59s  user:   58s     OK
ListProgTheory                                                                                                                                real:   49s  user:   48s     OK
Starting work on VectorProgTheory
Starting work on ListProofTheory
ListProofTheory                                                                                                                               real:   25s  user:   24s     OK
VectorProgTheory                                                                                                                              real:   33s  user:   32s     OK
Starting work on StringProgTheory
StringProgTheory                                                                                                                              real:   37s  user:   36s     OK
Starting work on mlbasicsProgTheory
mlbasicsProgTheory                                                                                                                            real:   26s  user:   25sFAIL<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-1290/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-1290/basis/mlbasicsProgScript.sml : Fail "Static Errors"
 error in load /home/myreen/regression/cakeml-1290/basis/mlbasicsProgScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"