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
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:
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and