Re: [isabelle] Proof document to span multiple sessions



On Fri, 4 Nov 2011, Andreas Lochbihler wrote:

Florian suggested to split JinjaThreads in the AFP into multiple sessions. He hopes that this will reduce the overall memory consumption because Isabelle forces PolyML to share objects on the heap only when the image is written. I am currently testing whether this is a promising way. However, I am wondering how multiple sessions would fit in with the proof document and proof outline in the AFP. Ideally, there would be one document each that covers all JinjaThreads theories although they are processed in different sessions. Is there any support for this?

I can't say anyting specific about the intention of the AFP setup, although I remember a time when there was a 500MB heap limit (in Poly/ML 4.x) and Gerwin split up the original Jinja session to get the compaction effect when heaps are dumped and reloaded.

In Poly/ML 5.x the compaction phase has become available separately, without dumping. So in principle you could just split the invocations of use_thys in ROOT.ML and make an intermediate share_common_data() in raw ML in between.

I have already experimented with this occasionally. It basically works (reducing heap size at runtime from several GB to a few 100 MB). It also has some limitations: doing it too aggressively can make the process dump core.


	Makarius





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