max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: bundle updated lean4.py Pygments file and lstlean.tex

Browse source
This commit is contained in:
Sebastian Ullrich 2021-07-06 11:34:07 +02:00 • committed by Leonardo de Moura
parent 7dc3e72bcb
commit 2c3067e91b
3 changed files with 445 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

101
doc/latex/lean4.py Normal file
View file

@ -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 <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', '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'),
],
}

287
doc/latex/lstlean.tex Normal file
View file

@ -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 },
}

69
doc/syntax_highlight_in_latex.md
View file

@ -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: