List of linters

Stream: mathlib4

[Sebastien Gouezel]

I'd like to try to define a new linter, that would complain if a lemma uses a [MetricSpace X] assumption but only uses the topology ofX in the statement, telling the user to use a [MetrizableSpace X] assumption instead. My idea was to get inspiration from another linter for decidable assumption which does roughly the same (if the assumption is only used in the proof, tell the user to use classical instead in the proof). But I can't find this linter in mathlib4 (I know it existed in mathlib3, but I don't know if it has been ported). When I went to the documentation to learn more about which linters we have, in https://leanprover-community.github.io/glossary.html#code-linter, the link a collection of Lean programs goes unfortunately to mathlib3 docs.

Is there a way to see a list of active linters? And do you know if the above decidable linter has been ported to Lean 4?

[Yaël Dillies]

Same thing as the fintypefinite linter, right?

[Yaël Dillies]

Could we also have enumerablecountable?

[Mario Carneiro]

#list_linters lists the available mathlib linters (this is import dependent)

[Sebastien Gouezel]

I have just found https://leanprover-community.github.io/mathlib4_docs/Std/Tactic/Lint/Frontend.html and the #list_linters command.

[Sebastien Gouezel]

It looks like the linter I was looking for has not been ported.

[Mario Carneiro]

it looks like mathlib currently has no linters at all, they are all in std now

[Mario Carneiro]

except for the structureInType linter

[Mario Carneiro]

Are the missing linters tracked anywhere? I don't see any conspicuously long comments containing lean 3 implementations

[Mario Carneiro]

mathlib3 has the following comment:

/--
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.
-/
add_tactic_doc
{ name                     := "linting commands",
  category                 := doc_category.cmd,
  decl_names               := [`lint_cmd, `lint_mathlib_cmd, `lint_all_cmd, `list_linters],
  tags                     := ["linting"] }

what ever happened to these notes? They seem to have been deleted in the port

[Mario Carneiro]

there are a few add_tactic_doc commands in mathlib4 (all commented out, because the PR which adds this command was never merged), but not nearly enough - there are 290 hits for add_tactic_doc in mathlib3 and 5 in mathlib4

[Sebastien Gouezel]

I am trying to update a little bit the mathlib documentation pages to mathlib 4. Doing this, I notice that the library notes are apparently not in mathlib 4 documentation. Am I missing something?

[Johan Commelin]

cc @Alex J. Best who had a general tool for detecting such issues (e.g. lemma about rings only uses group structure) in Lean 3.

[Mario Carneiro]

From the list of linters above, I found that the following linters are missing in lean 4:

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. has_nonempty_instance checks whether every type has an associated inhabited, unique
   or nonempty instance.

7. incorrect_type_class_argument checks for arguments in [square brackets] that are not classes.

8. dangerous_instance checks for instances that generate type-class problems with metavariables.
9. fails_quickly tests that type-class inference ends (relatively) quickly when applied to
   variables.
10. has_coe_variable tests that there are no instances of type has_coe α t for a variable α.
11. inhabited_nonempty checks for inhabited instance arguments that should be changed to
    nonempty.
12. 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.
13. has_coe_to_fun checks that every type that coerces to a function has a direct
    has_coe_to_fun instance.
14. check_reducibility checks whether non-instances with a class as type are reducible.
15. unprintable_interactive checks that interactive tactics have parser documentation.
16. to_additive_doc checks if additive versions of lemmas have documentation.

Additionally there are some more (non-default) linters which are not listed in the library note and which are also missing:

• assert_not_exists: A linter for checking that the declarations marked assert_not_exists eventually exist.
• assert_no_instance: A linter for checking that the declarations marked assert_no_instance eventually exist.

• class_structure: Checks that all uses of the @[class] attribute apply to structures or inductive types.
  This is future-proofing for lean 4, which no longer supports @[class] def.

• fintype_finite: Checks whether a declaration is Prop-valued and takes a fintype _
  hypothesis that is unused elsewhere in the type.
  In this case, that hypothesis can be replaced with casesI nonempty_fintype _ in the proof.

[Alex J. Best]

I hope to port my linter at some point, but probably it will only be in a couple of months from now.
Certainly that shouldn't stop people making useful intermediate versions though! If you know how the typeclass graph looks for some specific TCs it should be quite ok to fold over the proof term and look for whether you find any bare _inst_1 of that type if you stop searching whenever you hit instTopologyPseudoMetricSpace or whatever the specific edge you want to know if everything is passing through is. Of course it does start the get harder when you have multiple possible paths!

[Eric Wieser]

Regarding library notes; I think those are not implemented anywhere in lean 4: neither doc-gen4 or vscode knows about them