Re: [isabelle] Poor man's LaTeX markup for Isabelle listings

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;

1. I'd like to write them in my favourite LaTeX editor.
2. They sometimes deviate from my actual formalisation for readability
or didactic purposes.
3. 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.
4. 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.
5. 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
– actually written by Isabelle user John Wickerson :-))

What would you suggest?


Christoph Lange, School of Computer Science, University of Birmingham, Skype duke4701

→ Mathematics in Computer Science Special Issue on “Enabling Domain
  Experts to use Formalised Reasoning”; submission until 31 October.

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