Overview

Job 878

CakeML:4ded65ad3479759c5274f28017b05ecf9300c189
  Move more theorems to HOL
#653 (cleanup)
Merging into:8f8560b3414274dcffa62719ba224df92d8cb039
  Merge pull request #651 from talsewell/translator_messages
HOL:f6c660ddb3151f18cd07b606f2439087858abe20
  Further polish Definition documentation (incl. schematic attribute)
Machine:te1

 Claimed job
 Building HOL
 Starting developers
 Finished developers                                               2s  32MB
 Starting developers/bin
 Finished developers/bin                                           6s 927MB
 Starting semantics/ffi
 Finished semantics/ffi                                           54s 630MB
 Starting semantics
 FAILED: semantics
]0;Holmake: .]0;Holmake: ~/regression-worker/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression-worker/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-worker/cakeml-878/developers]0;Holmake: ~/regression-worker/cakeml-878/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: .]0;Holmake: ~/regression-worker/cakeml-878/misc]0;Holmake: ~/regression-worker/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/machine-code/hoare-triple]0;Holmake: ~/regression-worker/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-worker/cakeml-878/misc]0;Holmake: ~/regression-worker/cakeml-878/misc/lem_lib_stub]0;Holmake: ~/regression-worker/cakeml-878/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression-worker/cakeml-878/misc]0;Holmake: ~/regression-worker/cakeml-878/misc[1mWorking in $(CAKEMLDIR)/misc[0m
Holdep failed: miscScript.sml 2995.2 Bad character >[< after open
Holmake failed with exception: HolDepFailed
Raised from: /usr/local/google/home/ramanakumar/regression-worker/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/tools/Holmake/Holmake_tools.sml: 637:0 - 637:0