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_OPTIONS=-H 500
> 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
This archive was generated by a fusion of
Pipermail (Mailman edition) and