Insert Lean code in Latex

Stream: new members

[Suryansh Shrivastava]

Is there a standard way to insert code snippets into a latex document?

[Alex J. Best]

Many people use lstlean (a style for the listings package), which is included with lean 3, https://github.com/leanprover-community/lean/blob/master/extras/latex/lstlean.md. I think there are a few variations of it around by now with more symbols, but its a good start. There is a lean 4 one too (https://github.com/leanprover/lean4/blob/master/doc/latex/lstlean.tex)

[Adam Topaz]

@Coleton Kotch this :up: will be helpful for you as well

[Eric Wieser]

I usually go with the minted option instead of listings, which uses pymentize under the hood

[Kevin Buzzard]

Yes I've been directing my students away from lstlean because minted seems to work better in practice (isn't there an issue that lstlean doesn't work properly with things like lualatex or xelatex? I can't remember the details of what encouraged me to switch allegiances, maybe Eric's observation has something to do with it under the hood)

[Kevin Buzzard]

Screenshot_20230407-083224.png

[Kevin Buzzard]

Sorry for user-unfriendly screenshot but that's my go-to explanation of how to use minted

[Kevin Buzzard]

\usepackage{minted}
\usepackage{newunicodechar}
\newunicodechar{Ñ}{\ensuremath{\mathcal{N}}}
\newunicodechar{ᵐ}{\ensuremath{^m}}
\newunicodechar{ᶜ}{\ensuremath{^c}}
\newunicodechar{ᶠ}{\ensuremath{^f}}

is the text that would be most annoying to transcribe from that screenshot

[Kevin Buzzard]

\begin{minted}[mathescape, numbersep=5pt, frame=lines, framesep=2mm, fontsize=\small]{Lean}
lemma eventually.mono {p q : α → Prop} {f : filter α}
  (hp : ∀ᶠ x in f, p x) (hq : ∀ x, p x → q x) :
  ∀ᶠ x in f, q x
\end{minted}

[Kevin Buzzard]

Credit to @Jason KY.

[Kevin Buzzard]

One advantage of this is that you don't have to find and download the most recent version of lstlean.tex, it just works out of the box

[Eric Wieser]

Minted can be a pain for lean in pdflatex due to unicode, but works well for lualatex/xetex, especially if you use the DejaVuSansMono package to provide a font with better coverage

[Eric Wieser]

In my CICM paper that looked like

\usepackage{fontspec}
\usepackage{DejaVuSansMono}

\setmonofont[Scale=0.8]{DejaVu Sans Mono}
\newfontface{\monofallback}{DejaVu Sans}[Scale=0.85]

% add the missing glyphs in the non-monospace font
\newunicodechar{⨁}{{\normalfont\monofallback⨁}}
\newunicodechar{⦃}{{\normalfont\monofallback⦃}}
\newunicodechar{⦄}{{\normalfont\monofallback⦄}}
\newunicodechar{⨂}{{\normalfont\monofallback⨂}}
\newunicodechar{⨆}{\ensuremath{\bigsqcup}}
\newunicodechar{⋃}{\ensuremath{\bigcup}}