Job 1224

CakeML:e593088bf68375cf78d006ae9d7819e9c7ad873c
  Pretty print dataLang code into file for cost examples [Apr 27 09:41:00]
HOL:58c4d6875c6c6333705a63dc970bd4a3b0c15342
  emacs-mode: indent after in of let-in; regression test included [May 12 05:51:30]
Machine:stove 4.15.0-55-generic x86_64 GNU/Linux

May 13 02:37:50 Claimed job
May 13 02:37:57 Building HOL
May 13 02:50:04 Starting developers
May 13 02:50:08 Finished developers                                               4s 140MB
May 13 02:50:08 Starting developers/bin
May 13 02:50:15 Finished developers/bin                                           7s   1GB
May 13 02:50:15 Starting semantics/ffi
May 13 02:50:25 Finished semantics/ffi                                            9s 244MB
May 13 02:50:25 Starting semantics
May 13 02:51:52 Finished semantics                                             1m26s   1GB
May 13 02:51:52 Starting semantics/proofs
May 13 02:55:03 Finished semantics/proofs                                      3m11s   1GB
May 13 02:55:03 Starting semantics/alt_semantics
May 13 02:55:11 Finished semantics/alt_semantics                                  7s 330MB
May 13 02:55:11 Starting semantics/alt_semantics/proofs
May 13 02:57:13 Finished semantics/alt_semantics/proofs                        2m02s 732MB
May 13 02:57:14 Starting basis/pure
May 13 02:57:35 FAILED: basis/pure
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
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:    8s  user:    8s     OK
Starting work on regexpTheory
mloptionTheory                                  real:    8s  user:    7s     OK
mllistTheory                                    real:    8s  user:    8s     OK
Starting work on mlstringTheory
mlstringTheory                                  real:    9s  user:    8sFAIL<1>
 Saved theorem _____ "strlen_substring"
 Saved definition __ "extract_def"
 Saved theorem _____ "strlen_extract_le"
 error in quse /home/cur/sao/cakeml/regression/cakeml-1224/basis/pure/mlstringScript.sml : Fail "Static Errors"
 error in load /home/cur/sao/cakeml/regression/cakeml-1224/basis/pure/mlstringScript : Fail "Static Errors"
 Saved theorem _____ "strsub_substring_0_thm"
 Saved theorem _____ "substring_full"
 /home/cur/sao/cakeml/regression/cakeml-1224/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