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?
Not that I know of. PolyML should run in 64bit mode. How do I find out?
In the meantime, I found the reason for the large memory consumption: A
tactic was running amok, recursively instantiating a schematic again and
again, creating larger and larger terms. This was easy to fix, and now
everything runs fine again.
> 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.
> > --
> > Peter
> > 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