The "header" linter

The "header" style linter checks that a file starts with

/-
Copyright ...
Apache ...
Authors ...
-/

import statements*
module doc-string*
remaining file

It emits a warning if

• the copyright statement is malformed;
• Mathlib.Tactic is imported;
• any import in Lake is present;
• the first non-import command is not a module doc-string.

The linter allows import-only files and does not require a copyright statement in Mathlib.Init.

Implementation

The strategy used by the linter is as follows. The linter computes the end position of the first module doc-string of the file, resorting to the end of the file, if there is no module doc-string. Next, the linter tries to parse the file up to the position determined above.

If the parsing is successful, the linter checks the resulting Syntax and behaves accordingly.

If the parsing is not successful, this already means there is some "problematic" command after the imports. In particular, there is a command that is not a module doc-string immediately following the last import: the file should be flagged by the linter. Hence, the linter then falls back to parsing the header of the file, adding a spurious section after it. This makes it possible for the linter to check the entire header of the file, emit warnings that could arise from this part and also flag that the file should contain a module doc-string after the import statements.

def Mathlib.Linter.firstNonImport? : Lean.Syntax → Option Lean.Syntax

firstNonImport? stx assumes that the input Syntax is of kind Lean.Parser.Module.module. It returns

• none, if stx consists only of import statements,
• the first non-import command in stx, otherwise.

The intended use-case is to use the output of testParseModule as the input of firstNonImport?.

Equations

• Mathlib.Linter.firstNonImport? x✝ = match x✝ with | Lean.Syntax.node info `Lean.Parser.Module.module #[_header, Lean.Syntax.node info_1 `null args] => args[0]? | x => some Lean.Syntax.missing

partial def Mathlib.Linter.getImportIds (s : Lean.Syntax) : Array Lean.Syntax

getImportIds s takes as input s : Syntax. It returns the array of all import identifiers in s.

def Mathlib.Linter.parseUpToHere (pos : String.Pos) (post : String := "") : Lean.Elab.Command.CommandElabM Lean.Syntax

parseUpToHere pos post takes as input pos : String.Pos and the optional post : String. It parses the current file from the beginning until pos, appending post at the end. It returns a syntax node of kind Lean.Parser.Module.module. The option of appending a final string to the text gives more control to avoid syntax errors, for instance in the presence of #guard_msgs in or set_option ... in.

Note that this parsing will not be successful on every file. However, if the linter is parsing the file linearly, it will only need to parse

• the imports (that are always parseable) and
• the first non-import command that is supposed to be a module doc-string (so again always parseable).

In conclusion, either the parsing is successful, and the linter can continue with its analysis, or the parsing is not successful and the linter will flag a missing module doc-string!

Equations

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

def Mathlib.Linter.toSyntax (s pattern : String) (offset : String.Pos := 0) : Lean.Syntax

toSyntax s pattern converts the two input strings into a Syntax, assuming that pattern is a substring of s: the syntax is an atom with value pattern whose the range is the range of pattern in s.

Equations

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

def Mathlib.Linter.authorsLineChecks (line : String) (offset : String.Pos) : Array (Lean.Syntax × String)

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

The offset input is used to shift the position information of the Syntax that the command produces. authorsLineChecks computes a position for its warning relative to line. The offset input passes on the starting position of line in the whole file.

Equations

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

def Mathlib.Linter.copyrightHeaderChecks (copyright : String) : Array (Lean.Syntax × String)

The main function to validate the copyright string. The input is the copyright string, the output is an array of Syntax × String encoding:

• the Syntax factors are atoms whose ranges are "best guesses" for where the changes should take place; the embedded string is the current text that the linter flagged;
• the String factor is the linter message.

The linter checks that

• the first and last line of the copyright are a ("/-", "-/") pair, each on its own line;
• the first line is begins with Copyright (c) 20 and ends with . All rights reserved.;
• the second line is Released under Apache 2.0 license as described in the file LICENSE.;
• the remainder of the string begins with Authors: , does not end with . and contains no and nor a double space, except possibly after a line break.

Equations

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

def Mathlib.Linter.isInMathlib (modName : Lean.Name) : IO Bool

isInMathlib modName returns true if Mathlib.lean imports the file modName and false otherwise. This is used by the Header linter as a heuristic of whether it should inspect the file or not.

Equations

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

opaque Mathlib.Linter.inMathlibRef : IO.Ref (Option Bool)

inMathlibRef is

• none at initialization time;
• some true if the header linter has already discovered that the current file is imported in Mathlib.lean;
• some false if the header linter has already discovered that the current file is not imported in Mathlib.lean.

opaque Mathlib.Linter.linter.style.header : Lean.Option Bool

The "header" style linter checks that a file starts with

/-
Copyright ...
Apache ...
Authors ...
-/

import statements*
module doc-string*
remaining file

It emits a warning if

• the copyright statement is malformed;
• Mathlib.Tactic is imported;
• any import in Lake is present;
• the first non-import command is not a module doc-string.

The linter allows import-only files and does not require a copyright statement in Mathlib.Init.

def Mathlib.Linter.Style.header.broadImportsCheck (imports : Array Lean.Syntax) (mainModule : Lean.Name) : Lean.Elab.Command.CommandElabM Unit

Check the Syntax imports for broad imports: Mathlib.Tactic, any import starting with Lake, or Mathlib.Tactic.{Have,Replace}.

Equations

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

def Mathlib.Linter.Style.header.duplicateImportsCheck (imports : Array Lean.Syntax) : Lean.Elab.Command.CommandElabM Unit

Check the syntax imports for syntactically duplicate imports. The output is an array of Syntax atoms whose ranges are the import statements, and the embedded strings are the error message of the linter.

Equations

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

def Mathlib.Linter.Style.header.headerLinter : Lean.Linter

The "header" style linter checks that a file starts with

/-
Copyright ...
Apache ...
Authors ...
-/

import statements*
module doc-string*
remaining file

It emits a warning if

• the copyright statement is malformed;
• Mathlib.Tactic is imported;
• any import in Lake is present;
• the first non-import command is not a module doc-string.

The linter allows import-only files and does not require a copyright statement in Mathlib.Init.

Equations

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