Re: [isabelle] PolyML "Insufficient memory" exception while building images

On 18.09.2014 06:40, Thomas Sewell wrote:
> Thanks David. That is indeed what is going on.
> There's an Isabelle problem here: the suggested approach to executing
> 64-bit polyML does not actually result in 64-bit polyML being run.
> In the Isabelle NEWS file the following is suggested:
> The following example setting prefers 64 bit if available:
> I have in my isabelle settings the line:
> Running isabelle env | grep ML shows these settings:
> ML_IDENTIFIER=polyml-5.5.2_x86_64-linux
> POLYML_HOME=/home/tsewell/.isabelle/contrib/polyml-5.5.2
> ML_SYSTEM=polyml-5.5.2
> ML_PLATFORM=x86_64-linux
> ML_HOME=/home/tsewell/.isabelle/contrib/polyml-5.5.2/x86-linux
> ML_SOURCES=/home/tsewell/.isabelle/contrib/polyml-5.5.2/src
> So, the isabelle environment is now thoroughly confused which version of
> polyML is running, to the extent that my heap files are being saved in a
> directory called "polyml-5.5.2_x86_64-linux" despite the fact that the
> poly process which is running is actually the x86-linux variant.
> In short, that is all a bit confusing. Is there a better way to switch
> between 32 and 64 bit modes? For the moment, I've just moved the
> ~/.isabelle/contrib/polyml-5.2.2/x86-linux directory aside, which
> results in Isabelle falling back to 64-bit mode. Amusingly, polyML then
> objects to the version of the saved heap files.
Indeed, there doesn't seem to be a really clean way.

The etc/settings file of the polyml-5.2.2-1 component automatically
chooses between ISABELLE_PLATFORM32 and 64 by trying to run 32-bit poly
and there is no way of overriding this.

To fully switch to 64-bit poly, you need to set


after initializing the component.
Also, ML_OPTIONS is different for 64-bit mode, so you may want to set

   ML_OPTIONS="-H 1000"


   -- Lars

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