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 setOption 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. It also checks for maxHeartbeats options being present which are not scoped to single commands.
• 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 anonymous functions, instead of the fun keyword: mathlib prefers the latter for reasons of readability
• the longFile linter checks for files which have more than 1500 lines
• the longLine linter checks for lines which have more than 100 characters
• the openClassical linter checks for open (scoped) Classical statements which are not scoped to a single declaration
• the show linter checks for shows that change the goal and should be replaced by change

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. It also warns on an option containing maxHeartbeats (as these should be scoped as set_option ... in instead).

def Mathlib.Linter.Style.setOption.parseSetOption : 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.isSetOption : Lean.Syntax → Bool

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

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

The setOption linter: this lints any set_option command, term or tactic which sets a debug, pp, profiler or trace option. This also warns if an option containing maxHeartbeats (typically, the maxHeartbeats or synthInstance.maxHeartbeats option) is set.

Why is this bad? The debug, pp, profiler and trace options are good for debugging, but should not be used in production code.

maxHeartbeats options should be scoped as set_option opt in ... (and be followed by a comment explaining the need for them; another linter enforces this).

How to fix this? The maxHeartbeats options can be scoped to individual commands, if they are truly necessary.

The debug, pp, profiler and trace are usually not necessary for production code, so you can simply remove them. (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 ·.

Equations

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

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.

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

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.

def Mathlib.Linter.Style.nameCheck.doubleUnderscore : Lean.Linter

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.

Equations

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

The "openClassical" linter

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

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.

def Mathlib.Linter.Style.openClassical.extractOpenNames : Lean.Syntax → Array (Lean.TSyntax `ident)

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.

def Mathlib.Linter.Style.openClassical.openClassicalLinter : Lean.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.

Equations

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

The "show" linter

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

The "show" linter emits a warning if the show tactic changed the goal. show should only be used to indicate intermediate goal states for proof readability. When the goal is actually changed, change should be preferred.

def Mathlib.Linter.Style.show.showLinter : Lean.Linter

The "show" linter emits a warning if the show tactic changed the goal. show should only be used to indicate intermediate goal states for proof readability. When the goal is actually changed, change should be preferred.

Equations

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