Zulip Chat Archive

Stream: new members

Topic: Insert Lean code in Latex

Suryansh Shrivastava (Apr 06 2023 at 14:51):

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

Alex J. Best (Apr 06 2023 at 14:53):

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 (Apr 06 2023 at 14:56):

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

Eric Wieser (Apr 06 2023 at 14:58):

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

Kevin Buzzard (Apr 07 2023 at 02:59):

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 (Apr 07 2023 at 03:02):


Kevin Buzzard (Apr 07 2023 at 03:03):

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

Kevin Buzzard (Apr 07 2023 at 03:04):


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

Kevin Buzzard (Apr 07 2023 at 03:05):

\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

Kevin Buzzard (Apr 07 2023 at 03:06):

Credit to @Jason KY.

Kevin Buzzard (Apr 07 2023 at 03:07):

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 (Apr 07 2023 at 08:47):

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 (Apr 07 2023 at 08:51):

In my CICM paper that looked like


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

% add the missing glyphs in the non-monospace font

Last updated: Dec 20 2023 at 11:08 UTC