Text-based linters

This file defines various mathlib linters which are based on reading the source code only. In practice, all such linters check for code style issues.

Currently, this file contains linters checking

• if the string "adaptation note" is used instead of the command #adaptation_note,
• for lines with windows line endings,
• for lines containing trailing whitespace,
• for module names to be in upper camel case,
• for module names to be valid Windows filenames, and containing no forbidden characters such as !, . or spaces.

For historic reasons, some further such checks are written in a Python script lint-style.py: these are gradually being rewritten in Lean.

This linter has a file for style exceptions (to avoid false positives in the implementation), or for downstream projects to allow a gradual adoption of this linter.

An executable running all these linters is defined in scripts/lint-style.lean.

inductive Mathlib.Linter.TextBased.ErrorFormat : Type

How to format style errors

• humanReadable : ErrorFormat

  Produce style error output aimed at humans: no error code, clickable file name

• exceptionsFile : ErrorFormat

  Produce an entry in the style-exceptions file: mention the error code, slightly uglier than human-readable output

• github : ErrorFormat

  Produce output suitable for Github error annotations: in particular, duplicate the file path, line number and error code

def Mathlib.Linter.TextBased.instBEqErrorFormat.beq : ErrorFormat → ErrorFormat → Bool

Equations

• Mathlib.Linter.TextBased.instBEqErrorFormat.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Mathlib.Linter.TextBased.instBEqErrorFormat : BEq ErrorFormat

Equations

• Mathlib.Linter.TextBased.instBEqErrorFormat = { beq := Mathlib.Linter.TextBased.instBEqErrorFormat.beq }

Definitions of the actual text-based linters.

opaque Mathlib.Linter.TextBased.linter.adaptationNote : Lean.Option Bool

Lint on any occurrences of the string "Adaptation note:" or variants thereof.

opaque Mathlib.Linter.TextBased.linter.trailingWhitespace : Lean.Option Bool

Lint a collection of input strings if one of them contains trailing whitespace.

opaque Mathlib.Linter.TextBased.linter.whitespaceBeforeSemicolon : Lean.Option Bool

Lint a collection of input strings for a semicolon preceded by a space.

opaque Mathlib.Linter.TextBased.linter.nonbreakingSpace : Lean.Option Bool

Lint a collection of input strings for a non-breaking space character.

opaque Mathlib.Linter.TextBased.linter.pythonStyle : Lean.Option Bool

Enables the old Python-based style linters.

def Mathlib.Linter.TextBased.lintModules (opts : Lean.Linter.LinterOptions) (nolints : Array String) (moduleNames : Array Lean.Name) (style : ErrorFormat) (fix : Bool) : IO UInt32

Lint a collection of modules for style violations. Print formatted errors for all unexpected style violations to standard output; correct automatically fixable style errors if configured so. Return the number of files which had new style errors. opts contains the options defined in the Lakefile, determining which linters to enable. nolints is a list of style exceptions to take into account. moduleNames are the names of all the modules to lint, mode specifies what kind of output this script should produce, fix configures whether fixable errors should be corrected in-place.

Equations

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

opaque Mathlib.Linter.TextBased.linter.modulesUpperCamelCase : Lean.Option Bool

Verify that all modules are named in UpperCamelCase

def Mathlib.Linter.TextBased.modulesNotUpperCamelCase (opts : Lean.Linter.LinterOptions) (modules : Array Lean.Name) : IO ℕ

Verifies that all modules in modules are named in UpperCamelCase (except for explicitly discussed exceptions, which are hard-coded here). Return the number of modules violating this.

Equations

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

opaque Mathlib.Linter.TextBased.linter.modulesForbiddenWindows : Lean.Option Bool

Verify that no module name is forbidden according to Windows' filename rules.

def Mathlib.Linter.TextBased.modulesOSForbidden (opts : Lean.Linter.LinterOptions) (modules : Array Lean.Name) : IO ℕ

Verifies that no module in modules contains CON, PRN, AUX, NUL, COM1, COM2, COM3, COM4, COM5, COM6, COM7, COM8, COM9, COM¹, COM², COM³, LPT1, LPT2, LPT3, LPT4, LPT5, LPT6, LPT7, LPT8, LPT9, LPT¹, LPT² or LPT³ in its filename, as these are forbidden on Windows.

Also verify that module names contain no forbidden characters such as *, ? (Windows), ! (forbidden on Nix OS) or . (might result from confusion with a module name).

Source: https://learn.microsoft.com/en-gb/windows/win32/fileio/naming-a-file. Return the number of module names violating this rule.

Equations

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