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.

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

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.