LaTeX beamer

Stream: general

[Yaël Dillies]

Jannis Limperg said:

Good ol' fragile. "Half of our stuff doesn't work until you give this random argument and none of our error messages will even hint at this."

Guess who just spent half an hour debugging a \verb|| call :sweat:

[Eric Wieser]

Why use verb when you can use mintinline?

[Yaël Dillies]

Because I don't know what it is! Does it come from minted?

[Anthony Bordg]

What's the easiest way to extract Lean code snippets from VSCode for inclusion in Beamer slides? Are listings or minted the recommended methods, as outlined in the Lean manual? Which approach would you suggest?

[Adam Topaz]

I think listings is the most commonly used.

[Anthony Bordg]

Just realized the snippets need to be rather short ... (removing the comments helps).

[Eric Wieser]

I'd argue that minted + XeTeX/LuaLatex + fontspec + JuliaMono has the better results

[Yury G. Kudryashov]

@Eric Wieser Could you please post a preamble for minted+LuaLaTeX?

[Adam Topaz]

Even better would be to put such a preamble as a wiki page in mathlib.

[Eric Wieser]

I'll make an overleaf template (edit: submitted and pending moderation)

[Eric Wieser]

The basic preamble is

\documentclass{article}
\usepackage{fontspec}
\usepackage{minted}

% JuliaMono has all the symbols needed for Lean code
\setmonofont[Scale=MatchLowercase]{JuliaMono}[
  Extension=.ttf,
  UprightFont=*-Regular,
  BoldFont=*-Bold,
  ItalicFont=*-RegularItalic,
  BoldItalicFont=*-BoldItalic,
  RawFeature={-calt},
]

% autogobble lets us indent the lean code to distinguish it from the latex
\setminted{frame=single}
\newmintinline[lean]{lean}{breaklines,breakbefore={. },breakafter={_}}
\newminted[leancode]{lean}{autogobble}

% Configure the appearance of minted.
% We adjust the spacing around minted environments, which stretches badly by default
\fvset{listparameters=\setlength{\topsep}{0pt}\setlength{\parsep}{0pt}}
\AtBeginEnvironment{minted}{\vspace{4pt}}
\renewcommand{\floatpagefraction}{.99}
\renewcommand{\bottomfraction}{.7}

along with unzipping the juliamono tarball in an appropriate place

[Eric Wieser]

This is really just a slightly-opinionated version of https://docs.lean-lang.org/lean4/doc/syntax_highlight_in_latex.html#example-with-minted

[Eric Wieser]

Publishing was more trouble that it was worth, but I've made a public link at https://www.overleaf.com/read/cgqkbtvqrsdr#4440c9

[Bjørn Kjos-Hanssen]

Eric Wieser said:

Publishing was more trouble that it was worth, but I've made a public link at https://www.overleaf.com/read/cgqkbtvqrsdr#4440c9

Great, this still works if I simply change the documentclass to beamer.

[Notification Bot]

Eric Wieser has marked this topic as unresolved.

[Eric Wieser]

I should perhaps point out that the link above is still Lean 3 highlighting, because the pygments release for Lean 4 fell slightly after texlive 2024 was cut (or at least, overleaf did not update it in their docker image). Hopefully it made 2025...

[Bjørn Kjos-Hanssen]

@Eric Wieser It still works well, I'd say.