Job 533

CakeML:d83742f10a36f76853fc6e0d9de26bfa02ec9f3a
  Update HOL_STORE precondition theorem [Oct 10 20:10:02]
#511 (argparse)
Merging into:eade0f2f7ccfe17bb7042cdc67f8379ff7edd270
  Add OpenTheory compiler proofs to build-sequence [Oct 16 04:15:06]
HOL:5486751385fa6b1f69feee739547ec7e4ef99d7f
  Add files demonstrating problem with interactive use of INCLUDES [Oct 15 23:25:26]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Oct 16 08:00:02 Claimed job
Oct 16 08:00:22 Building HOL
Oct 16 08:09:55 Starting developers/bin
Oct 16 08:11:06 Finished developers/bin                                        1m10s 913MB
Oct 16 08:11:07 Starting semantics/ffi
Oct 16 08:11:48 Finished semantics/ffi                                           40s 372MB
Oct 16 08:11:48 Starting semantics
Oct 16 08:13:22 Finished semantics                                             1m33s 847MB
Oct 16 08:13:23 Starting semantics/proofs
Oct 16 08:16:15 Finished semantics/proofs                                      2m51s   1GB
Oct 16 08:16:15 Starting basis/pure
Oct 16 08:19:03 FAILED: basis/pure
]0;Holmake: .]0;Holmake: ~/oven/regression/HOL-5486751385fa6b1f69feee739547ec7e4ef99d7f/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-5486751385fa6b1f69feee739547ec7e4ef99d7f/examples/balanced_bst]0;Holmake: ~/oven/regression/HOL-5486751385fa6b1f69feee739547ec7e4ef99d7f/examples/balanced_bstWorking in $(HOLDIR)/examples/balanced_bst
Starting work on balanced_mapTheory
balanced_mapTheory                                                           OK
Starting work on osetTheory
osetTheory                                                                   OK
]0;Holmake: ~/oven/regression/HOL-5486751385fa6b1f69feee739547ec7e4ef99d7f/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-5486751385fa6b1f69feee739547ec7e4ef99d7f/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-5486751385fa6b1f69feee739547ec7e4ef99d7f/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
Starting work on FormalLangTheory
FormalLangTheory                                                             OK
]0;Holmake: ~/oven/regression/HOL-5486751385fa6b1f69feee739547ec7e4ef99d7f/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-5486751385fa6b1f69feee739547ec7e4ef99d7f/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
Starting work on charsetTheory
Starting work on eq_cmp_bmapTheory
Starting work on vec_mapTheory
eq_cmp_bmapTheory                                                            OK
vec_mapTheory                                                                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: ~/oven/regression/HOL-5486751385fa6b1f69feee739547ec7e4ef99d7f/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-5486751385fa6b1f69feee739547ec7e4ef99d7f/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../../misc]0;Holmake: ~/oven/regression/HOL-5486751385fa6b1f69feee739547ec7e4ef99d7f/examples/machine-code/hoare-triple]0;Holmake: ~/oven/regression/HOL-5486751385fa6b1f69feee739547ec7e4ef99d7f/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: ../../misc]0;Holmake: ../../developers]0;Holmake: ../../developersWorking in ../../developers
]0;Holmake: ../../misc]0;Holmake: ../../misc/lem_lib_stub]0;Holmake: ../../misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ../../misc]0;Holmake: ../../miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/basis/pure
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