Great work! Tobias
On 19/01/2019 21:43, Makarius wrote:
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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
