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 historic reasons, some further such check 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.BroadImports : Type

Different kinds of "broad imports" that are linted against.

• TacticFolder : BroadImports

  Importing the entire "Mathlib.Tactic" folder

• Lake : BroadImports

  Importing any module in Lake, unless carefully measured This has caused unexpected regressions in the past.

instance Mathlib.Linter.TextBased.instBEqBroadImports : BEq BroadImports

Equations

• Mathlib.Linter.TextBased.instBEqBroadImports = { beq := Mathlib.Linter.TextBased.beqBroadImports✝ }

inductive Mathlib.Linter.TextBased.StyleError : Type

Possible errors that text-based linters can report.

• adaptationNote : StyleError

  The bare string "Adaptation note" (or variants thereof): instead, the #adaptation_note command should be used.

• windowsLineEnding : StyleError

  A line ends with windows line endings (\r\n) instead of unix ones (\n).

• trailingWhitespace : StyleError

  A line contains trailing whitespace.

• semicolon : StyleError

  A line contains a space before a semicolon

instance Mathlib.Linter.TextBased.instBEqStyleError : BEq StyleError

Equations

• Mathlib.Linter.TextBased.instBEqStyleError = { beq := Mathlib.Linter.TextBased.beqStyleError✝ }

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 humand-readable output

• github : ErrorFormat

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

instance Mathlib.Linter.TextBased.instBEqErrorFormat : BEq ErrorFormat

Equations

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

def Mathlib.Linter.TextBased.StyleError.errorMessage (err : StyleError) : String

Create the underlying error message for a given StyleError.

Equations

• Mathlib.Linter.TextBased.StyleError.adaptationNote.errorMessage = "Found the string \"Adaptation note:\", please use the #adaptation_note command instead"
• Mathlib.Linter.TextBased.StyleError.windowsLineEnding.errorMessage = "This line ends with a windows line ending (\x0d\n): please use Unix lineendings (\n) instead"
• Mathlib.Linter.TextBased.StyleError.trailingWhitespace.errorMessage = "This line ends with some whitespace: please remove this"
• Mathlib.Linter.TextBased.StyleError.semicolon.errorMessage = "This line contains a space before a semicolon"

def Mathlib.Linter.TextBased.StyleError.errorCode (err : StyleError) : String

The error code for a given style error. Keep this in sync with parse?_errorContext below!

Equations

• Mathlib.Linter.TextBased.StyleError.adaptationNote.errorCode = "ERR_ADN"
• Mathlib.Linter.TextBased.StyleError.windowsLineEnding.errorCode = "ERR_WIN"
• Mathlib.Linter.TextBased.StyleError.trailingWhitespace.errorCode = "ERR_TWS"
• Mathlib.Linter.TextBased.StyleError.semicolon.errorCode = "ERR_SEM"

structure Mathlib.Linter.TextBased.ErrorContext : Type

Context for a style error: the actual error, the line number in the file we're reading and the path to the file.

• error : StyleError

  The underlying StyleError

• lineNumber : ℕ

  The line number of the error (1-based)

• path : System.FilePath

  The path to the file which was linted

inductive Mathlib.Linter.TextBased.ComparisonResult : Type

Possible results of comparing an ErrorContext to an existing entry: most often, they are different --- if the existing entry covers the new exception, depending on the error, we prefer the new or the existing entry.

• Different : ComparisonResult

  The contexts describe different errors: two separate style exceptions are required to cover both.

• Comparable : ComparisonResult

  The existing exception also covers the new error: we keep the existing exception.

instance Mathlib.Linter.TextBased.instBEqComparisonResult : BEq ComparisonResult

Equations

• Mathlib.Linter.TextBased.instBEqComparisonResult = { beq := Mathlib.Linter.TextBased.beqComparisonResult✝ }

def Mathlib.Linter.TextBased.compare (existing new : ErrorContext) : ComparisonResult

Determine whether a new ErrorContext is covered by an existing exception, and, if it is, if we prefer replacing the new exception or keeping the previous one.

Equations

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

def Mathlib.Linter.TextBased.ErrorContext.find?_comparable (e : ErrorContext) (exceptions : Array ErrorContext) : Option ErrorContext

Find the first style exception in exceptions (if any) which covers a style exception e.

Equations

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

def Mathlib.Linter.TextBased.outputMessage (errctx : ErrorContext) (style : ErrorFormat) : String

Output the formatted error message, containing its context. style specifies if the error should be formatted for humans to read, github problem matchers to consume, or for the style exceptions file.

Equations

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

def Mathlib.Linter.TextBased.parse?_errorContext (line : String) : Option ErrorContext

Try parsing an ErrorContext from a string: return some if successful, none otherwise.

Equations

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

def Mathlib.Linter.TextBased.parseStyleExceptions (lines : Array String) : Array ErrorContext

Parse all style exceptions for a line of input. Return an array of all exceptions which could be parsed: invalid input is ignored.

Equations

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

def Mathlib.Linter.TextBased.formatErrors (errors : Array ErrorContext) (style : ErrorFormat) : IO Unit

Print information about all errors encountered to standard output. style specifies if the error should be formatted for humans to read, github problem matchers to consume, or for the style exceptions file.

Equations

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

@[reducible, inline]

abbrev Mathlib.Linter.TextBased.TextbasedLinter : Type

Core logic of a text based linter: given a collection of lines, return an array of all style errors with line numbers. If possible, also return the collection of all lines, changed as needed to fix the linter errors. (Such automatic fixes are only possible for some kinds of StyleErrors.)

Equations

• Mathlib.Linter.TextBased.TextbasedLinter = (Array String → Array (Mathlib.Linter.TextBased.StyleError × ℕ) × Option (Array String))

Definitions of the actual text-based linters.

def Mathlib.Linter.TextBased.adaptationNoteLinter : TextbasedLinter

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

Equations

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

def Mathlib.Linter.TextBased.trailingWhitespaceLinter : TextbasedLinter

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

Equations

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

def Mathlib.Linter.TextBased.semicolonLinter : TextbasedLinter

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

Equations

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

def Mathlib.Linter.TextBased.isImportsOnlyFile (lines : Array String) : Bool

Whether a collection of lines consists only of imports, blank lines and single-line comments. In practice, this means it's an imports-only file and exempt from almost all linting.

Equations

• Mathlib.Linter.TextBased.isImportsOnlyFile lines = lines.all fun (line : String) => line.startsWith "import " || line == "" || line.startsWith "-- "

def Mathlib.Linter.TextBased.allLinters : Array TextbasedLinter

All text-based linters registered in this file.

Equations

• Mathlib.Linter.TextBased.allLinters = #[Mathlib.Linter.TextBased.adaptationNoteLinter, Mathlib.Linter.TextBased.semicolonLinter, Mathlib.Linter.TextBased.trailingWhitespaceLinter]

def Mathlib.Linter.TextBased.lintFile (path : System.FilePath) (exceptions : Array ErrorContext) : IO (Array ErrorContext × Option (Array String))

Read a file and apply all text-based linters. Return a list of all unexpected errors, and, if some errors could be fixed automatically, the collection of all lines with every automatic fix applied. exceptions are any pre-existing style exceptions for this file.

Equations

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

def Mathlib.Linter.TextBased.lintModules (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. 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.