Re: [isabelle] Insufficient memory when building heap image

On Fri, 28 Sep 2012, Manuel Eberl wrote:

Also, if I load all these theories by hand by importing them in a theory and loading that theory in Proof General, everything seems to work, but when I do "isabelle usedir" with an appropriate ROOT.ML file, I get this insufficient memory exception.

Traditionally, Proof General runs things with slightly different options, such as quick_and_dirty and reduced parallel proof checking, so there can be easily a difference to batch mode.

I am trying hard not to repeat these mistakes and consequent confusion in the current interactive document model, the one that is used for Isabelle/jEdit. So after a few more rounds of refinements, and when Proof General is forgotten, such issues should no longer occur.

The reason for that is that, apparently, "Isabelle usedir" uses up to 6.5 GiB of memory (tested on a 64 bit system), but the computer with which I normally work runs a 32 bit system, so I only have 4 GiB per process.

You need to find out where the resources are going, i.e. which part of your application burns them. You may try this in plain "isabelle tty" which is a bit closer to batch mode than the Proof General interaction mode.

Alternatively, you can ignore the problem and use current polyml-5.5.0 from here:

This is the brand-new Poly/ML release, with greatly improved heap management (parallel garbage collection and online sharing of values).
It is able to run much larger Isabelle applications even in 32bit mode.

To use the above polyml-5.5.0 component in Isabelle2012, add something like this to your $ISABELLE_HOME_USER/etc/settings:

  ML_OPTIONS="-H 500"

Then rebuild the required images as usual via Isabelle2012/build.


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