[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.


More information about the isabelle-dev mailing list