Lean code in LaTeX and hyperref package

Stream: general

[Ali Ramsey]

Hi, I'm trying to present some Lean code in a LaTeX document, but I keep getting the errors Argument of � has an extra } and Paragraph ended before � was complete at seemingly random points in the code (I can't see anything different about the points it occurs at, and sometimes if I shuffle other parts of the text they disappear or reappear somewhere else, e.g. if I delete the first block of Lean code below, the error in the second block goes away). The smallest example I could reproduce the errors in is below.

\documentclass{article}
\usepackage[colorlinks=true, allcolors=blue]{hyperref}

\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{listings}
\usepackage{amssymb}

\usepackage{color}
\definecolor{keywordcolor}{rgb}{0.7, 0.1, 0.1}   % red
\definecolor{tacticcolor}{rgb}{0.0, 0.1, 0.6}    % blue
\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{attributecolor}{rgb}{0.7, 0.1, 0.1} % red

\def\lstlanguagefiles{lstlean.tex}
% set default language
\lstset{language=lean}

\usepackage{newunicodechar}
\newunicodechar{ₜ}{\ensuremath{_t}}

\begin{document}
\begin{lstlisting}
theorem funext {f₁ f₂ : ∀ (x : α), β x} (h : ∀ x, f₁ x = f₂ x) : f₁ = f₂ := by
  show extfunApp (Quotient.mk f₁) = extfunApp (Quotient.mk f₂)
  apply congrArg
  apply Quotient.sound
  exact h
\end{lstlisting}

(some text)

\begin{lstlisting}
/-- Every commutative (semi)ring is a coalgebra over itself, with `Δ r = 1 ⊗ₜ r`. -/
instance toCoalgebra : Coalgebra R R where
  comul := (TensorProduct.mk R R R) 1
  counit := .id
  coassoc := rfl
  rTensor_counit_comp_comul := by ext; rfl
  lTensor_counit_comp_comul := by ext; rfl

@[simp]
theorem counit_apply (r : R) : counit r = r := rfl

end CommSemiring

namespace Finsupp
variable (ι : Type v)

/-- The `R`-module whose elements are functions `ι → R` which are zero on all but finitely many
elements of `ι` has a coalgebra structure. The coproduct `Δ` is given by `Δ(fᵢ) = fᵢ ⊗ fᵢ` and the
counit `ε` by `ε(fᵢ) =  1`, where `fᵢ` is the function sending `i` to `1` and all other elements of
`ι` to zero. -/
noncomputable
instance instCoalgebra : Coalgebra R (ι →₀ R) where
  comul := Finsupp.total ι ((ι →₀ R) ⊗[R] (ι →₀ R)) R (fun i ↦ .single i 1 ⊗ₜ .single i 1)
  counit := Finsupp.total ι R R (fun _ ↦ 1)
  coassoc := by ext; simp
  rTensor_counit_comp_comul := by ext; simp
  lTensor_counit_comp_comul := by ext; simp

@[simp]
theorem comul_single (i : ι) (r : R) :
    comul (Finsupp.single i r) = (Finsupp.single i r) ⊗ₜ[R] (Finsupp.single i 1) := by
  unfold comul instCoalgebra
  rw [total_single, TensorProduct.smul_tmul', smul_single_one i r]

@[simp]
theorem counit_single (i : ι) (r : R) : counit (Finsupp.single i r) = r := by
  unfold counit instCoalgebra; simp
\end{lstlisting}

\end{document}

(I obviously also have the lstlean.tex file, from https://raw.githubusercontent.com/leanprover/lean4/master/doc/latex/lstlean.tex). I seems like the hyperref package is clashing with lstlean.tex, because when I comment it out the errors go away, but I can't do this in the bigger document I'm working on because I need this package. I couldn't find this issue mentioned anywhere online, it seems like the errors I'm getting are pretty generic. Does anyone know a way to work around this, or why it might be happening?

Apologies if this is not the right place to ask, I thought about asking on stackexchange but I figured it would be more likely that someone here had written Lean code in LaTeX whilst using the hyperref package.

[Patrick Massot]

This problem was discussed recently at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/weird.20LaTeX.20bug.3A.20fullpage.20.2B.20hyperref.20.2B.20listings.20on.20NixOS/near/417641482

[Patrick Massot]

But without a very good conclusion. We ended up wrapping our Lean snippets into minipages.

[Ali Ramsey]

Ah ok, thank you