Re: [isabelle] Looking for the GOOD way to use Isabelle and Latex together when writing a thesis

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.


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