[isabelle-dev] Poly/ML x86_64_32 available for testing

[Makarius]

Thanks to great work by David Matthews, there is now an Isabelle
component polyml-test-0a6ebca445fc (Isabelle/3b777286c3ec), which can be
enabled manually, e.g. in $ISABELLE_HOME_USER/etc/settings like this:

  init_component "$HOME/.isabelle/contrib/polyml-test-0a6ebca445fc"

It requires the usual "isabelle components -a" incantation afterwards.


This supports 3 platform variants:

  x86
  x86_64
  x86_64_32

x86 is still there for comparison, but will disappear soon.

x86_64 is the full 64-bit model as before, and subject to the system
option "ML_system_64 = true".

x86_64_32 is the default. It is a synthesis of the x86_64 architecture
(more memory, more registers etc.) with a 32-bit value model for ML.
Thus we get approx. 5 times more memory as in x86, without the penalty
of full 64-bit values.

Moreover, we have a proper "64-bit application" according to Apple (and
Linux distributions): it is getting increasingly hard to run old x86
executables, and soon it might be hardly possible at all. In other
words, Poly/ML is now getting ready for many more years to come.


The above component already works smoothly for all of Isabelle + AFP,
only with spurious drop-outs that can happen rarely. x86_64_32 is
already more stable than x86, which often suffers from out-of-memory
situations.


So this is the right time for further testing of applications:
Isabelle2018 should work as well, but I have not done any testing beyond
"isabelle build -g main" -- Isabelle development only moves forward in
one direction on a single branch.

For really big applications, it might occasionally help to use something
like "--maxheap 8g" in ML_OPTIONS: the implicit maximum is 16g, which is
sometimes too much for many parallel jobs on mid-range hardware. There
are additional memory requirements outside the ML heap, for program code
and stacks.


	Makarius