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

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

Thanks Lars.

OK, so I've learned a lot from this. Apparently the order of the
"init_components" line with respect to the other lines of the settings
file matters quite a lot.

The polyml component currently overrules any settings that were
previously set, and then sets quite a few settings of its own. The
missing "clean" approach would probably involve requesting 64-bit mode
before the component initialises, and having the component notice this
has been done.

To override the settings after the component has initialised, you must
override all the settings it set, but there's no obvious way to ask what
they were. Perhaps in the past it was sufficient to adjust ML_PLATFORM.

To confuse matters, further settings (environment variables) seem to be
updated after the end of the user's settings file. For instance,
adjusting ML_PLATFORM seems to imply an update to ML_IDENTIFIER, but not
to ML_HOME or POLYML_HOME, thus the confusing outcome.

Well, I now know a lot more about how this works. However, I'm going to
continue enabling 64-bit mode by sabotaging 32-bit mode until someone
suggests a significantly better way.

Thanks for educating me,


The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

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