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 set_option linter checks for the presence of set_option commands activating options disallowed in mathlib: these are meant to be temporary, and not for polished code
• the missingEnd linter 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 cdotLinter linter checks for focusing dots · which are typed using a . instead: this is allowed Lean syntax, but it is nicer to be uniform
• the dollarSyntax linter 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 lambdaSyntax linter checks for uses of the λ symbol for ananomous functions, instead of the fun keyword: mathlib prefers the latter for reasons of readability (This linter is still under review in PR #15896.)
• the longLine linter checks for lines which have more than 100 characters
• the longFile linter checks for files which have more than 1500 lines: this linter is still under development in PR #15610.

All of these linters are enabled in mathlib by default, but disabled globally since they enforce conventions which are inherently subjective.

opaque Mathlib.Linter.linter.style.setOption : Lean.Option Bool

The setOption linter emits a warning on a set_option command, term or tactic which sets a pp, profiler or trace option.

def Mathlib.Linter.Style.setOption.parse_set_option : Lean.Syntax → Option Lean.Name

Whether a syntax element is a set_option command, tactic or term: Return the name of the option being set, if any.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Linter.Style.setOption.is_set_option : Lean.Syntax → Bool

Whether a given piece of syntax is a set_option command, tactic or term.

Equations

• Mathlib.Linter.Style.setOption.is_set_option stx = match Mathlib.Linter.Style.setOption.parse_set_option stx with | some _name => true | x => false

def Mathlib.Linter.Style.setOption.setOptionLinter : Lean.Linter

The setOption linter: this lints any set_option command, term or tactic which sets a pp, profiler or trace option.

Why is this bad? These options are good for debugging, but should not be used in production code. How to fix this? Remove these options: usually, they are not necessary for production code. (Some tests will intentionally use one of these options; in this case, simply allow the linter.)

Equations

• One or more equations did not get rendered due to their size.

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).

opaque Mathlib.Linter.linter.style.missingEnd : Lean.Option Bool

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).

def Mathlib.Linter.Style.missingEnd.missingEndLinter : Lean.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).

Equations

• One or more equations did not get rendered due to their size.

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.

opaque Mathlib.Linter.linter.style.cdot : Lean.Option Bool

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.

def Mathlib.Linter.isCDot? : Lean.Syntax → Bool

isCDot? stx checks whether stx is a Syntax node corresponding to a cdot typed with the character ·.

partial def Mathlib.Linter.findCDot : Lean.Syntax → Array Lean.Syntax

findCDot stx extracts from stx the syntax nodes of kind Lean.Parser.Term.cdot or cdotTk.

def Mathlib.Linter.unwanted_cdot (stx : Lean.Syntax) : Array Lean.Syntax

unwanted_cdot stx returns an array of syntax atoms within stx corresponding to cdots that are not written with the character ·. This is precisely what the cdot linter flags.

Equations

• Mathlib.Linter.unwanted_cdot stx = Array.filter (fun (x : Lean.Syntax) => !Mathlib.Linter.isCDot? x) (Mathlib.Linter.findCDot stx)

def Mathlib.Linter.Style.cdotLinter : Lean.Linter

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.

Equations

• One or more equations did not get rendered due to their size.

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 |>.

opaque Mathlib.Linter.linter.style.dollarSyntax : Lean.Option Bool

The dollarSyntax linter flags uses of <| that are achieved by typing $. These are disallowed by the mathlib style guide, as using <| pairs better with |>.

partial def Mathlib.Linter.Style.dollarSyntax.findDollarSyntax : Lean.Syntax → Array Lean.Syntax

findDollarSyntax stx extracts from stx the syntax nodes of kind $.

def Mathlib.Linter.Style.dollarSyntax.dollarSyntaxLinter : Lean.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 |>.

Equations

• One or more equations did not get rendered due to their size.

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.

opaque Mathlib.Linter.linter.style.lambdaSyntax : Lean.Option Bool

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.

partial def Mathlib.Linter.Style.lambdaSyntax.findLambdaSyntax : Lean.Syntax → Array Lean.Syntax

findLambdaSyntax stx extracts from stx all syntax nodes of kind Term.fun.

def Mathlib.Linter.Style.lambdaSyntax.lambdaSyntaxLinter : Lean.Linter

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.

Equations

• One or more equations did not get rendered due to their size.

The "longFile" linter

The "longFile" linter emits a warning on files which are longer than a certain number of lines (1500 by default).

opaque Mathlib.Linter.linter.style.longFile : Lean.Option Nat

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.

opaque Mathlib.Linter.linter.style.longFileDefValue : Lean.Option Nat

The number of lines that the longFile linter considers the default.

def Mathlib.Linter.Style.longFile.longFileLinter : Lean.Linter

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.

Equations

• One or more equations did not get rendered due to their size.

The "longLine linter"

opaque Mathlib.Linter.linter.style.longLine : Lean.Option Bool

The "longLine" linter emits a warning on lines longer than 100 characters. We allow lines containing URLs to be longer, though.

def Mathlib.Linter.Style.longLine.longLineLinter : Lean.Linter

The "longLine" linter emits a warning on lines longer than 100 characters. We allow lines containing URLs to be longer, though.

Equations

• One or more equations did not get rendered due to their size.