[isabelle-dev] NEWS: isabelle_process and isabelle console
Makarius
makarius at sketis.net
Sat Mar 5 23:08:20 CET 2016
*** System ***
* Command-line tool "isabelle_process" no longer supports writable heap
images. INCOMPATIBILITY in exotic situations where "isabelle build"
cannot be used: the structure ML_Heap provides operations to save the ML
heap under program control.
* Command-line tool "isabelle_process" supports ML evaluation of literal
expressions (option -e) or files (option -f). Errors lead to premature
exit of the ML process with return code 1.
* Command-line tool "isabelle console -r" helps to bootstrap
Isabelle/Pure interactively.
* SML/NJ and old versions of Poly/ML are no longer supported.
This refers e.g. to Isabelle/0c9081056829.
The discontinuation of SML/NJ and old Poly/ML versions means that we can
now use more up-to-date ways to manage the poly process. A bit more is
coming later.
Makarius
More information about the isabelle-dev
mailing list