Text-based linters

This file defines various mathlib linters which are based on reading the source code only. In practice, only style linters will have this form. All of these have been rewritten from the lint-style.py script.

For now, this only contains the linters for the copyright and author headers and large files: further linters will be ported in subsequent PRs.

An executable running all these linters is defined in scripts/lint_style.lean.

inductive 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 instBEqBroadImports : BEq BroadImports

Equations

• instBEqBroadImports = { beq := beqBroadImports✝ }

inductive StyleError : Type

Possible errors that text-based linters can report.

• copyright: Option String → StyleError

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

• authors: StyleError

  Malformed authors line in the copyright header

• adaptationNote: StyleError

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

• broadImport: BroadImports → StyleError

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

• fileTooLong: ℕ → ℕ → StyleError

  The current file was too large: this error contains the current number of lines as well as a size limit (slightly larger). On future runs, this linter will allow this file to grow up to this limit.

instance instBEqStyleError : BEq StyleError

Equations

• instBEqStyleError = { beq := beqStyleError✝ }

inductive 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 instBEqErrorFormat : BEq ErrorFormat

Equations

• instBEqErrorFormat = { beq := beqErrorFormat✝ }

def StyleError.errorMessage (err : StyleError) (style : ErrorFormat) : String

Create the underlying error message for a given StyleError.

Equations

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

def StyleError.errorCode (err : StyleError) : String

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

Equations

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

structure 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

def StyleError.normalise (err : StyleError) : StyleError

The parts of a StyleError which are considered when matching against the existing style exceptions: for example, we ignore the particular line length of a "line too long" error.

Equations

• err.normalise = match err with | StyleError.fileTooLong number_lines new_size_limit => StyleError.fileTooLong 0 0 | StyleError.copyright context => StyleError.copyright none | x => err

instance instBEqErrorContext : BEq ErrorContext

Careful: we do not want to compare ErrorContexts exactly; we ignore some details.

Equations

• instBEqErrorContext = { beq := fun (ctx ctx' : ErrorContext) => ctx.path == ctx'.path && ctx.error.normalise == ctx'.error.normalise }

def 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 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 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

• parseStyleExceptions lines = Id.run (Array.filterMap (fun (x : String) => parse?_errorContext x) (Array.filter (fun (line : String) => !line.startsWith "--") lines 0) 0)

def 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

• formatErrors errors style = do forIn errors PUnit.unit fun (e : ErrorContext) (r : PUnit) => do IO.println (outputMessage e style) pure (ForInStep.yield PUnit.unit) pure PUnit.unit

@[reducible, inline]

abbrev TextbasedLinter : Type

Core logic of a text based linter: given a collection of lines, return an array of all style errors with line numbers.

Equations

• TextbasedLinter = (Array String → Array (StyleError × ℕ))

Definitions of the actual text-based linters.

def isCorrectAuthorsLine (line : String) : Bool

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

Equations

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

def copyrightHeaderLinter : 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 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 broadImportsLinter : 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 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

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

def checkFileLength (lines : Array String) (existing_limit : Option ℕ) : Option StyleError

Error if a collection of lines is too large. "Too large" means more than 1500 lines and longer than an optional previous limit. If the file is too large, return a matching StyleError, which includes a new size limit (which is somewhat larger than the current size).

Equations

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

def allLinters : Array TextbasedLinter

All text-based linters registered in this file.

Equations

• allLinters = #[copyrightHeaderLinter, adaptationNoteLinter, broadImportsLinter]

def lintFile (path : System.FilePath) (sizeLimit : Option ℕ) (exceptions : Array ErrorContext) : IO (Array ErrorContext)

Read a file and apply all text-based linters. Return a list of all unexpected errors. sizeLimit is any pre-existing limit on this file's size. exceptions are any other style exceptions.

Equations

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

def lintModules (moduleNames : Array String) (style : ErrorFormat) : IO UInt32

Lint a collection of modules for style violations. Print formatted errors for all unexpected style violations to standard output. Return the number of files which had new style errors. 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.