Documentation

Std.Tactic.Lint.Frontend

Linter frontend and commands #

This file defines the linter commands which spot common mistakes in the code.

For a list of default / non-default linters, see the "Linting Commands" user command doc entry.

The command #list_linters prints a list of the names of all available linters.

You can append a * to any command (e.g. #lint* in Std) to omit the slow tests.

You can append a - to any command (e.g. #lint- in Std) to run a silent lint that suppresses the output if all checks pass. A silent lint will fail if any test fails.

You can append a + to any command (e.g. #lint+ in Std) to run a verbose lint that reports the result of each linter, including the successes.

You can append a sequence of linter names to any command to run extra tests, in addition to the default ones. e.g. #lint doc_blame_thm will run all default tests and doc_blame_thm.

You can append only name1 name2 ... to any command to run a subset of linters, e.g. #lint only unused_arguments in Std

You can add custom linters by defining a term of type Linter with the @[std_linter] attribute. A linter defined with the name Std.Tactic.Lint.myNewCheck can be run with #lint myNewCheck or #lint only myNewCheck. If you add the attribute @[std_linter disabled] to linter.myNewCheck it will be registered, but not run by default.

Adding the attribute @[nolint doc_blame unused_arguments] to a declaration omits it from only the specified linter checks.

Tags #

sanity check, lint, cleanup, command, tactic

Verbosity for the linter output.

Instances For

    getChecks slow extra use_only produces a list of linters. extras is a list of names that should resolve to declarations with type linter. If useOnly is true, it only uses the linters in extra. Otherwise, it uses all linters in the environment tagged with @[std_linter]. If slow is false, it only uses the fast default tests.

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

      Runs all the specified linters on all the specified declarations in parallel, producing a list of results.

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

        Sorts a map with declaration keys as names by line number.

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

          Formats a linter warning as #check command with comment.

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

            Formats a map of linter warnings using print_warning, sorted by line number.

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

              Formats a map of linter warnings grouped by filename with -- filename comments. The first drop_fn_chars characters are stripped from the filename.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                def Std.Tactic.Lint.formatLinterResults (results : Array (Std.Tactic.Lint.NamedLinter × Lean.HashMap Lean.Name Lean.MessageData)) (decls : Array Lean.Name) (groupByFilename : Bool) (whereDesc : String) (runSlowLinters : Bool) (verbose : Std.Tactic.Lint.LintVerbosity) (numLinters : Nat) (useErrorFormat : optParam Bool false) :

                Formats the linter results as Lean code with comments and #check commands.

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

                  Get the list of declarations in the current module.

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

                    Get the list of all declarations in the environment.

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

                      Get the list of all declarations in the specified package.

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

                        The in foo config argument allows running the linter on a specified project.

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

                          The command #lint runs the linters on the current file (by default).

                          #lint only someLinter can be used to run only a single linter.

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

                            The command #list_linters prints a list of all available linters.

                            Equations
                            Instances For