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



On Thu, 18 Sep 2014, Thomas Sewell wrote:

There's an Isabelle problem here

So, the isabelle environment is now thoroughly confused which version of
polyML is running

I hope this is easy to fix.

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

It seems that some more basic Isabelle education is required. As usual there are two approaches: to work with the system, or to work against it.

Working with the system means to look around carefully how things are usually done, under the assumption that the system is mostly right. Concerning settings the "system" manual also has a lot to say -- here it needs to be read in the context of Isabelle component settings in particular.

Taking a NEWS entry from 2010 in isolation is unlikely to succeed, without its historical context. In the past there were no Isabelle components and people usually had the full bunch of ML settings somewhere. Then it was
obvious what the change of a single line line ML_PLATFORM="..." meant.

Today in Isabelle2014, the component polyml-5.5.2-1/etc/settings still make it possible to work like that, taking the with a commented-out section of "basic settings" as a starting point:

  ML_SYSTEM=polyml-5.5.2
  ML_PLATFORM="$ISABELLE_PLATFORM32"
  ML_HOME="$POLYML_HOME/$ML_PLATFORM"
  ML_OPTIONS="-H 500"
  ML_SOURCES="$POLYML_HOME/src"

Applying some care and common-sense, it should be obvious who to work with that, without any need to "fix" Isabelle, nor to "sabotage" anything.


	Makarius




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