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