CakeML:d83742f10a36f76853fc6e0d9de26bfa02ec9f3a
Update HOL_STORE precondition theorem
#511 (argparse)
Merging into:5312faa061cfb56576674791f13d27dc328efdf1
Merge pull request #540 from CakeML/assign-reorg
HOL:e1183800f51cfd469a8048ca65733cd1ac97c87e
Add DISJ_EQ_IMP to boolTheory
Machine:oven1 4.15.9-300.fc27.x86_64 x86_64 GNU/Linux
Claimed job
Building HOL
Starting developers/bin
Finished developers/bin 1m10s 912MB
Starting semantics/ffi
Finished semantics/ffi 38s 647MB
Starting semantics
Finished semantics 1m26s 928MB
Starting semantics/proofs
Finished semantics/proofs 2m42s 1GB
Starting basis/pure
FAILED: basis/pure
]0;Holmake: .]0;Holmake: ~/regression/HOL-e1183800f51cfd469a8048ca65733cd1ac97c87e/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-e1183800f51cfd469a8048ca65733cd1ac97c87e/examples/balanced_bst]0;Holmake: ~/regression/HOL-e1183800f51cfd469a8048ca65733cd1ac97c87e/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-e1183800f51cfd469a8048ca65733cd1ac97c87e/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-e1183800f51cfd469a8048ca65733cd1ac97c87e/examples/formal-languages]0;Holmake: ~/regression/HOL-e1183800f51cfd469a8048ca65733cd1ac97c87e/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
Starting work on FormalLangTheory
FormalLangTheory OK
]0;Holmake: ~/regression/HOL-e1183800f51cfd469a8048ca65733cd1ac97c87e/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-e1183800f51cfd469a8048ca65733cd1ac97c87e/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-e1183800f51cfd469a8048ca65733cd1ac97c87e/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-e1183800f51cfd469a8048ca65733cd1ac97c87e/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ../../misc]0;Holmake: ~/regression/HOL-e1183800f51cfd469a8048ca65733cd1ac97c87e/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-e1183800f51cfd469a8048ca65733cd1ac97c87e/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