Email Gateway (Aug 18 2022 at 14:06): Email Gateway (Aug 18 2022 at 14:06):From: barzan stefania <stefania_barzan@yahoo.com>
Dear all,
I have tried to make pdf file for Isabelle theories. And i have some questions.
First, is this also possible under Windows?
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?
Thank you very much,
Stefania Barzan
Email Gateway (Aug 18 2022 at 14:06):From: Makarius <makarius@sketis.net>
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
Last updated: Nov 21 2024 at 12:39 UTC