This file defines the following user commands to spot common mistakes in the code.
The following linters are run by default:
Another linter, doc_blame_thm, checks for missing doc strings on lemmas and theorems. This is not run by default.
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 of passing checks. A silent lint will fail if any test fails.
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] to a declaration omits it from all linter checks.
sanity check, lint, cleanup, command, tactic
Defines the user attribute nolint for skipping #lint
A linting test for the #lint command.
test defines a test to perform on every declaration. It should never fail. Returning none signifies a passing test. Returning some msg reports a failing test with error msg.
no_errors_found is the message printed when all tests are negative, and errors_found is printed when at least one test is positive.
If is_fast is false, this test will be omitted from #lint-.
Takes a list of names that resolve to declarations of type linter, and produces a list of linters.
Defines the user attribute linter for adding a linter to the default set. Linters should be defined in the linter namespace. A linter linter.my_new_linter is referred to as my_new_linter (without the linter namespace) when used in #lint.
Find all declarations in l where tac returns some x and list them.
Find all declarations in l where tac returns some x and sort the resulting list by file name.
Make the output of fold_over_with_cond printable, in the following form: #print <name> <open multiline comment> <elt of α> <close multiline comment>
Make the output of fold_over_with_cond_sorted printable, with the file path + name inserted.
Same as print_decls_sorted, but removing the first n characters from the string. Useful for omitting the mathlib directory from the output.
Auxilliary definition for check_unused_arguments
Check which arguments of a declaration are not used. Prints a list of natural numbers corresponding to which arguments are not used (e.g. this outputs [1, 4] if the first and fourth arguments are unused). Checks both the type and the value of d for whether the argument is used (in rare cases an argument is used in the type but not in the value). We return [] if the declaration was automatically generated. We print arguments that are larger than the arity of the type of the declaration (without unfolding definitions).
Check for unused arguments, and print them with their position, variable name, type and whether the argument is a duplicate. See also check_unused_arguments. This tactic additionally filters out all unused arguments of type parse _
A linter object for checking for unused arguments. This is in the default linter set.
Checks whether the correct declaration constructor (definition or theorem) by comparing it to its sort. Instances will not be printed.
A linter for checking whether the correct declaration constructor (definition or theorem) has been used.
Checks whether a declaration has a namespace twice consecutively in its name
A linter for checking whether a declaration has a namespace twice consecutively in its name.
Checks whether a >/≥ is used in the statement of d.
A linter for checking whether illegal constants (≥, >) appear in a declaration's type.
checks whether an instance that always applies has priority ≥ 1000.
A linter object for checking instance priorities of instances that always apply. This is in the default linter set.
Reports definitions and constants that are missing doc strings
Reports definitions and constants that are missing doc strings
A linter for checking definition doc strings
A linter for checking theorem doc strings. This is not in the default linter set.
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.
If verbose is true, return old ++ new, else return old.
The common denominator of #lint[|mathlib|all]. The different commands have different configurations for l, printer 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.
Return the message printed by #lint.
Return the message printed by #lint_mathlib.
Return the message printed by #lint_all.
Parses an optional only, followed by a sequence of zero or more identifiers. Prepends linter. to each of these identifiers.
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 of passing checks. Use the command #list_linters to see all available linters.
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 of passing checks. Use the command #list_linters to see all available linters.
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 of passing checks. Use the command #list_linters to see all available linters.
The command #list_linters prints a list of all available linters.
Use lint as a hole command. Note: In a large file, there might be some delay between choosing the option and the information appearing