CakeML:7600968e23d5d803f06d21605c935db01ea3580c
Make compiler return non-zero exit code on error
#589 (compiler-exit-code)
Merging into:75614126e5170e953dbab330960f90b715bf38b3
Fix to_bvlProg
HOL:89daca206b2ad7a8e43f3a59c20a178cc04d7748
Fix bug: TypeBase.simpls_of not being filled in on load
Machine:oven2 4.13.0-37-generic x86_64 GNU/Linux
Claimed job
Reusing HOL
Starting developers
Finished developers 0s 44MB
Starting developers/bin
Finished developers/bin 39s 201MB
Starting semantics/ffi
Finished semantics/ffi 10s 203MB
Starting semantics
FAILED: semantics
]0;Holmake: .]0;Holmake: ~/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-645/developers]0;Holmake: ~/regression/cakeml-645/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-645/misc]0;Holmake: ~/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/cakeml-645/misc]0;Holmake: ~/regression/cakeml-645/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-645/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-645/misc]0;Holmake: ~/regression/cakeml-645/misc[1mWorking in $(CAKEMLDIR)/misc[0m
Starting work on alist_treeTheory
Starting work on miscTheory
Starting work on README.md
README.md OK
alist_treeTheory OK
miscTheory OK
]0;Holmake: .]0;Holmake: ffi]0;Holmake: ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/semantics[0m
Starting work on addancs
Starting work on fpSemScript
Starting work on README.md
README.md OK
addancs OK
Starting work on astScript
Starting work on namespaceScript
Starting work on tokensScript
tokensScript OK
Starting work on tokensTheory
namespaceScript OK
Starting work on namespaceTheory
astScript OK
namespaceTheory FAILED! <1>
error in quse /home/myreen/regression/cakeml-645/semantics/namespaceScript.sml : HOL_ERR {message = "unsatisfied predicate", origin_function = "first", origin_structure = "Lib"}
error in load namespaceScript : HOL_ERR {message = "unsatisfied predicate", origin_function = "first", origin_structure = "Lib"}
<<HOL message: Created theory "namespace">>
Uncaught exception: HOL_ERR {message = "unsatisfied predicate", origin_function = "first", origin_structure = "Lib"}
fpSemScript M-KILLED
tokensTheory M-KILLED