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

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