Make snippets from LaTeX files:
Copy snippets to clipboard:
Save snippets:
The following command in the terminal makes the proof assistant Isabelle generate LaTeX code for the theories in the current directory:
isabelle build -D . -o document=pdf -o document_output=outputNote that this requires a ROOT file in that directory. Such a file can be generated by
isabelle mkroot (but must be adjusted afterwards).
For each theory T.thy, the command generates a LaTeX file output/document/T.tex.
This webpage takes such LaTeX files and chops them into pieces.
One can either copy/paste the LaTeX of a single theory in the text area to the left or upload multiple files.
The results are displayed to the right.
This process makes it possible to include only the desired parts of the theory when writing a paper: that cartouche containing a crucial definition or lines 2-5 of that important proof.
The LaTeX code can also be used when collaborating on sites like Overleaf to easily include Isabelle code in papers with multiple authors.
The tool generates a number of \SNIP{name}{body} commands where the names have the following shape:
[Theory:]cmd:name[-no]-line[-cartouche]
theory is added when snippets are generated for more than one theory.cmd corresponds to the Isabelle command, e.g. "lemma" or "definition".name is a best guess at identifying the snippet.
In most cases it will be the name following the Isabelle command, e.g. "f" in "fun f ...".
Symbols like φ (\<phi>) are converted to their name ("phi") and underscores are
replaced by
hyphens.
If the tool cannot guess a name, e.g. for anonymous corollaries, it uses a hash of the Isabelle code.
This remains the same as long as the Isabelle code for that particular snippet is not changed.
no is added when the snippet name would not otherwise be unique. This can especially happen
when a name cannot be guessed.line specifies the line of the snippet starting from 0.cartouche is a number, starting from 0, used to retrieve only that cartouche on the specified
line.
To use the snippets you must include the *.sty files from output/document/ in your own
LaTeX directory.
The following LaTeX code is recommended.
In particular, the tool outputs \SNIP and \Cartouche commands that must be defined to
use the snippets.
\usepackage{isabelle, isabellesym}
\isabellestyle{it} % optional
\newcommand{\SNIPTEXT}[1]{#1} % remove #1 to ignore text commands
\newcommand{\SNIP}[2]{\expandafter\newcommand\csname snippet--#1\endcsname{#2}}
\input{snips} % assuming the snippets are saved as snips.tex
% \GetSnip{name} gets the snippet defined by `name' or produces a warning that it does not exist.
\newcommand{\GetSnip}[1]{%
\ifcsname snippet--#1\endcsname%
\csname snippet--#1\endcsname%
\else%
\PackageWarning{snips}{Snippet ``#1'' is undefined.}%
\emph{Warning: Snippet ``#1'' is undefined.}%
\fi%
}
% \RawCartouche{name}{line}{n}: content of cartouche `n' on line `line' of snippet `name'
\newcommand{\RawCartouche}[3]{\GetSnip{#1-#2-#3}}
% \Cartouche{name}{line}{n}: enclosed cartouche `n' on line `line' of snippet `name'
\newcommand{\Cartouche}[3]{%
{\isacartoucheopen}%
\RawCartouche{#1}{#2}{#3}%
{\isacartoucheclose}%
}
The LaTeX error "Command \guilsinglright unavailable in encoding OT1." can be fixed by also adding
\usepackage[T1]{fontenc}.
The following LaTeX code can be useful:
% \Snippet{name}: the full snippet `name'
\newcommand{\Snippet}[1]{{%
\newcount\i
\i=0
\loop
\GetSnip{#1-\the\i}%
\advance \i 1
\ifcsname snippet--#1-\the\i\endcsname
\repeat
}}
% \SnippetPart{n}{m}{name}: the snippet `name' from line `n' to line `m' inclusive
\newcommand{\SnippetPart}[3]{{%
\newcount\i
\i=#1
\loop
\ifnum \i=#2
\renewcommand{\isanewline}{}%
\fi
\GetSnip{#3-\the\i}%
\advance \i 1
\ifnum \i>#2 {}
\else \repeat
}}
The following code can be necessary to make the snippets work with some document classes.
\def\isadelimtheory{}\def\endisadelimtheory{}
\def\isatagtheory{}\def\endisatagtheory{}
\def\isadelimML{}\def\endisadelimML{}
\def\isadelimdocument{}\def\endisadelimdocument{}
\def\isatagML{}\def\endisatagML{}
\def\isatagdocument{}\def\endisatagdocument{}
\def\isafoldML{}
\def\isadelimproof{}\def\endisadelimproof{}
\def\isatagproof{}\def\endisatagproof{}
\def\isafoldproof{}
Take the following Isabelle theory as example:
theory Scratch imports Main begin
lemma myConjI: ‹P ⟹ Q ⟹ P ∧ Q›
..
end
To include the whole lemma with proof in your paper you can use:
\begin{isabelle}
\Snippet{lemma:myConjI}
\end{isabelle}
To include just the first line of the lemma:
\begin{isabelle}
\SnippetPart{0}{0}{lemma:myConjI}
\end{isabelle}
Or to include just the contents of the cartouche (P ⟹ Q ⟹ P ∧ Q):
\begin{isabelle}
\RawCartouche{lemma:myConjI}{0}{0}
\end{isabelle}
This tool was built for Isabelle 2022 and may not support the LaTeX output of other versions. The processing of the LaTeX is ad hoc and may result in unexpected behaviour, especially regarding the names of snippets.
The tool reduces duplication, to save space in the final output, by trying to replace the cartouches on each
line with a
\Cartouche command that references the \SNIP for that cartouche.
However, it can only do so for cartouches without newlines: those that contain newlines are left in place.
This means that every cartouche is not necessarily inserted by the \Cartouche macro.
In particular, to modify the delimiters around cartouches that are inserted via \Snippet and
\SnippetPart it is safest to use code like \renewcommand{\isacartoucheopen}{...}.
Depending on the Isabelle code, it may not be enough to modify the definition of \Cartouche.
The tool assumes that the Isabelle theories use the ‹› cartouche delimiters, not the older double quotes.
See Section 2.7 of the Isabelle System
Manual
for how to update your theory file accordingly.
Alternatively, to update a single theory using Isabelle/jEdit, search for "([^"]+)" and replace it
with
‹$1›.
Some manual cleanup is likely necessary afterwards.
The source code is available on GitHub: astahfrom/cartouches.
Asta Halkjær From. Github: github.com/astahfrom/