[isabelle-dev] Towards Poly/ML 5.8

[Makarius]

After a lot of refinements by David Matthews we are moving towards the
new Poly/ML 5.8 release. Isabelle/8c587dd44f51 already bundles a Poly/ML
version of that number, without being official yet. The Isabelle NEWS
already talk about an official release:


*** System ***

* 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 version also discontinues compatibility with Poly/ML 5.7.x, i.e.
Isabelle2018 will not work with it, but polyml-test-8fda4fd22441 can
still be used for that.

I have also omitted old x86 from the bundle: it is difficult to build
and run on current systems and much less stable than the new default
x86_64_32. A minor disadvantage is that old hardware with only 4 GB will
be somewhat slower, but we de-facto require 8 GB already.

Everything in Isabelle + AFP should work with x86_64_32 on all platforms
-- further automated and manual tests are running (some on old hardware
with only 3 or 5 GB per CPU node, e.g. see
https://isabelle.sketis.net/devel/build_status/AFP/index.html).

Full x86_64 with 64-bit values/addresses is not required for anything in
the visible universe of Isabelle + AFP. The "large" group runs
considerably faster in full 64-bit mode, but this is not an existential
problem for x86_64_32: a full "build -a" will be usually faster with
x86_64_32 (and require much less resources).


	Makarius