[isabelle-dev] NEWS: standard heap images

Makarius makarius at sketis.net
Wed Apr 10 16:57:31 CEST 2019


*** Isabelle/jEdit Prover IDE ***

* The Isabelle/jEdit desktop application uses the same options as
"isabelle jedit" for its internal "isabelle build" process: the implicit
option "-o system_heaps" (or "-s") has been discontinued. This reduces
the potential for surprise wrt. command-line tools.

* The official download of the Isabelle/jEdit application already
contains heap images for Isabelle/HOL within its main directory: thus
the first encounter becomes faster and more robust (e.g. when run from a
read-only directory).


This refers to Isabelle/eadd87383e30.

Pre-built heap images have become possible for a variety of reasons:
predictable ML platform even on Linux (x86_64_32), proper
Admin/build_release in Isabelle/Scala with its on-board ssh library etc.

The downloads are now slightly bigger (400MB), but overall more robust
-- especially on first encounter with Isabelle. On recent macOS the
Isabelle.app even works the special read-only mount provided by Apple
after unpacking within the Downloads directory.


Note: The heap images do contain a funny directory location from the
build process, but this is subsequently unused by Isabelle/Scala
invoking Poly/ML. The images are relocatable as usual.


	Makarius



More information about the isabelle-dev mailing list