Re: [isabelle] isabelle build -vb runs out of store

Hi Peter,

Just a quick guess. Are you running PolyML in 32bit mode and thus hit the 32bit memory wall? Or have you limitted PolyML's maximum heap size with some configuration parameters?

Several years ago, I got that error message frequently when working with JinjaThreads before I switched to 64bit mode. When David Matthews implemented some kind of online sharing in PolyML, I could get JinjaThreads fit back into 32bit heap space. At that time, PG was still officially supported and IIRC it did not terminate the whole Isabelle process. Nowadays, I noted that I can reduce memory consumption by loading less theories in parallel in PG. From what I understand, Isabelle processed theories that are loaded in the background in parallel like jEdit does. Only the currently active theory gets processed incrementally (and slowly) in PG. Hence, you might want to either reduce parallelism with some runtime options or just load theories in smaller chunks.

Hope this helps,

On 11/06/14 14:30, Peter Lammich wrote:
More info on this:
   This message seems to come from PolyML directly. When it happens,
   top tells me I have about 500m of free heap, and lots (6g) of free
   swap space.

The same happens when trying to build in ProofGeneral, it just kills the
whole Isabelle process.


On Mi, 2014-06-11 at 14:15 +0200, Peter Lammich wrote:
When I type
   isabelle build -vbd. ProjectName

it starts the build process as usual, and after some while, it
terminates with the message "Run out of store - interrupting threads":

What runs out of store here, and how can I increase the available store?

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