Overview

Job 1289

CakeML:107033ffe631f1bc87118d7432c551699eabff59
  update several makefiles
#738 (export_update)
Merging into:31cf1e91d1619efb58727dc9f0b85abac809d44d
  Open BasicProvers to get scripts to build
HOL:de873d08971c87bcfbbce86cdcd59909ef803929
  Remove some Unicode in src
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

 Claimed job
 Reusing HOL
 Starting developers
 Finished developers                                               0s  30MB
 Starting developers/bin
 Finished developers/bin                                           6s   1GB
 Starting semantics/ffi
 Finished semantics/ffi                                            8s 255MB
 Starting semantics
 Finished semantics                                             1m20s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      3m16s   1GB
 Starting semantics/alt_semantics
 Finished semantics/alt_semantics                                  7s 332MB
 Starting semantics/alt_semantics/proofs
 Finished semantics/alt_semantics/proofs                        2m02s 915MB
 Starting basis/pure
 Finished basis/pure                                            2m53s 842MB
 Starting translator
 Finished translator                                            2m35s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                      1m07s   2GB
 Starting characteristic
 Finished characteristic                                        5m42s   1GB
 Starting translator/monadic
 Finished translator/monadic                                    1m35s   1GB
 Starting basis
 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"