Re: [isabelle] Proof document to span multiple sessions



On 05/11/2011, at 12:00 AM, Makarius wrote:

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

That is probably the best solution. It only works for polyml, but JinjaThreads won't work in smlnj anyway.

When I made multiple images for Jinja (to speed up development, not so much because of memory problems), we had exactly the problem that there was no one document any more and we introduced a separate session just to build the document. That would defeat the point here, of course.

Cheers,
Gerwin




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