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:
>
>   ML_PLATFORM="${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"
>
> I have in my isabelle settings the line:
>
> ML_PLATFORM="$ISABELLE_PLATFORM64"
>
> 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_OPTIONS=-H 500
> ISABELLE_POLYML=true
> 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

   ML_PLATFORM=$ISABELLE_PLATFORM64
   ML_HOME=$POLYML_HOME/$ML_PLATFORM"

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

   ML_OPTIONS="-H 1000"

too.

   -- Lars




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