Generate TeX Snippets

From Isabelle Community Wiki
Jump to: navigation, search

Usually Isabelle's document preparation system directly generates PDF files from theory files. Sometimes (e.g., when writing a document in cooperation with people not using Isabelle) it is needed to generate only TeX snippets and include them into a normal TeX document.

The idea is to add a TeX command that marks the parts of a theory file that should be exported. The generated file is then transformed by an easy sed invocation. Afterwards, the snippets can simply be used in the TeX file by calling \Snippet{<snippet_name>}.

To annotate a snippet in an Isabelle theory use

 text {*
 \DefineSnippet{half_log_simps}{
    @{thm [display] half.simps}
    @{thm_style [display] concl Loga.log.psimps}
 }%EndSnippet
 *}

when referring to existing facts, and

 text_raw {*\DefineSnippet{<snippet_name>}{*}
 ...
 text_raw {*}%EndSnippet*}

when referring to arbitrary parts of a theory file in theory mode and proof mode, respectively (i.e., out- or inside of a proof).

At the beginning of your main TeX file add:

 \newcommand{\DefineSnippet}[2]{%
   \expandafter\newcommand\csname snippet--#1\endcsname{%
     \begin{quote}
     \begin{isabelle}
     #2
     \end{isabelle}
     \end{quote}}}
 \newcommand{\Snippet}[1]{\csname snippet--#1\endcsname}
 
 \input{generated/snippets}

Then do the following:

Create a file ROOT containing

 session Snippets = "HOL" +
   options [
     document = "pdf",
     document_output = "generated"]
   theories
     File
   document_files
     build

which tells the system to generate files in the subdirectory "generated". Then create a directory "document" containing an executable file "build" with the following content:

 #!/bin/bash
 find . -type f -name "*.tex" -exec sed -n '/DefineSnippet/,/EndSnippet/p' {} + > ../snippets.tex
 touch ../document.pdf

This script will be run in a subdirectory of "generated", hence the occurrences of ".." to refer to "generated".

In order to generate the snippets run

 isabelle build -d . Snippets

and then compile your TeX sources as usual.

Caveats

Misspelling a snippet

If you misspell a snippet name, then you will receive no kind of notification from the system. The following replacement code remedies that:

 \usepackage{ifthen}
 
 \newcommand{\DefineSnippet}[2]{%
    \expandafter\newcommand\csname snippet--#1\endcsname{%
      %\begin{quote}
      \begin{isabelle}
      #2
      \end{isabelle}
      %\end{quote}
      }}
 \newcommand{\Snippet}[1]{ \ifcsname snippet--#1\endcsname {\csname snippet--#1\endcsname} \else
   +++++++ERROR: Snippet ``#1 not defined+++++++ \fi}
  
 \input{generated/snippets}

Necessary imports

It is important that the folder of your .tex also contains the following files

 comment.sty
 isabelle.sty
 isabellesym.sty
 isabelletags.sty

The files can be copied from

generated/snippets/document 

after the first time you run

 isabelle build -d . Snippets

They should be imported in the beginning of the tex file as follows

 \usepackage{isabelle,isabellesym}

Note that the latex distribution also has a comment.sty, but that one is in conflict with Isabelle's. Therefore, do NOT write this:

\usepackage{comment} <-- don't write this!

Style

You can choose a style for your code, e.g. italic:

   \isabellestyle{it}

When using old-style isabelle make

For each theory file File.thy containing snippets add to the Makefile:

 sed -n '/DefineSnippet/,/EndSnippet/p' ./Paper/generated/File.tex > generated/snippets.tex