Style linters #
This file contain linters about stylistic aspects: these are only about coding style,
but do not affect correctness nor global coherence of mathlib.
Historically, some of these were ported from the lint-style.py Python script.
This file defines the following linters:
- the
setOptionlinter checks for the presence ofset_optioncommands activating options disallowed in mathlib: these are meant to be temporary, and not for polished code. It also checks formaxHeartbeatsoptions being present which are not scoped to single commands. - the
missingEndlinter checks for sections or namespaces which are not closed by the end of the file: enforcing this invariant makes minimising files or moving code between files easier - the
cdotLinterlinter checks for focusing dots·which are typed using a.instead: this is allowed Lean syntax, but it is nicer to be uniform - the
dollarSyntaxlinter checks for use of the dollar sign$instead of the<|pipe operator: similarly, both symbols have the same meaning, but mathlib prefers<|for the symmetry with the|>symbol - the
lambdaSyntaxlinter checks for uses of theλsymbol for anonymous functions, instead of thefunkeyword: mathlib prefers the latter for reasons of readability - the
longFilelinter checks for files which have more than 1500 lines - the
longLinelinter checks for lines which have more than 100 characters - the
openClassicallinter checks foropen (scoped) Classicalstatements which are not scoped to a single declaration - the
showlinter checks forshows that change the goal and should be replaced bychange
All of these linters are enabled in mathlib by default, but disabled globally since they enforce conventions which are inherently subjective.
The setOption linter emits a warning on a set_option command, term or tactic
which sets a pp, profiler or trace option.
It also warns on an option containing maxHeartbeats
(as these should be scoped as set_option ... in instead).
Whether a given piece of syntax is a set_option command, tactic or term.
Equations
- Mathlib.Linter.Style.setOption.isSetOption stx = match Mathlib.Linter.Style.setOption.parseSetOption✝ stx with | some _name => true | x => false
Instances For
The "missing end" linter #
The "missing end" linter emits a warning on non-closed sections and namespaces.
It allows the "outermost" noncomputable section to be left open (whether or not it is named).
The "missing end" linter emits a warning on non-closed sections and namespaces.
It allows the "outermost" noncomputable section to be left open (whether or not it is named).
The cdot linter #
The cdot linter is a syntax-linter that flags uses of the "cdot" · that are achieved
by typing a character different from ·.
For instance, a "plain" dot . is allowed syntax, but is flagged by the linter.
It also flags "isolated cdots", i.e. when the · is on its own line.
The cdot linter flags uses of the "cdot" · that are achieved by typing a character
different from ·.
For instance, a "plain" dot . is allowed syntax, but is flagged by the linter.
It also flags "isolated cdots", i.e. when the · is on its own line.
The dollarSyntax linter #
The dollarSyntax linter flags uses of <| that are achieved by typing $.
These are disallowed by the mathlib style guide, as using <| pairs better with |>.
The dollarSyntax linter flags uses of <| that are achieved by typing $.
These are disallowed by the mathlib style guide, as using <| pairs better with |>.
findDollarSyntax stx extracts from stx the syntax nodes of kind $.
The lambdaSyntax linter #
The lambdaSyntax linter is a syntax linter that flags uses of the symbol λ to define anonymous
functions, as opposed to the fun keyword. These are syntactically equivalent; mathlib style
prefers the latter as it is considered more readable.
The lambdaSyntax linter flags uses of the symbol λ to define anonymous functions.
This is syntactically equivalent to the fun keyword; mathlib style prefers using the latter.
findLambdaSyntax stx extracts from stx all syntax nodes of kind Term.fun.
The "longFile" linter #
The "longFile" linter emits a warning on files which are longer than a certain number of lines (1500 by default).
The "longFile" linter emits a warning on files which are longer than a certain number of lines
(linter.style.longFileDefValue by default on mathlib, no limit for downstream projects).
If this option is set to N lines, the linter warns once a file has more than N lines.
A value of 0 silences the linter entirely.
The number of lines that the longFile linter considers the default.
The "longLine linter" #
The "longLine" linter emits a warning on lines longer than 100 characters. We allow lines containing URLs to be longer, though.
The nameCheck linter emits a warning on declarations whose name is non-standard style.
(Currently, this only includes declarations whose name includes a double underscore.)
Why is this bad? Double underscores in theorem names can be considered non-standard style and probably have been introduced by accident. How to fix this? Use single underscores to separate parts of a name, following standard naming conventions.
The "openClassical" linter #
The "openClassical" linter emits a warning on open Classical statements which are not
scoped to a single declaration. A non-scoped open Classical can hide that some theorem statements
would be better stated with explicit decidability statements.
If stx is syntax describing an open command, extractOpenNames stx
returns an array of the syntax corresponding to the opened names,
omitting any renamed or hidden items.
This only checks independent open commands: for open ... in ... commands,
this linter returns an empty array.
Equations
- One or more equations did not get rendered due to their size.