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

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.


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

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