Documentation

Mathlib.Tactic.Linter.TextBased

Text-based linters #

This file defines various mathlib linters which are based on reading the source code only. In practice, all such linters check for code style issues.

For now, this only contains linters checking

For historic reasons, some of these checks are still written in a Python script lint-style.py: these are gradually being rewritten in Lean.

This linter maintains a list of exceptions, for legacy reasons. Ideally, the length of the list of exceptions tends to 0.

The longFile and the longLine syntax linter take care of flagging lines that exceed the 100 character limit and files that exceed the 1500 line limit. The text-based versions of this file are still used for the files where the linter is not imported. This means that the exceptions for the text-based linters are shorter, as they do not need to include those handled with set_option linter.style.longFile x/set_option linter.longLine false.

An executable running all these linters is defined in scripts/lint-style.lean.

Different kinds of "broad imports" that are linted against.

Instances For

    Possible errors that text-based linters can report.

    Instances For

      How to format style errors

      Instances For

        Create the underlying error message for a given StyleError.

        Equations
        Instances For

          The error code for a given style error. Keep this in sync with parse?_errorContext below!

          Equations
          Instances For

            Context for a style error: the actual error, the line number in the file we're reading and the path to the file.

            Instances For

              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: Mathlib.Linter.TextBased.ComparisonResult

                The contexts describe different errors: two separate style exceptions are required to cover both.

              • Comparable: BoolMathlib.Linter.TextBased.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).

              Instances For

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

                  Find the first style exception in exceptions (if any) which covers a style exception e.

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

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

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

                        Parse all style exceptions for a line of input. Return an array of all exceptions which could be parsed: invalid input is ignored.

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

                          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
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[reducible, inline]

                            Core logic of a text based linter: given a collection of lines, return an array of all style errors with line numbers. If possible, also return the collection of all lines, changed as needed to fix the linter errors. (Such automatic fixes are only possible for some kinds of StyleErrors.)

                            Equations
                            Instances For

                              Definitions of the actual text-based linters.

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

                              Equations
                              Instances For

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

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

                                    Lint on a collection of input strings if one of the is a duplicate import statement.

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

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

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

                                          All text-based linters registered in this file.

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

                                            Read a file and apply all text-based linters. Return a list of all unexpected errors, and, if some errors could be fixed automatically, the collection of all lines with every automatic fix applied. exceptions are any pre-existing style exceptions for this file.

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

                                              Lint a collection of modules for style violations. Print formatted errors for all unexpected style violations to standard output; correct automatically fixable style errors 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, fix configures whether fixable errors should be corrected in-place.

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