Re: [isabelle] isabelle build -vb runs out of store
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
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