Linters for Mathlib

In this file we define additional linters for mathlib.

Perhaps these should be moved to Batteries in the future.

def Batteries.Tactic.Lint.structureInType : Batteries.Tactic.Lint.Linter

Linter that checks whether a structure should be in Prop.

Equations

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

def Batteries.Tactic.Lint.deprecatedNoSince : Batteries.Tactic.Lint.Linter

Linter that check that all deprecated tags come with since dates.

Equations

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

dupNamespace linter

The dupNamespace linter produces a warning when a declaration contains the same namespace at least twice consecutively.

For instance, Nat.Nat.foo and One.two.two trigger a warning, while Nat.One.Nat does not.

opaque Mathlib.Linter.linter.dupNamespace : Lean.Option Bool

The dupNamespace linter is set on by default. Lean emits a warning on any declaration that contains the same namespace at least twice consecutively.

For instance, Nat.Nat.foo and One.two.two trigger a warning, while Nat.One.Nat does not.

Note. This linter will not detect duplication in namespaces of autogenerated declarations (other than the one whose declId is present in the source declaration).

partial def Mathlib.Linter.DupNamespaceLinter.getIds : Lean.Syntax → Array Lean.Syntax

getIds stx extracts the declId nodes from the Syntax stx. If stx is an alias or an export, then it extracts an ident, instead of a declId.

def Mathlib.Linter.DupNamespaceLinter.dupNamespace : Lean.Linter

The dupNamespace linter is set on by default. Lean emits a warning on any declaration that contains the same namespace at least twice consecutively.

For instance, Nat.Nat.foo and One.two.two trigger a warning, while Nat.One.Nat does not.

Note. This linter will not detect duplication in namespaces of autogenerated declarations (other than the one whose declId is present in the source declaration).

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