Lean Latex unicode

Stream: general

[Jason KY.]

Hi, I'm trying to present some Lean code in a Latex document. In particular, I have the following code

\documentclass{article}

\usepackage[utf8x]{inputenc}
\usepackage{amssymb, upgreek}

\usepackage{color}
\definecolor{keywordcolor}{rgb}{0.7, 0.1, 0.1}   % red
\definecolor{commentcolor}{rgb}{0.4, 0.4, 0.4}   % grey
\definecolor{symbolcolor}{rgb}{0.0, 0.1, 0.6}    % blue
\definecolor{sortcolor}{rgb}{0.1, 0.5, 0.1}      % green
\definecolor{errorcolor}{rgb}{1, 0, 0}           % bright red
\definecolor{stringcolor}{rgb}{0.5, 0.3, 0.2}    % brown

\usepackage{listings}
\def\lstlanguagefiles{lstlean.tex}
\lstset{language=lean}

\begin{document}

\begin{lstlisting}
  lemma tendsto_uniformly_on_of_ae_tendsto' [is_finite_measure μ]
  (hf : ∀ n, measurable (f n)) (hg : measurable g)
  (hfg : ∀ᵐ x ∂μ, tendsto (λ n, f n x) at_top (𝓝 (g x))) {ε : ℝ} (hε : 0 < ε) :
  ∃ t, measurable_set t ∧ μ t ≤ ennreal.of_real ε ∧ tendsto_uniformly_on f g at_top tᶜ :=
\end{lstlisting}

\end{document}

in the same directory as the lstlean.tex file from https://github.com/leanprover-community/lean/blob/master/extras/latex/lstlean.tex

However, when I compile with XeLaTeX all of the unicode is gone. Is there a way to fix this?
Using pdfLaTeX works but I would like to use some packages which is not compatible with pdfLaTeX.

[Kevin Buzzard]

I can reproduce -- seems to work fine with pdflatex, \foralls and \Rs missing with lualatex and xelatex

[Alex J. Best]

If using xelatex you probably need to remove the \usepackage[utf8x]{inputenc} line at least

[Kevin Buzzard]

still compiles but still no unicode

[Kevin Buzzard]

and still compiles with pdflatex and looks fine

[Alex J. Best]

Yeah this seems quite tricky. For Lean 4 it seems minted is recommended to use XeLaTeX https://leanprover.github.io/lean4/doc/syntax_highlight_in_latex.html but I don't know if there are corresponding instructions / python files for Lean 3

[Alex J. Best]

Ah actually maybe these instructions will work then
https://github.com/leanprover-community/lean/blob/master/doc/syntax_highlight_in_latex.md

[Jason KY.]

Im able to get:
image.png
with the following:

\documentclass{article}
\usepackage{fontspec}
% switch to a monospace font supporting more Unicode characters
\setmonofont{FreeMono}
\usepackage{minted}
% instruct minted to use our local theorem.py
\newmintinline[lean]{lean4.py:Lean4Lexer -x}{bgcolor=white}
\newminted[leancode]{lean4.py:Lean4Lexer -x}{fontsize=\footnotesize}
\usepackage{newunicodechar}
\newfontfamily{\freeserif}{DejaVu Sans}
\newunicodechar{𝓝}{\ensuremath{\mathcal{N}}}
\newunicodechar{ᵐ}{\ensuremath{^m}}
\newunicodechar{ᶜ}{\ensuremath{^c}}


\begin{document}
% some example options
\begin{minted}[mathescape,
               linenos,
               numbersep=5pt,
               frame=lines,
               framesep=2mm]{Lean}
lemma tendsto_uniformly_on_of_ae_tendsto' [is_finite_measure μ]
  (hf : ∀ n, measurable (f n)) (hg : measurable g)
  (hfg : ∀ᵐ x ∂μ, tendsto (λ n, f n x) at_top (𝓝 (g x)))
  {ε : ℝ} (hε : 0 < ε) :
∃ t, measurable_set t ∧ μ t ≤ ennreal.of_real ε ∧
  tendsto_uniformly_on f g at_top tᶜ
\end{minted}
\end{document}

and the lean4.py from that lean4 page

[Jason KY.]

Alex J. Best said:

Ah actually maybe these instructions will work then
https://github.com/leanprover-community/lean/blob/master/doc/syntax_highlight_in_latex.md

Great! I will give it a try

[Jason KY.]

image.png
It seems that some of the unicode is not declared as with the lean 4 version. I think I will just declare manually for now.
Thanks for the help!

[Alex J. Best]

Yeah that looks pretty good, it looks like there is lean support in pygments version 2 by default so maybe additional files aren't needed

[Jason KY.]

Yeah, it seems to work the same way without adding lean4.py or minted.sty