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 linter checks if it is linting the first command or not by (quickly) parsing the imports, and checking whether the end position of the header is the same as the start position of the current command. If so, it re-parses the header more slowly and checks that the current (first) command is a module doc-string (unless the command is exempted for some reason).

def Mathlib.Linter.copyrightHeaderChecks (copyright expectedLicense : 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 equals expectedLicense (determined by the linter.style.header.license option, defaults to the Mathlib default);
• 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.

opaque Mathlib.Linter.linter.style.header.license : Lean.Option String

The text required by linter.style.header as the second line of the header.