From 2c3067e91bd4eec9058d8f1be330db81c177d3dc Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 6 Jul 2021 11:34:07 +0200 Subject: [PATCH] doc: bundle updated `lean4.py` Pygments file and `lstlean.tex` --- doc/latex/lean4.py | 101 +++++++++++ doc/latex/lstlean.tex | 287 +++++++++++++++++++++++++++++++ doc/syntax_highlight_in_latex.md | 69 ++++++-- 3 files changed, 445 insertions(+), 12 deletions(-) create mode 100644 doc/latex/lean4.py create mode 100644 doc/latex/lstlean.tex diff --git a/doc/latex/lean4.py b/doc/latex/lean4.py new file mode 100644 index 0000000000..c5d10f6cca --- /dev/null +++ b/doc/latex/lean4.py @@ -0,0 +1,101 @@ +# -*- 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', 'exposing', 'parameter', 'parameters', + 'conjecture', 'hypothesis', 'lemma', 'corollary', 'variable', 'variables', + 'theorem', 'axiom', 'inductive', 'structure', 'universe', 'alias', + 'help', 'options', 'precedence', 'postfix', 'prefix', 'calc_trans', + 'calc_subst', 'calc_refl', 'infix', 'infixl', 'infixr', 'notation', '#eval', + '#check', '#reduce', '#exit', 'coercion', 'end', 'private', 'using', 'namespace', + 'including', 'instance', 'section', 'context', 'protected', 'expose', + 'export', 'set_option', 'add_rewrite', '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/latex/lstlean.tex b/doc/latex/lstlean.tex new file mode 100644 index 0000000000..c91a9d7e1e --- /dev/null +++ b/doc/latex/lstlean.tex @@ -0,0 +1,287 @@ +% Listing style definition for the Lean Theorem Prover. +% Defined by Jeremy Avigad, 2015, by modifying Assia Mahboubi's SSR style. +% Unicode replacements taken from Olivier Verdier's unixode.sty + +\lstdefinelanguage{lean} { + +% Anything betweeen $ becomes LaTeX math mode +mathescape=false, +% Comments may or not include Latex commands +texcl=false, + +% keywords, list taken from lean-syntax.el +morekeywords=[1]{ +import, prelude, protected, private, noncomputable, definition, meta, renaming, +hiding, exposing, parameter, parameters, begin, conjecture, constant, constants, +hypothesis, lemma, corollary, variable, variables, premise, premises, theory, +print, theorem, proposition, example, +open, as, export, override, axiom, axioms, inductive, with, without, +structure, record, universe, universes, +alias, help, precedence, reserve, declare_trace, add_key_equivalence, +match, infix, infixl, infixr, notation, postfix, prefix, instance, +eval, vm_eval, check, coercion, end, this, suppose, +using, using_well_founded, namespace, section, fields, +attribute, local, set_option, extends, include, omit, classes, class, +instances, coercions, attributes, raw, replacing, +calc, have, show, suffices, by, in, at, let, forall, Pi, fun, +exists, if, dif, then, else, assume, obtain, from, aliases, register_simp_ext, unless, break, continue, +mutual, do, def, run_cmd, const +partial,mut,where,macro,syntax,deriving, return, try, catch, for, macro_rules,declare_syntax_cat,abbrev}, + +% Sorts +morekeywords=[2]{Sort, Type, Prop}, + +% tactics, list taken from lean-syntax.el +morekeywords=[3]{ +assumption, +apply, intro, intros, allGoals, +generalize, clear, revert, done, exact, +refine, repeat, cases, rewrite, rw, +simp, simp_all, contradiction, +constructor, injection, +induction, +}, + +% modifiers, taken from lean-syntax.el +% note: 'otherkeywords' is needed because these use a different symbol. +% this command doesn't allow us to specify a number -- they are put with [1] +% otherkeywords={ +% [persistent], [notation], [visible], [instance], [trans_instance], +% [class], [parsing-only], [coercion], [unfold_full], [constructor], +% [reducible], [irreducible], [semireducible], [quasireducible], [wf], +% [whnf], [multiple_instances], [none], [decl], [declaration], +% [relation], [symm], [subst], [refl], [trans], [simp], [congr], [unify], +% [backward], [forward], [no_pattern], [begin_end], [tactic], [abbreviation], +% [reducible], [unfold], [alias], [eqv], [intro], [intro!], [elim], [grinder], +% [localrefinfo], [recursor] +% }, + +% Various symbols +literate= +{α}{{\ensuremath{\mathrm{\alpha}}}}1 +{β}{{\ensuremath{\mathrm{\beta}}}}1 +{γ}{{\ensuremath{\mathrm{\gamma}}}}1 +{δ}{{\ensuremath{\mathrm{\delta}}}}1 +{ε}{{\ensuremath{\mathrm{\varepsilon}}}}1 +{ζ}{{\ensuremath{\mathrm{\zeta}}}}1 +{η}{{\ensuremath{\mathrm{\eta}}}}1 +{θ}{{\ensuremath{\mathrm{\theta}}}}1 +{ι}{{\ensuremath{\mathrm{\iota}}}}1 +{κ}{{\ensuremath{\mathrm{\kappa}}}}1 +{μ}{{\ensuremath{\mathrm{\mu}}}}1 +{ν}{{\ensuremath{\mathrm{\nu}}}}1 +{ξ}{{\ensuremath{\mathrm{\xi}}}}1 +{π}{{\ensuremath{\mathrm{\mathnormal{\pi}}}}}1 +{ρ}{{\ensuremath{\mathrm{\rho}}}}1 +{σ}{{\ensuremath{\mathrm{\sigma}}}}1 +{τ}{{\ensuremath{\mathrm{\tau}}}}1 +{φ}{{\ensuremath{\mathrm{\varphi}}}}1 +{χ}{{\ensuremath{\mathrm{\chi}}}}1 +{ψ}{{\ensuremath{\mathrm{\psi}}}}1 +{ω}{{\ensuremath{\mathrm{\omega}}}}1 + +{Γ}{{\ensuremath{\mathrm{\Gamma}}}}1 +{Δ}{{\ensuremath{\mathrm{\Delta}}}}1 +{Θ}{{\ensuremath{\mathrm{\Theta}}}}1 +{Λ}{{\ensuremath{\mathrm{\Lambda}}}}1 +{Σ}{{\ensuremath{\mathrm{\Sigma}}}}1 +{Φ}{{\ensuremath{\mathrm{\Phi}}}}1 +{Ξ}{{\ensuremath{\mathrm{\Xi}}}}1 +{Ψ}{{\ensuremath{\mathrm{\Psi}}}}1 +{Ω}{{\ensuremath{\mathrm{\Omega}}}}1 + +{ℵ}{{\ensuremath{\aleph}}}1 + +{≤}{{\ensuremath{\leq}}}1 +{≥}{{\ensuremath{\geq}}}1 +{≠}{{\ensuremath{\neq}}}1 +{≈}{{\ensuremath{\approx}}}1 +{≡}{{\ensuremath{\equiv}}}1 +{≃}{{\ensuremath{\simeq}}}1 + +{≤}{{\ensuremath{\leq}}}1 +{≥}{{\ensuremath{\geq}}}1 + +{∂}{{\ensuremath{\partial}}}1 +{∆}{{\ensuremath{\triangle}}}1 % or \laplace? + +{∫}{{\ensuremath{\int}}}1 +{∑}{{\ensuremath{\mathrm{\Sigma}}}}1 +{Π}{{\ensuremath{\mathrm{\Pi}}}}1 + +{⊥}{{\ensuremath{\perp}}}1 +{∞}{{\ensuremath{\infty}}}1 +{∂}{{\ensuremath{\partial}}}1 + +{∓}{{\ensuremath{\mp}}}1 +{±}{{\ensuremath{\pm}}}1 +{×}{{\ensuremath{\times}}}1 + +{⊕}{{\ensuremath{\oplus}}}1 +{⊗}{{\ensuremath{\otimes}}}1 +{⊞}{{\ensuremath{\boxplus}}}1 + +{∇}{{\ensuremath{\nabla}}}1 +{√}{{\ensuremath{\sqrt}}}1 + +{⬝}{{\ensuremath{\cdot}}}1 +{•}{{\ensuremath{\cdot}}}1 +{∘}{{\ensuremath{\circ}}}1 + +%{⁻}{{\ensuremath{^{\textup{\kern1pt\rule{2pt}{0.3pt}\kern-1pt}}}}}1 +{⁻}{{\ensuremath{^{-}}}}1 +{▸}{{\ensuremath{\blacktriangleright}}}1 + +{∧}{{\ensuremath{\wedge}}}1 +{∨}{{\ensuremath{\vee}}}1 +{¬}{{\ensuremath{\neg}}}1 +{⊢}{{\ensuremath{\vdash}}}1 + +%{⟨}{{\ensuremath{\left\langle}}}1 +%{⟩}{{\ensuremath{\right\rangle}}}1 +{⟨}{{\ensuremath{\langle}}}1 +{⟩}{{\ensuremath{\rangle}}}1 + +{↦}{{\ensuremath{\mapsto}}}1 +{←}{{\ensuremath{\leftarrow}}}1 +{<-}{{\ensuremath{\leftarrow}}}1 +{→}{{\ensuremath{\rightarrow}}}1 +{↔}{{\ensuremath{\leftrightarrow}}}1 +{⇒}{{\ensuremath{\Rightarrow}}}1 +{⟹}{{\ensuremath{\Longrightarrow}}}1 +{⇐}{{\ensuremath{\Leftarrow}}}1 +{⟸}{{\ensuremath{\Longleftarrow}}}1 + +{∩}{{\ensuremath{\cap}}}1 +{∪}{{\ensuremath{\cup}}}1 +{⊂}{{\ensuremath{\subseteq}}}1 +{⊆}{{\ensuremath{\subseteq}}}1 +{⊄}{{\ensuremath{\nsubseteq}}}1 +{⊈}{{\ensuremath{\nsubseteq}}}1 +{⊃}{{\ensuremath{\supseteq}}}1 +{⊇}{{\ensuremath{\supseteq}}}1 +{⊅}{{\ensuremath{\nsupseteq}}}1 +{⊉}{{\ensuremath{\nsupseteq}}}1 +{∈}{{\ensuremath{\in}}}1 +{∉}{{\ensuremath{\notin}}}1 +{∋}{{\ensuremath{\ni}}}1 +{∌}{{\ensuremath{\notni}}}1 +{∅}{{\ensuremath{\emptyset}}}1 + +{∖}{{\ensuremath{\setminus}}}1 +{†}{{\ensuremath{\dag}}}1 + +{ℕ}{{\ensuremath{\mathbb{N}}}}1 +{ℤ}{{\ensuremath{\mathbb{Z}}}}1 +{ℝ}{{\ensuremath{\mathbb{R}}}}1 +{ℚ}{{\ensuremath{\mathbb{Q}}}}1 +{ℂ}{{\ensuremath{\mathbb{C}}}}1 +{⌞}{{\ensuremath{\llcorner}}}1 +{⌟}{{\ensuremath{\lrcorner}}}1 +{⦃}{{\ensuremath{\{\!|}}}1 +{⦄}{{\ensuremath{|\!\}}}}1 + +{‖}{{\ensuremath{\|}}}1 +{₁}{{\ensuremath{_1}}}1 +{₂}{{\ensuremath{_2}}}1 +{₃}{{\ensuremath{_3}}}1 +{₄}{{\ensuremath{_4}}}1 +{₅}{{\ensuremath{_5}}}1 +{₆}{{\ensuremath{_6}}}1 +{₇}{{\ensuremath{_7}}}1 +{₈}{{\ensuremath{_8}}}1 +{₉}{{\ensuremath{_9}}}1 +{₀}{{\ensuremath{_0}}}1 +{ᵢ}{{\ensuremath{_i}}}1 +{ⱼ}{{\ensuremath{_j}}}1 +{ₐ}{{\ensuremath{_a}}}1 + +{¹}{{\ensuremath{^1}}}1 + +{ₙ}{{\ensuremath{_n}}}1 +{ₘ}{{\ensuremath{_m}}}1 +{↑}{{\ensuremath{\uparrow}}}1 +{↓}{{\ensuremath{\downarrow}}}1 + +{...}{{\ensuremath{\ldots}}}1 +{·}{{\ensuremath{\cdot}}}1 + +{▸}{{\ensuremath{\triangleright}}}1 + +{Σ}{{\color{symbolcolor}\ensuremath{\Sigma}}}1 +{Π}{{\color{symbolcolor}\ensuremath{\Pi}}}1 +{∀}{{\color{symbolcolor}\ensuremath{\forall}}}1 +{∃}{{\color{symbolcolor}\ensuremath{\exists}}}1 +{λ}{{\color{symbolcolor}\ensuremath{\mathrm{\lambda}}}}1 +{\$}{{\color{symbolcolor}\$}}1 + +{:=}{{\color{symbolcolor}:=}}1 +{=}{{\color{symbolcolor}=}}1 +{<|>}{{\color{symbolcolor}<|>}}1 +{<\$>}{{\color{symbolcolor}<\$>}}1 +{+}{{\color{symbolcolor}+}}1 +{*}{{\color{symbolcolor}*}}1, + +% Comments +%comment=[s][\itshape \color{commentcolor}]{/-}{-/}, +morecomment=[s][\color{commentcolor}]{/-}{-/}, +morecomment=[l][\itshape \color{commentcolor}]{--}, + +% Spaces are not displayed as a special character +showstringspaces=false, + +% keep spaces +keepspaces=true, + +% String delimiters +morestring=[b]", +morestring=[d]’, + +% Size of tabulations +tabsize=3, + +% Enables ASCII chars 128 to 255 +extendedchars=false, + +% Case sensitivity +sensitive=true, + +% Automatic breaking of long lines +breaklines=true, +breakatwhitespace=true, + +% Default style fors listingsred +basicstyle=\ttfamily\small, + +% Position of captions is bottom +captionpos=b, + +% Full flexible columns +columns=[l]fullflexible, + + +% Style for (listings') identifiers +identifierstyle={\ttfamily\color{black}}, +% Note : highlighting of Coq identifiers is done through a new +% delimiter definition through an lstset at the begining of the +% document. Don't know how to do better. + +% Style for declaration keywords +keywordstyle=[1]{\ttfamily\color{keywordcolor}}, + +% Style for sorts +keywordstyle=[2]{\ttfamily\color{sortcolor}}, + +% Style for tactics keywords +keywordstyle=[3]{\ttfamily\color{tacticcolor}}, + +% Style for attributes +keywordstyle=[4]{\ttfamily\color{attributecolor}}, + +% Style for strings +stringstyle=\ttfamily, + +% Style for comments +commentstyle={\ttfamily\footnotesize }, + +} diff --git a/doc/syntax_highlight_in_latex.md b/doc/syntax_highlight_in_latex.md index 21405b9e19..212e3886e1 100644 --- a/doc/syntax_highlight_in_latex.md +++ b/doc/syntax_highlight_in_latex.md @@ -1,34 +1,79 @@ -The [Pygments](https://pygments.org/) syntax highlighting library has official support for Lean (however, Lean 4 keywords have not been added yet), which can be used in LaTeX via the [`minted`](https://ctan.org/pkg/minted) package. +You can copy highlighted code [straight from VS Code](https://code.visualstudio.com/updates/v1_10#_copy-with-syntax-highlighting) to any rich text editor supporting HTML input. For highlighting code in LaTeX, there are two options: +* [listings](https://ctan.org/pkg/listings), which is a common package and simple to set up, but you may run into some restrictions of it and LaTeX around Unicode +* [`minted`](https://ctan.org/pkg/minted), a LaTeX package wrapping the [Pygments](https://pygments.org/) syntax highlighting library. It needs a few more steps to set up, but provides unrestricted support for Unicode when combined with XeLaTeX or LuaLaTex. -# Example +## Example with `listings` -Save the following sample LaTeX file as `test.tex`: +Save [`lstlean.tex`](https://raw.githubusercontent.com/leanprover/lean4/master/doc/latex/lstlean.tex) into the same directory, or anywhere in your `TEXINPUTS` path, as the following test file: +```latex +\documentclass{article} +\usepackage[T1]{fontenc} +\usepackage[utf8]{inputenc} +\usepackage{listings} + +\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} + +\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} +\end{document} +``` +Compile the file via +```bash +$ pdflatex test.tex +``` + +* for older LaTeX versions, you might need to use `[utf8x]` instead of `[utf8]` with `inputenc` + +## 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: ```latex \documentclass{article} -\usepackage{minted} \usepackage{fontspec} -\setmainfont{FreeSerif} +% switch to a monospace font supporting more Unicode characters \setmonofont{FreeMono} -\usepackage{fullpage} +\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} + \begin{document} +% some example options \begin{minted}[mathescape, linenos, numbersep=5pt, frame=lines, framesep=2mm]{Lean} -theorem mul_cancel_left_or {a b c : ℤ} (H : a * b = a * c) : a = 0 ∨ b = c := -have H2 : a * (b - c) = 0, by simp, -have H3 : a = 0 ∨ b - c = 0, from mul_eq_zero H2, -or.imp_or_right H3 (assume H4 : b - c = 0, sub_eq_zero H4) +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{minted} \end{document} ``` -You can compile `test.tex` by executing the following command: +You can then compile `test.tex` by executing the following command: ```bash -xelatex --shell-escape test +xelatex --shell-escape test.tex ``` Some remarks: