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.

For now, this only contains linters checking

• that the copyright header and authors line are correctly formatted
• existence of module docstrings (in the right place)
• for certain disallowed imports
• if the string "adaptation note" is used instead of the command #adaptation_note
• files are at most 1500 lines long (unless specifically allowed).

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

This linter maintains a list of exceptions, for legacy reasons. Ideally, the length of the list of exceptions tends to 0.

The longFile and the longLine syntax linter take care of flagging lines that exceed the 100 character limit and files that exceed the 1500 line limit. The text-based versions of this file are still used for the files where the linter is not imported. This means that the exceptions for the text-based linters are shorter, as they do not need to include those handled with set_option linter.style.longFile x/set_option linter.longLine false.

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: Mathlib.Linter.TextBased.BroadImports

  Importing the entire "Mathlib.Tactic" folder

• Lake: Mathlib.Linter.TextBased.BroadImports

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

instance Mathlib.Linter.TextBased.instBEqBroadImports : BEq Mathlib.Linter.TextBased.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.

• copyright: Option String → Mathlib.Linter.TextBased.StyleError

  Missing or malformed copyright header. Unlike in the python script, we may provide some context on the actual error.

• authors: Mathlib.Linter.TextBased.StyleError

  Malformed authors line in the copyright header

• adaptationNote: Mathlib.Linter.TextBased.StyleError

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

• broadImport: Mathlib.Linter.TextBased.BroadImports → Mathlib.Linter.TextBased.StyleError

  Lint against "too broad" imports, such as Mathlib.Tactic or any module in Lake (unless carefully measured)

• windowsLineEnding: Mathlib.Linter.TextBased.StyleError

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

instance Mathlib.Linter.TextBased.instBEqStyleError : BEq Mathlib.Linter.TextBased.StyleError

Equations

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

inductive Mathlib.Linter.TextBased.ErrorFormat : Type

How to format style errors

• humanReadable: Mathlib.Linter.TextBased.ErrorFormat

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

• exceptionsFile: Mathlib.Linter.TextBased.ErrorFormat

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

• github: Mathlib.Linter.TextBased.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 Mathlib.Linter.TextBased.ErrorFormat

Equations

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

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

Create the underlying error message for a given StyleError.

Equations

• One or more equations did not get rendered due to their size.
• (Mathlib.Linter.TextBased.StyleError.copyright (some context)).errorMessage = toString "Malformed or missing copyright header: " ++ toString context ++ toString ""
• (Mathlib.Linter.TextBased.StyleError.copyright none).errorMessage = "Malformed or missing copyright header"
• Mathlib.Linter.TextBased.StyleError.authors.errorMessage = "Authors line should look like: 'Authors: Jean Dupont, Иван Иванович Иванов'"
• Mathlib.Linter.TextBased.StyleError.adaptationNote.errorMessage = "Found the string \"Adaptation note:\", please use the #adaptation_note command instead"
• (Mathlib.Linter.TextBased.StyleError.broadImport Mathlib.Linter.TextBased.BroadImports.TacticFolder).errorMessage = "Files in mathlib cannot import the whole tactic folder"
• Mathlib.Linter.TextBased.StyleError.windowsLineEnding.errorMessage = "This line ends with a windows line ending (\x0d\n): please use Unix lineendings (\n) instead"

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

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

Equations

• (Mathlib.Linter.TextBased.StyleError.copyright context).errorCode = "ERR_COP"
• Mathlib.Linter.TextBased.StyleError.authors.errorCode = "ERR_AUT"
• Mathlib.Linter.TextBased.StyleError.adaptationNote.errorCode = "ERR_ADN"
• (Mathlib.Linter.TextBased.StyleError.broadImport module).errorCode = "ERR_IMP"
• Mathlib.Linter.TextBased.StyleError.windowsLineEnding.errorCode = "ERR_WIN"

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 : Mathlib.Linter.TextBased.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: Mathlib.Linter.TextBased.ComparisonResult

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

• Comparable: Bool → Mathlib.Linter.TextBased.ComparisonResult

  The existing exception also covers the new error. Indicate whether we prefer keeping the existing exception (the more common case) or would rather replace it by the new exception (this is more rare, and currently only happens for particular file length errors).

instance Mathlib.Linter.TextBased.instBEqComparisonResult : BEq Mathlib.Linter.TextBased.ComparisonResult

Equations

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

def Mathlib.Linter.TextBased.compare (existing : Mathlib.Linter.TextBased.ErrorContext) (new : Mathlib.Linter.TextBased.ErrorContext) : Mathlib.Linter.TextBased.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 : Mathlib.Linter.TextBased.ErrorContext) (exceptions : Array Mathlib.Linter.TextBased.ErrorContext) : Option Mathlib.Linter.TextBased.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 : Mathlib.Linter.TextBased.ErrorContext) (style : Mathlib.Linter.TextBased.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 Mathlib.Linter.TextBased.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 Mathlib.Linter.TextBased.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 Mathlib.Linter.TextBased.ErrorContext) (style : Mathlib.Linter.TextBased.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.isCorrectAuthorsLine (line : String) : Bool

Return if line looks like a correct authors line in a copyright header.

Equations

• Mathlib.Linter.TextBased.isCorrectAuthorsLine line = (line.startsWith "Authors: " && !line.containsSubstr " ".toSubstring && !line.containsSubstr " and ".toSubstring && !line.endsWith ".")

def Mathlib.Linter.TextBased.copyrightHeaderLinter : Mathlib.Linter.TextBased.TextbasedLinter

Lint a collection of input lines if they are missing an appropriate copyright header.

A copyright header should start at the very beginning of the file and contain precisely five lines, including the copy year and holder, the license and main author(s) of the file (in this order).

Equations

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

def Mathlib.Linter.TextBased.adaptationNoteLinter : Mathlib.Linter.TextBased.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.broadImportsLinter : Mathlib.Linter.TextBased.TextbasedLinter

Lint a collection of input strings if one of them contains an unnecessarily broad import.

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 Mathlib.Linter.TextBased.TextbasedLinter

All text-based linters registered in this file.

Equations

• Mathlib.Linter.TextBased.allLinters = #[Mathlib.Linter.TextBased.copyrightHeaderLinter, Mathlib.Linter.TextBased.adaptationNoteLinter, Mathlib.Linter.TextBased.broadImportsLinter]

def Mathlib.Linter.TextBased.lintFile (path : System.FilePath) (exceptions : Array Mathlib.Linter.TextBased.ErrorContext) : IO (Array Mathlib.Linter.TextBased.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 (moduleNames : Array String) (style : Mathlib.Linter.TextBased.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. moduleNames are 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.