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:
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