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

[Tobias Nipkow]

This is really phantastic - at last I can build HOL-Analysis on my terrible new 
Mac without having to put it in the freezer and it does not fall over at the 
very end. It is also 20% faster.

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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190125/6a145d6e/attachment.bin>