Stream: Beginner Questions

Topic: Isabelle Listings in LaTeX


view this post on Zulip Max Nowak (May 27 2021 at 13:27):

I'm writing a larger document in LaTeX, and while it is primarily in classic math notation, I want to include some interesting Isabelle/HOL snippets. So far (i.e. not very far yet :D) I've used verbatim, but verbatim has issues with ∀, ⇒, etc. I am aware of https://isabelle.in.tum.de/doc/sugar.pdf, however I do not want to typeset my whole document in Isabelle, merely a few snippets, which doesn't have to be 1:1 what isabelle sugar would produce.
I also found https://github.com/lammich/isabelle_llvm/blob/master/papers/2021_Enschede_Talk/lstisabelle.tex which looks promising but has rough edges and depends on some auto-generated isabelle tex files which give me plenty of LaTeX errors.
Is there some easy-to-use style I can just import and get pretty isabelle listings?

view this post on Zulip Max Nowak (May 27 2021 at 13:31):

Main concerns are rendering unicode symbols (forall, etc) in the listings, maybe bold and/or colored keywords.

view this post on Zulip Lukas Stevens (May 27 2021 at 13:35):

I just use

\usepackage{listings}
\definecolor{isarblue}{HTML}{006699}
\definecolor{isargreen}{HTML}{009966}
\lstdefinelanguage{isabelle}{%
    keywords=[1]{type_synonym,datatype,fun,abbreviation,definition,proof,lemma,theorem,corollary},
    keywordstyle=[1]\bfseries\color{isarblue},
    keywords=[2]{where,assumes,shows,and},
    keywordstyle=[2]\bfseries\color{isargreen},
    keywords=[3]{if,then,else,case,of,SOME,let,in,O},
    keywordstyle=[3]\color{isarblue},
}
\lstset{%
  language=isabelle,
  escapeinside={&}{&},
  columns=fixed,
  extendedchars,
  basewidth={0.5em,0.45em},
  basicstyle=\ttfamily,
  mathescape,
}

Unicode symbols go inside mathescape $.

view this post on Zulip Lukas Stevens (May 27 2021 at 13:35):

You might need to fiddle around to get it typeset in a nice way though.


Last updated: Sep 25 2022 at 23:25 UTC