mathlib3 documentation

tactic.lint.default

Default linters #

This file defines the list of linters that are run in mathlib CI. Not all linters are considered "default" and run that way. A linter is marked as default if it is tagged with the linter attribute.

User commands to 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)

The following linters are run by default:

  1. unused_arguments checks for unused arguments in declarations.
  2. def_lemma checks whether a declaration is incorrectly marked as a def/lemma.
  3. dup_namespce checks whether a namespace is duplicated in the name of a declaration.
  4. ge_or_gt checks whether ≥/> is used in the declaration.
  5. instance_priority checks that instances that always apply have priority below default.
  6. doc_blame checks for missing doc strings on definitions and constants.
  7. has_nonempty_instance checks whether every type has an associated inhabited, unique or nonempty instance.
  8. impossible_instance checks for instances that can never fire.
  9. incorrect_type_class_argument checks for arguments in [square brackets] that are not classes.
  10. dangerous_instance checks for instances that generate type-class problems with metavariables.
  11. fails_quickly tests that type-class inference ends (relatively) quickly when applied to variables.
  12. has_coe_variable tests that there are no instances of type has_coe α t for a variable α.
  13. inhabited_nonempty checks for inhabited instance arguments that should be changed to nonempty.
  14. simp_nf checks that the left-hand side of simp lemmas is in simp-normal form.
  15. simp_var_head checks that there are no variables as head symbol of left-hand sides of simp lemmas.
  16. simp_comm checks that no commutativity lemmas (such as add_comm) are marked simp.
  17. decidable_classical checks for decidable hypotheses that are used in the proof of a proposition but not in the statement, and could be removed using classical. Theorems in the decidable namespace are exempt.
  18. has_coe_to_fun checks that every type that coerces to a function has a direct has_coe_to_fun instance.
  19. check_type checks that the statement of a declaration is well-typed.
  20. check_univs checks that there are no bad max u v universe levels.
  21. syn_taut checks that declarations are not syntactic tautologies.
  22. check_reducibility checks whether non-instances with a class as type are reducible.
  23. unprintable_interactive checks that interactive tactics have parser documentation.
  24. to_additive_doc checks if additive versions of lemmas have documentation.

The following linters are not run by default:

  1. doc_blame_thm, checks for missing doc strings on lemmas and theorems.
  2. explicit_vars_of_iff checks if there are explicit variables used on both sides of an iff.

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.

meta def mathlib_linters  :

The default linters used in mathlib CI.