Re: [isabelle] generate- pdf



On Mon, 28 Sep 2009, barzan stefania wrote:

I have tried to make pdf file for Isabelle theories. And i have some questions.

First, is this also possible under Windows?

Yes, it should work, by using the tetex installation of Cygwin. If you have installed everything according to http://isabelle.in.tum.de/installation.html (bottom part) then document preparation should work as described in the Isabelle manuals. See http://isabelle.in.tum.de/dist/Isabelle/doc/system.pdf chapter 3, or http://isabelle.in.tum.de/dist/Isabelle/doc/isar-ref.pdf chapter 4.

(I've tried this a few months ago.)


In the http://www.cl.cam.ac.uk/research/hvg/Isabelle/faq.html i found out it is possible to make a so called heap image. That will be very useful for me when i make the pdfs. but until now i could not make it work. Can someone be more specific and explain to me in more details how to do it?

Heap images are not necessary for document preparation, but both can be controlled via isabelle usedir. Note that in contrast to what the FAQ suggests, the fundamental isabelle-process provides even more basic heap persistence. The system manual will tell you a few more things. (In practice the main problem will be to convince Proof General not to time out and abort, while Isabelle is busy writing a heap image.)


	Makarius





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