Re: [isabelle] Isabelle2019-RC2 Does poly really honor --maxheap?

On 24/05/2019 01:04, Eugene W. Stark wrote:
> This might not be new to Isabelle2019-RC2, but I thought that I had set a limit
> on the size of the ML heap, but it is still exceeding that and sending my system
> into thrashing mode.

There have been significant changes in Poly/ML in the latest releases,
changing the game each time:

  * Isabelle2019: Poly/ML 5.8
  * Isabelle2018: Poly/ML 5.7
  * Isabelle2017: Poly/ML 5.6

The relevant NEWS entry for Isabelle2019 is:

* Update to 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.

> Contents of my ~/.isabelle/Isabelle2019-RC2/etc/settings
> ML_HOME="${POLYML_HOME}/x86_64-linux"
> ML_OPTIONS="--maxheap 12000"

That setup looks fairly old-fashioned, and is obsolete in Isabelle2019.
The default x86_64_32 platform allows 16GB ML heap, and x86_64 only
makes sense for something like 32-64 GB.

If you remove all these accumulated settings, it should work fine.

> ps output showing poly with --maxheap option applied:
> gene     18897 75.2 71.7 23475004 17680688 ?   Ssl  May21 2365:39
> /opt/Isabelle2019-RC2/contrib/polyml-5.8/x86_64-linux/poly -q --maxheap 12000 --gcthreads 0 --eval
> (PolyML.SaveState.loadHierarchy ["/home/gene/.isabelle/Isabelle2019-RC2/heaps/polyml-5.8_x86_64-linux/Pure",
> Output from "top":
> 18897 gene      20   0 22.372g 0.016t   6104 S 127.9 71.6   2367:46 poly

I see 16GB resident memory here, which is sufficiently close to the
specified 12GB to hold up the claim that poly manages its memory
correctly: there can be more things outside of the ML heap, e.g.
generated code and stacks.

It is up to David Matthews to explain further details.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.