doc: upstream the Lean4 pygments lexer (#3125)

An improved `lean4` lexer is now part of pygments. This depends on https://github.com/pygments/pygments/pull/2618 (now merged), and [a subsequent release](https://github.com/pygments/pygments/milestone/23)
2026-03-17 10:24:07 +00:00 · 2024-05-20 12:40:24 +01:00
parent 42215cc072
commit f0471a519b
2 changed files with 15 additions and 115 deletions
--- a/doc/latex/lean4.py
+++ b/doc/latex/lean4.py
@@ -1,100 +0,0 @@
-# -*- coding: utf-8 -*-
-"""
-    pygments.lexers.theorem
-    ~~~~~~~~~~~~~~~~~~~~~~~
-
-    Lexers for theorem-proving languages.
-
-    :copyright: Copyright 2006-2017 by the Pygments team, see AUTHORS.
-    :license: BSD, see LICENSE for details.
-"""
-
-import re
-
-from pygments.lexer import RegexLexer, default, words
-from pygments.token import Text, Comment, Operator, Keyword, Name, String, \
-    Number, Punctuation, Generic
-
-__all__ = ['Lean4Lexer']
-
-class Lean4Lexer(RegexLexer):
-    """
-    For the `Lean 4 <https://github.com/leanprover/lean4>`_
-    theorem prover.
-
-    .. versionadded:: 2.0
-    """
-    name = 'Lean4'
-    aliases = ['lean4']
-    filenames = ['*.lean']
-    mimetypes = ['text/x-lean']
-
-    flags = re.MULTILINE | re.UNICODE
-
-    keywords1 = (
-        'import', 'abbreviation', 'opaque_hint', 'tactic_hint', 'definition',
-        'renaming', 'inline', 'hiding', 'parameter', 'lemma', 'variable',
-        'theorem', 'axiom', 'inductive', 'structure', 'universe', 'alias',
-        'help', 'options', 'precedence', 'postfix', 'prefix',
-        'infix', 'infixl', 'infixr', 'notation', '#eval',
-        '#check', '#reduce', '#exit', 'coercion', 'end', 'private', 'using', 'namespace',
-        'including', 'instance', 'section', 'context', 'protected', 'expose',
-        'export', 'set_option', 'extends', 'open', 'example',
-        'constant', 'constants', 'print', 'opaque', 'reducible', 'irreducible',
-        'def', 'macro', 'elab', 'syntax', 'macro_rules', 'reduce', 'where',
-        'abbrev', 'noncomputable', 'class', 'attribute', 'synth', 'mutual',
-    )
-
-    keywords2 = (
-        'forall', 'fun', 'Pi', 'obtain', 'from', 'have', 'show', 'assume',
-        'take', 'let', 'if', 'else', 'then', 'by', 'in', 'with', 'begin',
-        'proof', 'qed', 'calc', 'match', 'nomatch', 'do', 'at',
-    )
-
-    keywords3 = (
-        # Sorts
-        'Type', 'Prop', 'Sort',
-    )
-
-    operators = (
-        u'!=', u'#', u'&', u'&&', u'*', u'+', u'-', u'/', u'@', u'!', u'`',
-        u'-.', u'->', u'.', u'..', u'...', u'::', u':>', u';', u';;', u'<',
-        u'<-', u'=', u'==', u'>', u'_', u'|', u'||', u'~', u'=>', u'<=', u'>=',
-        u'/\\', u'\\/', u'∀', u'Π', u'λ', u'↔', u'∧', u'∨', u'≠', u'≤', u'≥',
-        u'¬', u'⁻¹', u'⬝', u'▸', u'→', u'∃', u'ℕ', u'ℤ', u'≈', u'×', u'⌞',
-        u'⌟', u'≡', u'⟨', u'⟩',
-    )
-
-    punctuation = (u'(', u')', u':', u'{', u'}', u'[', u']', u'⦃', u'⦄',
-                   u':=', u',')
-
-    tokens = {
-        'root': [
-            (r'\s+', Text),
-            (r'/-', Comment, 'comment'),
-            (r'--.*?$', Comment.Single),
-            (words(keywords1, prefix=r'\b', suffix=r'\b'), Keyword.Namespace),
-            (words(keywords2, prefix=r'\b', suffix=r'\b'), Keyword),
-            (words(keywords3, prefix=r'\b', suffix=r'\b'), Keyword.Type),
-            (words(operators), Name.Builtin.Pseudo),
-            (words(punctuation), Operator),
-            (u"[A-Za-z_\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2100-\u214f]"
-             u"[A-Za-z_'\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2070-\u2079"
-             u"\u207f-\u2089\u2090-\u209c\u2100-\u214f0-9]*", Name),
-            (r'\d+', Number.Integer),
-            (r'"', String.Double, 'string'),
-            (r'[~?][a-z][\w\']*:', Name.Variable)
-        ],
-        'comment': [
-            # Multiline Comments
-            (r'[^/-]', Comment.Multiline),
-            (r'/-', Comment.Multiline, '#push'),
-            (r'-/', Comment.Multiline, '#pop'),
-            (r'[/-]', Comment.Multiline)
-        ],
-        'string': [
-            (r'[^\\"]+', String.Double),
-            (r'\\[n"\\]', String.Escape),
-            ('"', String.Double, '#pop'),
-        ],
-    }
--- a/doc/syntax_highlight_in_latex.md
+++ b/doc/syntax_highlight_in_latex.md
@@ -43,7 +43,8 @@ $ pdflatex test.tex

 ## Example with `minted`

-First [install Pygments](https://pygments.org/download/). Then save [`lean4.py`](https://raw.githubusercontent.com/leanprover/lean4/master/doc/latex/lean4.py), which contains an version of the Lean highlighter updated for Lean 4, and the following sample LaTeX file `test.tex` into the same directory:
+First [install Pygments](https://pygments.org/download/) (version 2.18 or newer).
+Then save the following sample LaTeX file `test.tex` into the same directory:

 ```latex
 \documentclass{article}
@@ -51,9 +52,8 @@ First [install Pygments](https://pygments.org/download/). Then save [`lean4.py`]
 % 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}
+\newmintinline[lean]{lean4}{bgcolor=white}
+\newminted[leancode]{lean4}{fontsize=\footnotesize}
 \usemintedstyle{tango}  % a nice, colorful theme

 \begin{document}
@@ -67,9 +67,6 @@ theorem funext {f₁ f₂ : ∀ (x : α), β x} (h : ∀ x, f₁ x = f₂ x) : f
 \end{document}
 ```

-If your version of `minted` is v2.7 or newer, but before v3.0,
-you will additionally need to follow the workaround described in https://github.com/gpoore/minted/issues/360.
-
 You can then compile `test.tex` by executing the following command:

 ```bash
@@ -81,11 +78,14 @@ Some remarks:
 - either `xelatex` or `lualatex` is required to handle Unicode characters in the code.
 - `--shell-escape` is needed to allow `xelatex` to execute `pygmentize` in a shell.
 - If the chosen monospace font is missing some Unicode symbols, you can direct them to be displayed using a fallback font or other replacement LaTeX code.
-``` latex
-\usepackage{newunicodechar}
-\newfontfamily{\freeserif}{DejaVu Sans}
-\newunicodechar{✝}{\freeserif{✝}}
-\newunicodechar{𝓞}{\ensuremath{\mathcal{O}}}
-```
- - minted has a "helpful" feature that draws red boxes around characters the chosen lexer doesn't recognize.
- Since the Lean lexer cannot encompass all user-defined syntax, it is advisable to [work around](https://tex.stackexchange.com/a/343506/14563) this feature.
+   ``` latex
+   \usepackage{newunicodechar}
+   \newfontfamily{\freeserif}{DejaVu Sans}
+   \newunicodechar{✝}{\freeserif{✝}}
+   \newunicodechar{𝓞}{\ensuremath{\mathcal{O}}}
+   ```
+ - If you are using an old version of Pygments, you can copy 
+   [`lean.py`](https://raw.githubusercontent.com/pygments/pygments/master/pygments/lexers/lean.py) into your working directory,
+   and use `lean4.py:Lean4Lexer -x` instead of `lean4` above.
+   If your version of `minted` is v2.7 or newer, but before v3.0,
+   you will additionally need to follow the workaround described in https://github.com/gpoore/minted/issues/360.