Job 1227

CakeML:c836e91226733fa77550b2b46d2cfd6f6b9f632c
  Merge pull request #735 from CakeML/lpr_new [May 13 09:44:58]
HOL:312b135db970ffbf5ef47a7cb46e98896a950de8
  emacs-mode: describe a regression test better [May 14 05:13:35]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

May 15 01:50:33 Claimed job
May 15 01:50:40 Building HOL
May 15 02:03:39 Starting developers
May 15 02:03:44 Finished developers                                               4s 116MB
May 15 02:03:44 Starting developers/bin
May 15 02:03:54 Finished developers/bin                                           7s   1GB
May 15 02:03:54 Starting semantics/ffi
May 15 02:04:05 Finished semantics/ffi                                           10s 233MB
May 15 02:04:05 Starting semantics
May 15 02:05:38 Finished semantics                                             1m31s   1GB
May 15 02:05:38 Starting semantics/proofs
May 15 02:09:11 Finished semantics/proofs                                      3m32s   1GB
May 15 02:09:11 Starting semantics/alt_semantics
May 15 02:09:21 Finished semantics/alt_semantics                                  8s 307MB
May 15 02:09:21 Starting semantics/alt_semantics/proofs
May 15 02:11:33 Finished semantics/alt_semantics/proofs                        2m11s 804MB
May 15 02:11:33 Starting basis/pure
May 15 02:11:56 FAILED: basis/pure
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
Scanning $(CAKEMLDIR)/misc
Starting work on balanced_mapTheory
Starting work on FormalLangTheory
Starting work on charsetTheory
Starting work on vec_mapTheory
FormalLangTheory                                real:    1s  user:    1s     OK
Starting work on README.md
vec_mapTheory                                   real:    1s  user:    1s     OK
Starting work on mllistTheory
README.md                                       real:    0s  user:    0s     OK
Starting work on mloptionTheory
charsetTheory                                   real:   10s  user:    9s     OK
Starting work on regexpTheory
mllistTheory                                    real:    9s  user:    8s     OK
Starting work on mlstringTheory
mloptionTheory                                  real:    9s  user:    8s     OK
mlstringTheory                                  real:    9s  user:    8sFAIL<1>
 Saved theorem _____ "strlen_substring"
 Saved definition __ "extract_def"
 Saved theorem _____ "strlen_extract_le"
 error in quse /home/cake/oven/regression/cakeml-1227/basis/pure/mlstringScript.sml : Fail "Static Errors"
 error in load /home/cake/oven/regression/cakeml-1227/basis/pure/mlstringScript : Fail "Static Errors"
 Saved theorem _____ "strsub_substring_0_thm"
 Saved theorem _____ "substring_full"
 /home/cake/oven/regression/cakeml-1227/basis/pure/mlstringScript.sml:166: error: Value or constructor (DROP_NIL) has not been declared
 Found near [substring_def, DROP_NIL]
 Uncaught exception: Fail "Static Errors"
balanced_mapTheory                                                      M-KILLED
regexpTheory                                                            M-KILLED