Email Gateway (Aug 19 2022 at 14:44): Email Gateway (Aug 19 2022 at 14:44):From: Peter Lammich <lammich@in.tum.de>
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?
Email Gateway (Aug 19 2022 at 14:44):From: Peter Lammich <lammich@in.tum.de>
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.
Email Gateway (Aug 19 2022 at 14:44):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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,
Andreas
Email Gateway (Aug 19 2022 at 14:44):From: Peter Lammich <lammich@in.tum.de>
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,
AndreasOn 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. ProjectNameit 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?
Email Gateway (Aug 19 2022 at 14:44):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Peter,
Normally, Isabelle starts PolyML in 32-bit mode even if you have a 64-bit system. I last
compared 32-bit PolyML against 64-bit PolyML two years ago and at that time, 32-bit took a
bit more than half the time the 64-bit system took for the same task. IIRC, the following
tells you the setting.
isabelle getenv ML_PLATFORM
Best,
Andreas
Last updated: Nov 21 2024 at 12:39 UTC