Overview

Job 889

CakeML:4ded65ad3479759c5274f28017b05ecf9300c189
  Move more theorems to HOL
#653 (cleanup)
Merging into:c3cbbfd27bd9e1f2836f8f307279178dc76ac571
  Merge pull request #650 from CakeML/tweak-how-to
HOL:15a1e85b5308eeb3ca329cafe2c409f1fd21edfd
  Fix Holmake regressions arising from b03aecf7b
Machine:brain12 4.14.89.1.amd64-smp x86_64 GNU/Linux

 Claimed job
 Building HOL
 Starting developers
 Finished developers                                               2s  36MB
 Starting developers/bin
 Finished developers/bin                                           9s 929MB
 Starting semantics/ffi
 Finished semantics/ffi                                         1m15s 845MB
 Starting semantics
 FAILED: semantics
]0;Holmake: .]0;Holmake: /local/hbecker/regression/HOL-15a1e85b5308eeb3ca329cafe2c409f1fd21edfd/examples/fun-op-sem/lprefix_lub]0;Holmake: /local/hbecker/regression/HOL-15a1e85b5308eeb3ca329cafe2c409f1fd21edfd/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: /local/hbecker/regression/cakeml-889/developers]0;Holmake: /local/hbecker/regression/cakeml-889/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: .]0;Holmake: /local/hbecker/regression/cakeml-889/misc]0;Holmake: /local/hbecker/regression/HOL-15a1e85b5308eeb3ca329cafe2c409f1fd21edfd/examples/machine-code/hoare-triple]0;Holmake: /local/hbecker/regression/HOL-15a1e85b5308eeb3ca329cafe2c409f1fd21edfd/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: /local/hbecker/regression/cakeml-889/misc]0;Holmake: /local/hbecker/regression/cakeml-889/misc/lem_lib_stub]0;Holmake: /local/hbecker/regression/cakeml-889/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: /local/hbecker/regression/cakeml-889/misc]0;Holmake: /local/hbecker/regression/cakeml-889/miscWorking in $(CAKEMLDIR)/misc
Holdep failed: miscScript.sml 2995.2 Bad character >[< after open
Holmake failed with exception: HolDepFailed
Raised from: /local/hbecker/regression/HOL-15a1e85b5308eeb3ca329cafe2c409f1fd21edfd/tools/Holmake/Holmake_tools.sml: 637:0 - 637:0