Job 539

CakeML:d83742f10a36f76853fc6e0d9de26bfa02ec9f3a
  Update HOL_STORE precondition theorem [Oct 10 20:10:02]
#511 (argparse)
Merging into:9620f70b0670e4f259ccd3b25a8efc9ed574bd50
  Put semantics/proofs into characteristic's INCLUDES [Oct 19 02:15:09]
HOL:1b4a5d5506b74451f62ba916ec8e07ecac2aad6a
  Merge pull request #603 from thtuerk/fix_pattern_match_demo [Oct 17 23:30:26]
Machine:oven1 4.15.9-300.fc27.x86_64 x86_64 GNU/Linux

Oct 19 07:23:43 Claimed job
Oct 19 07:23:50 Reusing HOL
Oct 19 07:32:47 Starting developers/bin
Oct 19 07:33:57 Finished developers/bin                                        1m09s 913MB
Oct 19 07:33:58 Starting semantics/ffi
Oct 19 07:34:37 Finished semantics/ffi                                           38s 362MB
Oct 19 07:34:38 Starting semantics
Oct 19 07:36:05 Finished semantics                                             1m26s 808MB
Oct 19 07:36:05 Starting semantics/proofs
Oct 19 07:38:50 Finished semantics/proofs                                      2m43s   1GB
Oct 19 07:38:50 Starting basis/pure
Oct 19 07:41:33 FAILED: basis/pure
]0;Holmake: .]0;Holmake: ~/regression/HOL-1b4a5d5506b74451f62ba916ec8e07ecac2aad6a/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-1b4a5d5506b74451f62ba916ec8e07ecac2aad6a/examples/balanced_bst]0;Holmake: ~/regression/HOL-1b4a5d5506b74451f62ba916ec8e07ecac2aad6a/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
Starting work on balanced_mapTheory
balanced_mapTheory                                                                                                                                                                                                                                                                       OK
Starting work on osetTheory
osetTheory                                                                                                                                                                                                                                                                               OK
]0;Holmake: ~/regression/HOL-1b4a5d5506b74451f62ba916ec8e07ecac2aad6a/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-1b4a5d5506b74451f62ba916ec8e07ecac2aad6a/examples/formal-languages]0;Holmake: ~/regression/HOL-1b4a5d5506b74451f62ba916ec8e07ecac2aad6a/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
Starting work on FormalLangTheory
FormalLangTheory                                                                                                                                                                                                                                                                         OK
]0;Holmake: ~/regression/HOL-1b4a5d5506b74451f62ba916ec8e07ecac2aad6a/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-1b4a5d5506b74451f62ba916ec8e07ecac2aad6a/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
Starting work on charsetTheory
Starting work on eq_cmp_bmapTheory
Starting work on vec_mapTheory
vec_mapTheory                                                                                                                                                                                                                                                                            OK
eq_cmp_bmapTheory                                                                                                                                                                                                                                                                        OK
charsetTheory                                                                                                                                                                                                                                                                            OK
Starting work on regexpTheory
regexpTheory                                                                                                                                                                                                                                                                             OK
Starting work on regexp_compilerTheory
Starting work on regexp_parserTheory
regexp_parserTheory                                                                                                                                                                                                                                                                      OK
regexp_compilerTheory                                                                                                                                                                                                                                                                    OK
Starting work on regexp2dfa
regexp2dfa                                                                                                                                                                                                                                                                               OK
]0;Holmake: .]0;Holmake: ../../misc]0;Holmake: ~/regression/HOL-1b4a5d5506b74451f62ba916ec8e07ecac2aad6a/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-1b4a5d5506b74451f62ba916ec8e07ecac2aad6a/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ../../misc]0;Holmake: ~/regression/HOL-1b4a5d5506b74451f62ba916ec8e07ecac2aad6a/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-1b4a5d5506b74451f62ba916ec8e07ecac2aad6a/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ../../misc]0;Holmake: ../../developers]0;Holmake: ../../developers[1mWorking in ../../developers[0m
]0;Holmake: ../../misc]0;Holmake: ../../misc/lem_lib_stub]0;Holmake: ../../misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ../../misc]0;Holmake: ../../misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/basis/pure[0m
Starting work on mllistTheory
Starting work on mloptionTheory
Starting work on README.md
README.md                                                                                                                                                                                                                                                                       FAILED! <1>
 ERROR! readme_gen.sml cannot produce README.md due to:
 ArgParseScript.sml: file must start with (*
mllistTheory                                                                                                                                                                                                                                                                       M-KILLED
mloptionTheory                                                                                                                                                                                                                                                                     M-KILLED