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



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.

Well, enough said. I hope this is easy to fix.

Thanks all,
    Thomas.

On 14/09/14 02:47, David Matthews wrote:
Looking at those figures I would guess that you are running the 32-bit
version of Poly/ML.  I think that is the default for Isabelle because,
generally, it gives better performance than the 64-bit version.  The
problem with it is that the total address space of a 32-bit
application is limited by the operating system to around 3Gbytes.
Poly/ML uses several memory pools and a situation can arise where the
address space limit is reached.  Try it with the 64-bit version and if
it happens there I will try and investigate further.

David

On 12/09/2014 06:56, Thomas Sewell wrote:
Hello isabelle-users.

I've been struggling lately with fairly frequent "Insufficient memory"
exceptions when trying to build heaps/images. The strange thing is that
I don't seem to have run out of memory in any sense.

 From reading the log, it looks a lot like PolyML ran out of something
while trying to do its final cleanup before saving the session. In the
session log, all the theories have been loaded already. There's also
plenty more total memory available on this machine at the time of
failure, so I don't think it's a fail-to-allocate problem. Perhaps
PolyML has exhausted some fixed resource used while doing a
shareCommonData or similar, such as stack space on some thread?
val it = (): unit
ML> Exception- Fail "Insufficient memory" raised


________________________________

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.