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)

• lineLength: Int → StyleError

  Line longer than 100 characters

• fileTooLong: ℕ → ℕ → Option ℕ → 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. For diagnostic purposes, this may also contain a previous size limit, which is now exceeded.

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

inductive 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: Bool → 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 instBEqComparisonResult : BEq ComparisonResult

Equations

• instBEqComparisonResult = { beq := beqComparisonResult✝ }

def compare (existing : ErrorContext) (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 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

• e.find?_comparable exceptions = exceptions.find? fun (new : ErrorContext) => match _root_.compare e new with | ComparisonResult.Comparable preferExisting => true | x => false

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

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 lineLengthLinter : TextbasedLinter

Iterates over a collection of strings, finding all lines which are longer than 101 chars. We allow URLs to be longer, though.

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

def checkFileLength (lines : Array String) (existingLimit : 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, lineLengthLinter]

inductive OutputSetting : Type

Controls what kind of output this programme produces.

• print: ErrorFormat → OutputSetting

  Print any style error to standard output (the default)

• update: OutputSetting

  Update the style exceptions file (and still print style errors to standard output). This adds entries for any new exceptions, removes any entries which are no longer necessary, and tries to not modify exception entries unless necessary. To fully regenerate the exceptions file, delete style-exceptions.txt and run again in this mode.

instance instBEqOutputSetting : BEq OutputSetting

Equations

• instBEqOutputSetting = { beq := beqOutputSetting✝ }

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) (mode : OutputSetting) : IO UInt32

Lint a collection of modules for style violations. Print formatted errors for all unexpected style violations to standard output; update the list of style exceptions 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.

Equations

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