Job 1223

CakeML:7cc0a8fa5dae7940bfd10658044739e9aa70cf0d
  array proof update [Apr 29 12:46:55]
#735 (lpr_new)
Merging into: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:oven3 4.19.67.1.amd64-smp

May 13 02:37:33 Claimed job
May 13 02:37:47 Building HOL
May 13 03:03:53 Starting developers
May 13 03:04:00 Finished developers                                               7s 123MB
May 13 03:04:01 Starting developers/bin
May 13 03:04:16 Finished developers/bin                                          15s   1GB
May 13 03:04:17 Starting semantics/ffi
May 13 03:04:39 Finished semantics/ffi                                           22s 264MB
May 13 03:04:40 Starting semantics
May 13 03:07:37 Finished semantics                                             2m57s 927MB
May 13 03:07:37 Starting semantics/proofs
May 13 03:14:46 Finished semantics/proofs                                      7m07s   1GB
May 13 03:14:46 Starting semantics/alt_semantics
May 13 03:15:05 Finished semantics/alt_semantics                                 19s 300MB
May 13 03:15:06 Starting semantics/alt_semantics/proofs
May 13 03:19:32 Finished semantics/alt_semantics/proofs                        4m26s   1GB
May 13 03:19:32 Starting basis/pure
May 13 03:20:17 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:    3s  user:    2s     OK
Starting work on README.md
vec_mapTheory                                                                                                                                                 real:    3s  user:    3s     OK
Starting work on mllistTheory
README.md                                                                                                                                                     real:    0s  user:    0s     OK
Starting work on mloptionTheory
charsetTheory                                                                                                                                                 real:   19s  user:   18s     OK
Starting work on regexpTheory
mllistTheory                                                                                                                                                  real:   19s  user:   17s     OK
mloptionTheory                                                                                                                                                real:   19s  user:   17s     OK
Starting work on mlstringTheory
mlstringTheory                                                                                                                                                real:   19s  user:   17sFAIL<1>
 Saved theorem _____ "strlen_substring"
 Saved definition __ "extract_def"
 Saved theorem _____ "strlen_extract_le"
 error in quse /root/regression/cakeml-1223/basis/pure/mlstringScript.sml : Fail "Static Errors"
 error in load /root/regression/cakeml-1223/basis/pure/mlstringScript : Fail "Static Errors"
 Saved theorem _____ "strsub_substring_0_thm"
 Saved theorem _____ "substring_full"
 /root/regression/cakeml-1223/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