mathlib documentation

tactic.lint.frontend

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_mathlib: check all declarations in mathlib (so excluding core or other projects, and also excluding the current file)
#lint_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_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]

def lint_verbosity.inhabited :

inhabited lint_verbosity

@[protected, instance]

def lint_verbosity.decidable_eq :

decidable_eq lint_verbosity

meta def get_checks (slow : bool) (extra : list name) (use_only : bool) :

tactic (list (name × linter))

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)) :

tactic (list (name × linter × native.rb_map name string))

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 print_warning (decl_name : name) (warning : string) :

Formats a linter warning as #check command with comment.

def escape_workflow_command (s : string) :

Escape characters that may not be used in a workflow commands, following https://github.com/actions/toolkit/blob/7257597d731b34d14090db516d9ea53439300e98/packages/core/src/command.ts#L92-L105

Equations

escape_workflow_command s = "".intercalate (list.map workflow_command_replacements s.to_list)

meta def print_workflow_command (env : environment) (linter_name decl_name : name) (warning : string) :

Prints a workflow command to emit an error understood by github in an actions workflow. This enables CI to tag the parts of the file where linting failed with annotations, and makes it easier for mathlib contributors to see what needs fixing. See https://docs.github.com/en/actions/learn-github-actions/workflow-commands-for-github-actions#setting-an-error-message

meta def print_warnings (env : environment) (emit_workflow_commands : bool) (linter_name : name) (results : native.rb_map name string) :

Formats a map of linter warnings using print_warning, sorted 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 string → format) :

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 : ℕ) (emit_workflow_commands : bool := ff) :

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

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

tactic (name_set × format)

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) :

tactic (name_set × format)

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

meta def lint_project_decls (proj_folder : string) :

tactic (list declaration)

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) :

tactic (name_set × format)

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) :

tactic (name_set × format)

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

meta def parse_lint_additions :

lean.parser (bool × list name)

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

meta def parse_verbosity :

lean.parser (option lint_verbosity)

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

meta def lint_cmd_aux (scope : bool → lint_verbosity → list name → bool → tactic (name_set × format)) :

lean.parser unit

The common denominator of lint_cmd, lint_mathlib_cmd, lint_all_cmd

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

lean.parser unit

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")) :

lean.parser unit

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")) :

lean.parser unit

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")) :

lean.parser unit

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

meta def lint_hole_cmd :

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.