[isabelle] PolyML "Insufficient memory" exception while building images
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] PolyML "Insufficient memory" exception while building images
- From: Thomas Sewell <thomas.sewell at nicta.com.au>
- Date: Fri, 12 Sep 2014 15:56:09 +1000
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.0
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?
Finally, in the past I've noticed that the problem is slightly
nondeterministic. If I delete a few heaps and try again, sometimes the
process succeeds, usually after three or four attempts. This is not a
lot of fun.
Does anyone have any idea what kinds of things might cause this problem,
and where I should be looking? I've noticed that polyML itself has a
number of command-line memory-debugging arguments, and I'm not sure what
will happen if I try to convince Isabelle to pass them along.
I don't set any limits on PolyML's memory usage in my isabelle settings
or via ulimit or similar. (There's a limit on Java's memory consumption,
but that's not what's being hit here.)
Here are the last few ML statistics messages from the log of the failed
And the final few lines:
### Cannot present theory with skipped proofs: "InitLemmas"
### Cannot present theory with skipped proofs: "Invocations_R"
val it = (): unit
ML> Exception- Fail "Insufficient memory" raised
Thanks for your time/thoughts,
This archive was generated by a fusion of
Pipermail (Mailman edition) and