From f0471a519ba70f4e5fdc0d4386ee0f50fe52f55b Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 20 May 2024 12:40:24 +0100 Subject: [PATCH] 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) --- doc/latex/lean4.py | 100 ------------------------------- doc/syntax_highlight_in_latex.md | 30 +++++----- 2 files changed, 15 insertions(+), 115 deletions(-) delete mode 100644 doc/latex/lean4.py diff --git a/doc/latex/lean4.py b/doc/latex/lean4.py deleted file mode 100644 index a75b26b5a9..0000000000 --- a/doc/latex/lean4.py +++ /dev/null @@ -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 `_ - 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'), - ], - } diff --git a/doc/syntax_highlight_in_latex.md b/doc/syntax_highlight_in_latex.md index 251fd5c3f8..07155e9449 100644 --- 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.