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



Hi Andreas.

> 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.

Thanks,
  Peter



> 
> 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,
> Andreas
> 
> 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 MHonArc.