[isabelle] Proof document to span multiple sessions



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 guess that I could dump the generated files of all sessions in some directory and appropriately string them together in root.tex, but that only gives me the proof document. How can I get to the sources for proof outline?

Cheers,
Andreas

--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 031
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft





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