Linter frontend and commands #
This file defines the linter commands which spot common mistakes in the code.
#lint
: check all declarations in the current file#lint in Pkg
: check all declarations in the packagePkg
(so excluding core or other projects, and also excluding the current file)#lint in all
: check all declarations in the environment (the current file and all imported files)
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 Batteries
) to omit the slow tests.
You can append a -
to any command (e.g. #lint- in Batteries
) 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 Batteries
) 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 Batteries
You can add custom linters by defining a term of type Linter
with the
@[env_linter]
attribute.
A linter defined with the name Batteries.Tactic.Lint.myNewCheck
can be run with #lint myNewCheck
or #lint only myNewCheck
.
If you add the attribute @[env_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.
- low : LintVerbosity
low
: only print failing checks, print nothing on success. - medium : LintVerbosity
medium
: only print failing checks, print confirmation on success. - high : LintVerbosity
high
: print output of every check.
Instances For
Equations
getChecks slow runOnly runAlways
produces a list of linters.
runOnly
is an optional list of names that should resolve to declarations with type NamedLinter
.
If populated, only these linters are run (regardless of the default configuration).
runAlways
is an optional list of names that should resolve to declarations with type
NamedLinter
. If populated, these linters are always run (regardless of their configuration).
Specifying a linter in runAlways
but not runOnly
is an error.
Otherwise, it uses all enabled linters in the environment tagged with @[env_linter]
.
If slow
is false, it only uses the fast default tests.
Equations
Instances For
Runs all the specified linters on all the specified declarations in parallel, producing a list of results.
Equations
Instances For
Sorts a map with declaration keys as names by line number.
Equations
Instances For
Formats a linter warning as #check
command with comment.
Equations
Instances For
Formats a map of linter warnings using print_warning
, sorted by line number.
Equations
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
Instances For
Formats the linter results as Lean code with comments and #check
commands.
Equations
Instances For
Get the list of declarations in the current module.
Equations
Instances For
Get the list of all declarations in the environment.
Equations
Instances For
Get the list of all declarations in the specified package.
Equations
Instances For
The in foo
config argument allows running the linter on a specified project.
Equations
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
Instances For
The command #list_linters
prints a list of all available linters.