CakeML:45b1619f37337d72ec309252e0e4c5351906545c
Fit patLang semantics for FMA
#633 (FMA_support)
Merging into:8f8560b3414274dcffa62719ba224df92d8cb039
Merge pull request #651 from talsewell/translator_messages
HOL:f6c660ddb3151f18cd07b606f2439087858abe20
Further polish Definition documentation (incl. schematic attribute)
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux
Claimed job
Building HOL
Starting developers
Finished developers 0s 22MB
Starting developers/bin
Finished developers/bin 2s 144MB
Starting semantics/ffi
Finished semantics/ffi 32s 517MB
Starting semantics
FAILED: semantics
]0;Holmake: .]0;Holmake: ~/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Starting work on lprefix_lubTheory
lprefix_lubTheory OK
]0;Holmake: .]0;Holmake: ~/regression/cakeml-876/developers]0;Holmake: ~/regression/cakeml-876/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-876/misc]0;Holmake: ~/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
Starting work on set_sepTheory
Starting work on tailrecTheory
tailrecTheory OK
set_sepTheory OK
Starting work on progTheory
progTheory OK
Starting work on addressTheory
Starting work on temporalTheory
temporalTheory OK
addressTheory OK
]0;Holmake: ~/regression/cakeml-876/misc]0;Holmake: ~/regression/cakeml-876/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-876/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-876/misc]0;Holmake: ~/regression/cakeml-876/misc[1mWorking in $(CAKEMLDIR)/misc[0m
Holdep failed: miscScript.sml 3110.2 Bad character >[< after open
Holmake failed with exception: HolDepFailed