[isabelle] Insufficient memory when building heap image
- To: isabelle-users at cl.cam.ac.uk
- Subject: [isabelle] Insufficient memory when building heap image
- From: Manuel Eberl <eberlm at in.tum.de>
- Date: Fri, 28 Sep 2012 15:47:06 +0200
- User-agent: Mozilla/5.0 (X11; Linux i686; rv:15.0) Gecko/20120827 Thunderbird/15.0
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and