Job 1225

CakeML:c836e91226733fa77550b2b46d2cfd6f6b9f632c
  Merge pull request #735 from CakeML/lpr_new [May 13 09:44:58]
HOL:58c4d6875c6c6333705a63dc970bd4a3b0c15342
  emacs-mode: indent after in of let-in; regression test included [May 12 05:51:30]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

May 13 09:50:56 Claimed job
May 13 09:51:06 Building HOL
May 13 10:04:05 Starting developers
May 13 10:04:10 Finished developers                                               4s  79MB
May 13 10:04:10 Starting developers/bin
May 13 10:04:18 Finished developers/bin                                           7s   1GB
May 13 10:04:18 Starting semantics/ffi
May 13 10:04:29 Finished semantics/ffi                                           10s 221MB
May 13 10:04:29 Starting semantics
May 13 10:06:01 Finished semantics                                             1m32s   1GB
May 13 10:06:02 Starting semantics/proofs
May 13 10:09:32 Finished semantics/proofs                                      3m30s   1GB
May 13 10:09:32 Starting semantics/alt_semantics
May 13 10:09:41 Finished semantics/alt_semantics                                  8s 329MB
May 13 10:09:41 Starting semantics/alt_semantics/proofs
May 13 10:11:55 Finished semantics/alt_semantics/proofs                        2m13s 891MB
May 13 10:11:55 Starting basis/pure
May 13 10:12:18 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
vec_mapTheory                                   real:    1s  user:    1s     OK
Starting work on README.md
FormalLangTheory                                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:   10s  user:    9sFAIL<1>
 Saved theorem _____ "strlen_substring"
 Saved definition __ "extract_def"
 Saved theorem _____ "strlen_extract_le"
 Saved theorem _____ "strsub_substring_0_thm"
 error in quse /home/cake/oven/regression/cakeml-1225/basis/pure/mlstringScript.sml : Fail "Static Errors"
 error in load /home/cake/oven/regression/cakeml-1225/basis/pure/mlstringScript : Fail "Static Errors"
 Saved theorem _____ "substring_full"
 /home/cake/oven/regression/cakeml-1225/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