Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2019-RC2 Does poly really honor --maxh...

Email Gateway (Aug 22 2022 at 19:42):

From: Makarius <makarius@sketis.net>
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

ISABELLE_PLATFORM="${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"
ML_PLATFORM="${ISABELLE_PLATFORM}"
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":

PID USER PR NI VIRT RES SHR S %CPU %MEM TIME+ COMMAND

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.

Makarius

Last updated: Apr 26 2024 at 12:28 UTC