Documentation

Mathlib.Tactic.Linter.Header

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

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

Instances For
    source
    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.

    source
    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.
    Instances For
      source
      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.
      Instances For
        source
        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.
        Instances For
          source
          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.
          Instances For
            source
            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.
            Instances For
              source
              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.

              source
              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, Mathlib.Tactic.{Have,Replace} or anything in the Deprecated folder.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                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.
                Instances For
                  source
                  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.
                  Instances For