Email Gateway (Aug 19 2022 at 12:04): Email Gateway (Aug 19 2022 at 12:04):From: Christoph LANGE <math.semantic.web@gmail.com>
Dear Isabelle community,
I frequently need to include Isabelle source code listings in my LaTeX
documents. However I have not yet figured out how to make Isabelle's
document preparation machinery export LaTeX snippets. I know it's
possible, but I haven't had the time. Moreover I often need to deviate
from my verbatim formalisation for didactic purposes.
I'm sure this has been done before, and I'm sure one could realise a
more advanced solution by reusing parts of the *.sty files that come
with Isabelle, but anyway I quickly hacked this LaTeX package together
from scratch, which does part of the job:
https://github.com/clange/latex/blob/master/pmisabelle.sty
If you check out https://github.com/clange/latex you may find a few more
useful LaTeX packages. In
https://github.com/clange/latex/blob/master/lstsemantic.sty#L20 you will
see that I have also tried this with the "listings" package, but gave up
quite soon, because the result didn't look nice.
Cheers,
Christoph
Email Gateway (Aug 19 2022 at 12:19):From: Lawrence Paulson <lp15@cam.ac.uk>
I continue to struggle with this machinery myself.
Some people use this system to write entire papers based upon their theory development. But this isn't very practical if your development takes 40 minutes to run, as in a recent one I completed. Instead I use the document preparation system to convert the theory files into .tex files, which I then insert into my document within the brackets \begin{isabelle} … \end{isabelle} or simply \isa{…}.
I pre-process these files using a shell script (attached) in order to replace some of the numerous macros by the character equivalents, in order to make them more compact unreadable.
Larry Paulson
cleanTeX.pl
Email Gateway (Aug 19 2022 at 12:19):From: Tobias Nipkow <nipkow@in.tum.de>
Are saying you need to run the whole development every time you latex your
paper? This is only the case if you want to include literally (some of) the text
of your theories. Which doesn't work very well anyway because you have to stick
to the order in which the material is presented in the theories.
The normal way to write a paper with Isabelle is to build on an image that
contains all the theories, start from that image and use antiquotation to
display material.
If for formatting reasons you absolutely need some fragment of the source text,
the LaTeX sugar document contains a section Theory Snippets describing how to do
that in a selective manner.
Tobias
Email Gateway (Aug 19 2022 at 12:20):From: Christoph LANGE <math.semantic.web@gmail.com>
Thanks, Larry and Tobias, for sharing your experience on including
Isabelle sources in LaTeX. I see that one has more flexibility in using
the document preparation system than I had thought.
Nevertheless I wonder whether is also offers an easy solution for the
problem that I tried to solve with my pmisabelle.sty, i.e. a solution
that addresses the following requirements:
My papers consist of a lot of LaTeX and a few short Isabelle listings;
therefore:
They sometimes deviate from my actual formalisation for readability
or didactic purposes.
It is not absolutely essential that these listings are syntactically
and semantically correct. "Correct to the eye of a proof-reader" is
good enough; "correct to Isabelle's verification engine" is nice to have
but not essential.
Exporting LaTeX snippets from my actual Isabelle sources is merely
nice to have. I wouldn't mind copy/pasting snippets from my *.thy files
into the LaTeX editor and applying minor adaptations manually or via a
script to make them render as nice LaTeX.
I don't want to invest a lot into the formalisation (such as
inserting special markup) to make it "exportable".
pmisabelle.sty satisfies these requirements, except that the adaptations
required in step (4) are a bit more than minor, which is mainly because
I am not experienced with modifying the behaviour of the LaTeX parser
(catcodes etc.). My approach to use a math align environment requires
me, e.g., to manually escape underscores in identifiers and to make sure
I insert the right amount of & and \\. The alternative approach to use
listings.sty would require me to explicitly wrap terms into $…$, to
manually pretty-print "…" into ``…'', plus possibly some more work to
get the spacing as right as you could do it in math mode, and it would
not accept Unicode input, which LaTeX allows
(http://tex.stackexchange.com/questions/110042/entering-unicode-math-symbols-into-latex-direct-from-keyboard-on-a-mac
– actually written by Isabelle user John Wickerson :-))
What would you suggest?
Christoph
Email Gateway (Aug 19 2022 at 12:20):From: Lawrence Paulson <lp15@cam.ac.uk>
The way I do markup is undoubtedly viewed by some as an abuse of the document preparation system, but I have exactly the same goals as you list below. An example of a paper written in that style can be found here, starting on page 5:
http://www.cl.cam.ac.uk/~lp15/Pages/Gödel-ar.pdf
I didn't understandThe following paragraph, were you wrote about modifying the behaviour of the LaTeX parser. I never do that. Equally there's no need to manually escape anything. The main trick is to let the document preparation system translate your theory files into LaTeX. This is not something you are supposed to do, so the way of doing it seems to change every year or two.
Larry Paulson
Last updated: Nov 21 2024 at 12:39 UTC