Job 882

CakeML:4ded65ad3479759c5274f28017b05ecf9300c189
  Move more theorems to HOL [May 15 03:51:13]
#653 (cleanup)
Merging into:c3cbbfd27bd9e1f2836f8f307279178dc76ac571
  Merge pull request #650 from CakeML/tweak-how-to [May 17 12:31:32]
HOL:f6c660ddb3151f18cd07b606f2439087858abe20
  Further polish Definition documentation (incl. schematic attribute) [May 16 14:38:46]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

May 17 12:40:20 Claimed job
May 17 12:41:04 Building HOL
May 17 12:50:22 Starting developers
May 17 12:50:25 Finished developers                                               2s  21MB
May 17 12:50:25 Starting developers/bin
May 17 12:51:42 Finished developers/bin                                        1m16s 919MB
May 17 12:51:42 Starting semantics/ffi
May 17 12:52:20 Finished semantics/ffi                                           37s 516MB
May 17 12:52:21 Starting semantics
May 17 12:52:37 FAILED: semantics
]0;Holmake: .]0;Holmake: ~/oven/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Starting work on lprefix_lubTheory
lprefix_lubTheory                                                            OK
]0;Holmake: .]0;Holmake: ~/oven/regression/cakeml-882/developers]0;Holmake: ~/oven/regression/cakeml-882/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: .]0;Holmake: ~/oven/regression/cakeml-882/misc]0;Holmake: ~/oven/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/machine-code/hoare-triple]0;Holmake: ~/oven/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
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: ~/oven/regression/cakeml-882/misc]0;Holmake: ~/oven/regression/cakeml-882/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-882/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ~/oven/regression/cakeml-882/misc]0;Holmake: ~/oven/regression/cakeml-882/miscWorking in $(CAKEMLDIR)/misc
Holdep failed: miscScript.sml 2995.2 Bad character >[< after open
Holmake failed with exception: HolDepFailed
Raised from: /home/cake/oven/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/tools/Holmake/Holmake_tools.sml: 637:0 - 637:0