Email Gateway (Aug 18 2022 at 19:40): Email Gateway (Aug 18 2022 at 19:40):From: Sylvia Grewe <sylvia.gruener@googlemail.com>
Hello everybody,
I am currently writing a master's thesis which includes a lot of Isabelle formalizations and proofs. So of course, I would like to write sections in which I show for example some "highlights" of the formalization or of the proofs, but not entire Isabelle theories (this being saved for the appendix).
I have already written a few "bigger" documents where I also used Isabelle's Latex generation, so I know the basics of how to generate Latex documents and how to use antiquotations etc. But as "solution" to the above scenario, I have always simply copied the parts of the .tex code generated from my theory files and inserted them in my tex source files where I wanted them. But obviously, this can be a lot of work, and if you change just a minor thing like a variable name in your theory files, you have to do this all over again and it is very likely you forget something and in the end, your Latex document is not consistent with your Isabelle theories. Also, I guess the Isabelle latex support is not really meant to be used like this ;).
So basically, I am looking for a good way to combine Isabelle and Latex such that
How do you deal with such problems when you create large documents and want to show parts of your Isabelle theories inside the text?
Thanks in advance,
Sylvia Grewe
Email Gateway (Aug 18 2022 at 19:40):From: Tobias Nipkow <nipkow@in.tum.de>
Maybe this helps: https://isabelle.in.tum.de/community/Generate_TeX_Snippets
The example is a bit simple, but you can probably do something like this:
text_raw{*
\DefineSnippet{name}{
*}
<your Isabelle text>
text_raw{* } *}
However, I haven't tried this. I have another way of achieving what you want,
but it needs a lengthier piece of latex code. I can send it to you if you want.
Tobias
Email Gateway (Aug 18 2022 at 19:42):From: Makarius <makarius@sketis.net>
On Mon, 14 May 2012, Sylvia Grewe wrote:
I am currently writing a master's thesis which includes a lot of
Isabelle formalizations and proofs. So of course, I would like to write
sections in which I show for example some "highlights" of the
formalization or of the proofs, but not entire Isabelle theories (this
being saved for the appendix).
But as "solution" to the above scenario, I have always simply copied the
parts of the .tex code generated from my theory files and inserted them
in my tex source files where I wanted them.
Also, I guess the Isabelle latex support is not really meant to be used
like this ;).
Copying generated material by hand is not a solution, as you have already
noticed. In some situations one can copy formally, using perl in a smart
way, say by integrating it into the isabelle make process. This is useful
for some hardcore re-organizations of the .tex sources. I used to have it
in my own setup, when subscripts where not yet supported by default, to
turn foo_42 to foo$_{42}$ etc. or to change the font/color of the symbol
following some funny Isabelle control symbol.
- I do not need to create very obfuscated versions of my Isabelle
theories, writing all the explanatory text in between definitions and
proof commands, blocking out unwanted parts using %invisible (This would
obviously be one answer to ensure only my first condition, but I would
like to keep and to work on "clean" versions of my theories, and also to
include these "clean" versions in my appendix. However, if there is a
way of managing a "clean" version of an Isabelle theory file next to a
"heavily commented and annotated" version such that all the definitions
inside both versions are consistent, I would also be interested in
that.)
This might point to a more high-level way to organize certain sections in
the sources. The interpretation of %invisible tags is just an example
that is provided by default. The underlying "comment" package of latex
can do more things, or one can use other packages to shuffle regions
within latex.
So assuming that the amount of hilighted things is relatively low, you
could tag them as %hilighted and then include the generated .tex sources
twice, with different definitions of the underlying latex macros.
- (optionally, if you know anything about it) I can use this way
together with latexmk such that the Isabelle .tex representation I need
is updated every time I change the .thy files. For this to work, one
needs to provide a perl method that tells latexmk how to generate a
tex/pdf file from a .thy file. But for example with isabelle make, you
usually produce .tex output for a bunch of Isabelle theory files, so if
you used this, it would regenerate the .tex output of all Isabelle
theory files even though you only changed one .thy file (which can then
take quite long if you have a lot of .thy files that belong
together...).
Many years ago, when I wrote my own thesis with the Isabelle document
preparation system, it was taking really long (45min IIRC). I organized
the "make" process mainly by hand, activating or deactivating theories in
ROOT.ML and in root.tex via \includeonly{} of latex.
The usedir -D options helps here, because it will dump the generated stuff
in some place and not delete it. So you can include old versions of
generated sources that where not checked again via ROOT.ML.
On the other hand, current machines might be fast enough to rebuild
everything on the spot in a few seconds/minutes. It also gives some
opportunity to rethink the content of the document in the meantime.
Makarius
Email Gateway (Aug 18 2022 at 20:25):From: "Tim (McKenzie) Makarios" <tjm1983@gmail.com>
I used this sort of thing for my MSc thesis. I used text (and sometimes
txt) instead of text_raw, and found it useful to include the %EndSnippet
comment suggested in the page Tobias linked to. Together with the other
suggestions in that page, including using a Makefile, I found a solution
based on this that was adequate for my needs.
Tim
<><
signature.asc
Last updated: May 07 2024 at 01:07 UTC