CakeML:289880182b8bf5cc04dd7efcbd9c9c5025be89f7
Bugfix in EVAL setup in ml_progLib changes.
#595 (local)
Merging into:6669d99667b1f4dbb60de32048f97f611277f41e
Remove unused parsing gitignore
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 30MB
Starting developers/bin
Finished developers/bin 34s 140MB
Starting semantics/ffi
Finished semantics/ffi 8s 217MB
Starting semantics
Finished semantics 1m21s 1GB
Starting semantics/proofs
Finished semantics/proofs 3m24s 1GB
Starting basis/pure
Finished basis/pure 51s 923MB
Starting translator
Finished translator 1m41s 1GB
Starting compiler/parsing
Finished compiler/parsing 1m05s 1GB
Starting characteristic
FAILED: characteristic
]0;Holmake: .]0;Holmake: ~/regression/cakeml-657/basis/pure]0;Holmake: ~/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/balanced_bst]0;Holmake: ~/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/formal-languages]0;Holmake: ~/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/regression/cakeml-657/basis/pure]0;Holmake: ~/regression/cakeml-657/misc]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: ~/regression/cakeml-657/misc]0;Holmake: ~/regression/cakeml-657/developers]0;Holmake: ~/regression/cakeml-657/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-657/misc]0;Holmake: ~/regression/cakeml-657/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-657/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-657/misc]0;Holmake: ~/regression/cakeml-657/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-657/basis/pure]0;Holmake: ~/regression/cakeml-657/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-657/compiler/parsing]0;Holmake: ~/regression/cakeml-657/semantics]0;Holmake: ~/regression/cakeml-657/semantics/ffi]0;Holmake: ~/regression/cakeml-657/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-657/semantics]0;Holmake: ~/regression/cakeml-657/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-657/compiler/parsing]0;Holmake: ~/regression/cakeml-657/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-657/semantics/proofs]0;Holmake: ~/regression/cakeml-657/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-657/translator]0;Holmake: ~/regression/cakeml-657/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/characteristic[0m
Starting work on cfFFITypeTheory
Starting work on README.md
README.md OK
cfFFITypeTheory OK
Starting work on cfHeapsBaseTheory
cfHeapsBaseTheory OK
Starting work on cfHeapsTheory
cfHeapsTheory OK
Starting work on cfStoreTheory
cfStoreTheory OK
Starting work on cfNormaliseTheory
cfNormaliseTheory OK
Starting work on cfAppTheory
cfAppTheory OK
Starting work on cfTheory
cfTheory OK
Starting work on cfTacticsTheory
cfTacticsTheory OK
Starting work on cfLetAutoTheory
Starting work on cfMainTheory
cfMainTheory FAILED! <1>
<<HOL message: Created theory "cfMain">>
error in quse /home/myreen/regression/cakeml-657/characteristic/cfMainScript.sml : HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}
error in load cfMainScript : HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}
Uncaught exception: HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}
cfLetAutoTheory M-KILLED