[isabelle] Insufficient memory when building heap image



Hallo,

I tried to build a heap image with "isabelle usedir", and the programme
completed - apparently successfully - but the heap image was nowhere to
be found. I then looked at the log file in the ~/.isabelle/ directory
and it turns out PolyML threw an "Insufficient Memory" exception and died.

Would it be possible to have Isabelle display an error message in these
cases so that the user knows something went wrong?


Also, if I load all these theories by hand by importing them in a theory
and loading that theory in Proof General, everything seems to work, but
when I do "isabelle usedir" with an appropriate ROOT.ML file, I get this
insufficient memory exception. The reason for that is that, apparently,
"Isabelle usedir" uses up to 6.5 GiB of memory (tested on a 64 bit
system), but the computer with which I normally work runs a 32 bit
system, so I only have 4 GiB per process.

What is the reason for this huge memory usage compared to the more
moderate requirements of loading the theories with Proof General? Is
there some workaround to build this heap image on a 32 bit system?


Cheers,
Manuel





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