[isabelle-dev] NEWS: Update to Poly/ML 5.8 -- and towards Isabelle2019

Makarius makarius at sketis.net
Tue Mar 12 16:36:08 CET 2019


*** System ***

* Update to Poly/ML 5.8 allows to use the native x86_64 platform without
the full overhead of 64-bit values everywhere. This special x86_64_32
mode provides up to 16GB ML heap, while program code and stacks are
allocated elsewhere. Thus approx. 5 times more memory is available for
applications compared to old x86 mode (which is no longer used by
Isabelle). The switch to the x86_64 CPU architecture also avoids
compatibility problems with Linux and macOS, where 32-bit applications
are gradually phased out.


This refers to Isabelle/63721ee8c86c, it is now the official release of
Poly/ML 5.8 by David Matthews.

It all looks great so far, and there is still plenty of time for further
testing until the official release of Isabelle2019.

The present plan is to publish an unofficial Isabelle2019-RC0 snapshot
in early April, and start officially with Isabelle2019-RC1 at the
beginning of May. It all should be finalized an published until
15-Jun-2019, when I will go on travel (not vacation, but a visit to
colleagues in Paris).


	Makarius


More information about the isabelle-dev mailing list