OverviewCakeML:4ded65ad3479759c5274f28017b05ecf9300c189
Move more theorems to HOL
#653 (cleanup)
Merging into:8f8560b3414274dcffa62719ba224df92d8cb039
Merge pull request #651 from talsewell/translator_messages
HOL:1557f72fc9a7a80bc5ce2e4df30afd51803c8b75
Get formal-languages/regular to pass src tests again
Machine:te1
Claimed job
Reusing HOL
Starting developers
Finished developers 2s 37MB
Starting developers/bin
Finished developers/bin 6s 924MB
Starting semantics/ffi
Finished semantics/ffi 14s 248MB
Starting semantics
FAILED: semantics
]0;Holmake: .]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: .]0;Holmake: ~/regression-worker/cakeml-875/developers]0;Holmake: ~/regression-worker/cakeml-875/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: .]0;Holmake: ~/regression-worker/cakeml-875/misc]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/machine-code/hoare-triple]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression-worker/cakeml-875/misc]0;Holmake: ~/regression-worker/cakeml-875/misc/lem_lib_stub]0;Holmake: ~/regression-worker/cakeml-875/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression-worker/cakeml-875/misc]0;Holmake: ~/regression-worker/cakeml-875/misc[1mWorking in $(CAKEMLDIR)/misc[0m
Starting work on byteTheory
Starting work on README.md
README.md OK
byteTheory OK
Starting work on miscTheory
miscTheory FAILED! <1>
Found near
(fn q => fn ... => ...)
[
QUOTE
" (*#loc 2955 4*)byte_align a \226\136\136 dm \226\136\167\n (dm = { w | low <=+ w \226\136\167 w <+ hi }) \226\136\167\n byte_aligned low \226\136\167 byte_aligned hi \226\135\146\n a \226\136\136 dm"
]
(
... ?? ... \\ ... ... \\ fs [...] \\ asm_exists_tac \\
fs [alignmentTheory.byte_align_def])
Uncaught exception: Fail "Static Errors"
]0;Holmake: .