mathlib documentation

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_mathlib*) to omit the slow tests (4).

You can append a - to any command (e.g. #lint_mathlib-) 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_mathlib+) 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

You can add custom linters by defining a term of type linter in the linter namespace. A linter defined with the name linter.my_new_check can be run with #lint my_new_check or lint only my_new_check. If you add the attribute @[linter] to linter.my_new_check it will 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

inductive lint_verbosity  :
Type

Verbosity for the linter output.

  • low: only print failing checks, print nothing on success.
  • medium: only print failing checks, print confirmation on success.
  • high: print output of every check.
@[protected, instance]
meta def get_checks (slow : bool) (extra : list name) (use_only : bool) :

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

meta def lint_core (all_decls non_auto_decls : list declaration) (checks : list (name × linter)) :

lint_core all_decls non_auto_decls checks applies the linters checks to the list of declarations. If auto_decls is false for a linter (default) the linter is applied to non_auto_decls. If auto_decls is true, then it is applied to all_decls. The resulting list has one element for each linter, containing the linter as well as a map from declaration name to warning.

meta def sort_results {α : Type} (e : environment) (results : native.rb_map name α) :
list (name × α)

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

meta def grouped_by_filename (e : environment) (results : native.rb_map name string) (drop_fn_chars : := 0) (formatter : native.rb_map name stringformat) :

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

meta def format_linter_results (env : environment) (results : list (name × linter × native.rb_map name string)) (decls non_auto_decls : list declaration) (group_by_filename : option ) (where_desc : string) (slow : bool) (verbose : lint_verbosity) (num_linters : ) :

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

meta def lint_aux (decls : list declaration) (group_by_filename : option ) (where_desc : string) (slow : bool) (verbose : lint_verbosity) (checks : list (name × linter)) :

The common denominator of #lint[|mathlib|all]. The different commands have different configurations for l, group_by_filename and where_desc. If slow is false, doesn't do the checks that take a lot of time. If verbose is false, it will suppress messages from passing checks. By setting checks you can customize which checks are performed.

Returns a name_set containing the names of all declarations that fail any check in check, and a format object describing the failures.

meta def lint (slow : bool := tt) (verbose : lint_verbosity := lint_verbosity.medium) (extra : list name := list.nil) (use_only : bool := ff) :

Return the message printed by #lint and a name_set containing all declarations that fail.

meta def lint_project_decls (proj_folder : string) :

Returns the declarations in the folder proj_folder.

meta def lint_project (proj_folder proj_name : string) (slow : bool := tt) (verbose : lint_verbosity := lint_verbosity.medium) (extra : list name := list.nil) (use_only : bool := ff) :

Returns the linter message by running the linter on all declarations in project proj_name in folder proj_folder. It also returns a name_set containing all declarations that fail.

To add a linter command for your own project, write

open lean.parser lean tactic interactive
@[user_command] meta def lint_my_project_cmd (_ : parse $ tk "#lint_my_project") : parser unit :=
do str  get_project_dir n k, lint_cmd_aux (@lint_project str "my project")

Here n is the name of any declaration in the project (like `lint_my_project_cmd and k is the number of characters in the filename of n after the src/ directory (so e.g. the number of characters in tactic/lint/frontend.lean). Warning: the linter will not work in the file where n is declared.

meta def lint_all (slow : bool := tt) (verbose : lint_verbosity := lint_verbosity.medium) (extra : list name := list.nil) (use_only : bool := ff) :

Return the message printed by #lint_all and a name_set containing all declarations that fail.

Parses an optional only, followed by a sequence of zero or more identifiers. Prepends linter. to each of these identifiers.

Parses a "-" or "+", returning lint_verbosity.low or lint_verbosity.high respectively, or returns none.

meta def lint_cmd_aux (scope : boollint_verbositylist namebooltactic (name_set × format)) :

The common denominator of lint_cmd, lint_mathlib_cmd, lint_all_cmd

The command #lint at the bottom of a file will warn you about some common mistakes in that file. Usage: #lint, #lint linter_1 linter_2, #lint only linter_1 linter_2. #lint- will suppress the output if all checks pass. #lint+ will enable verbose output.

Use the command #list_linters to see all available linters.

meta def lint_mathlib_cmd (_x : interactive.parse (lean.parser.tk "#lint_mathlib")) :

The command #lint_mathlib checks all of mathlib for certain mistakes. Usage: #lint_mathlib, #lint_mathlib linter_1 linter_2, #lint_mathlib only linter_1 linter_2. #lint_mathlib- will suppress the output if all checks pass. lint_mathlib+ will enable verbose output.

Use the command #list_linters to see all available linters.

meta def lint_all_cmd (_x : interactive.parse (lean.parser.tk "#lint_all")) :

The command #lint_all checks all imported files for certain mistakes. Usage: #lint_all, #lint_all linter_1 linter_2, #lint_all only linter_1 linter_2. #lint_all- will suppress the output if all checks pass. lint_all+ will enable verbose output.

Use the command #list_linters to see all available linters.

meta def list_linters (_x : interactive.parse (lean.parser.tk "#list_linters")) :

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

Invoking the hole command lint ("Find common mistakes in current file") will print text that indicates mistakes made in the file above the command. It is equivalent to copying and pasting the output of #lint. On large files, it may take some time before the output appears.