我正在合并两个之前正常工作的文档，并遇到了这个错误（实际上，有好几个这样的错误）。我将其简化为以下 MWE，它似乎是由 listings 和 hyperref 包之间的一些交互引起的。如果我删除 hyperref 包（更改导入顺序似乎根本不重要），一切都会正常工作。我无法减少的一件事是我所包含的代码。此外，它只发生在 TexLive 2022 中，而不是 TexLive 2021 中。
主文本
\documentclass{article} %
\usepackage[T1]{fontenc} %
\usepackage{listings} %
\usepackage{hyperref} % comment this line for the error to disappear
\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
\usepackage{amssymb} %
\def\lstlanguagefiles{lstlean.tex}
\lstnewenvironment{leancode}
{\lstset{language=lean}} %
{} %
\begin{document}
\lstinputlisting[language=lean]{zolt.lean}
\end{document}
zolt.lean（我将代码包含在 listings 包中）
structure Point : Type
structure Segment : Type where
p1 : Point
p2 : Point
neq : p1 ≠ p2
inductive PolySegment : Type where
| s₀ : PolySegment
| s₁ : Segment → PolySegment
| s₂ : PolySegment → PolySegment → PolySegment
opaque IsJordan : PolySegment → PolySegment → Prop
structure Face : Type where
s1 : PolySegment
s2 : PolySegment
jordan : IsJordan s1 s2
inductive PolyFace : Type where
| f₀ : PolyFace
| f₁ : Face → PolyFace
| f₂ : PolyFace → PolyFace → PolyFace
opaque IsClosed : PolyFace → PolyFace → Prop
structure Volume : Type where
vol1 : PolyFace
vol2 : PolyFace
closed : IsClosed vol1 vol2
inductive PolyVolume where
| v₀ : PolyVolume
| v₁ : Volume → PolyVolume
| v₂ : PolyVolume → PolyVolume → PolyVolume
opaque PolyVolume.HasFaceIntersection
: PolyVolume → PolyVolume → Prop
axiom PolyVolume.EmptyAlwaysHasFaceIntersection {v : PolyVolume} :
HasFaceIntersection v₀ v
axiom PolyVolume.HasFaceIntersection_comm {v u : PolyVolume} :
HasFaceIntersection v u → HasFaceIntersection u v
def PolyVolume.NonEmpty : PolyVolume → Prop
| v₀ => False
| v₁ _ => True
| v₂ _ _ => True
class Zₚ (a : Type u) where
ε : a
cmp : a → a → Prop
join : (p : a) → (q : a) → cmp p q → a
NonEmpty : a → Prop
您还需要伊斯特兰用于精益语言定义。
我不能不将 hyperref 包含在实际文档中，所以我没有选择。相关的原始日志是：
! Argument of � has an extra }.
<inserted text>
\par
l.52
ε : a
I've run across a `}' that doesn't seem to match anything.
For example, `\def\a#1{...}' and `\a}' would produce
this error. If you simply proceed now, the `\par' that
I've just inserted will cause me to report a runaway
argument that might be the root of the problem. But if
your `}' was spurious, just type `2' and it will go away.
Runaway argument?
! Paragraph ended before � was complete.
<to be read again>
\par
l.52
ε : a
I suspect you've forgotten a `}', causing me to apply this
control sequence to too much text. How can we recover?
My plan is to forget the whole thing and hope for the best.
! Argument of � has an extra }.
<inserted text>
\par
l.52
ε : a
I've run across a `}' that doesn't seem to match anything.
For example, `\def\a#1{...}' and `\a}' would produce
this error. If you simply proceed now, the `\par' that
I've just inserted will cause me to report a runaway
argument that might be the root of the problem. But if
your `}' was spurious, just type `2' and it will go away.
Runaway argument?
! Paragraph ended before � was complete.
<to be read again>
\par
l.52
ε : a
I suspect you've forgotten a `}', causing me to apply this
control sequence to too much text. How can we recover?
My plan is to forget the whole thing and hope for the best.
! Argument of � has an extra }.
<inserted text>
\par
l.52
ε : a
I've run across a `}' that doesn't seem to match anything.
For example, `\def\a#1{...}' and `\a}' would produce
this error. If you simply proceed now, the `\par' that
I've just inserted will cause me to report a runaway
argument that might be the root of the problem. But if
your `}' was spurious, just type `2' and it will go away.
Runaway argument?
! Paragraph ended before � was complete.
<to be read again>
\par
l.52
ε : a
I suspect you've forgotten a `}', causing me to apply this
control sequence to too much text. How can we recover?
My plan is to forget the whole thing and hope for the best.
! Argument of � has an extra }.
<inserted text>
\par
l.52
ε : a
I've run across a `}' that doesn't seem to match anything.
For example, `\def\a#1{...}' and `\a}' would produce
this error. If you simply proceed now, the `\par' that
I've just inserted will cause me to report a runaway
argument that might be the root of the problem. But if
your `}' was spurious, just type `2' and it will go away.
Runaway argument?
! Paragraph ended before � was complete.
<to be read again>
\par
l.52
ε : a
I suspect you've forgotten a `}', causing me to apply this
control sequence to too much text. How can we recover?
My plan is to forget the whole thing and hope for the best.