Zulip Chat Archive

Stream: new members

Topic: Mathlib linter


view this post on Zulip Jakob Scholbach (Mar 30 2021 at 19:24):

Is there a document explaining the meanings of error messages spit out by the mathlib linter that runs once I push to a PR such as here https://github.com/leanprover-community/mathlib/pull/6852/checks?check_run_id=2229251959 (and ideally a few baby examples including examples how to salvage them)? Concretely, in my case I run into
/- UNUSED ARGUMENTS: -/ and /- TYPES ARE MISSING INHABITED INSTANCES: -/.

view this post on Zulip Patrick Massot (Mar 30 2021 at 19:33):

Unused argument is pretty self-explanatory, one definition or lemma has an unused argument. The other is more controversial but a Zulip search will give you many answers.

view this post on Zulip Patrick Massot (Mar 30 2021 at 19:33):

/- UNUSED ARGUMENTS: -/
-- category_theory/lifting_properties.lean
#print category_theory.right_lifting_subcat /- argument 4: (F : D → category_theory.arrow C) -/

view this post on Zulip Patrick Massot (Mar 30 2021 at 19:34):

That's what it says: the 4th arguments of category_theory.right_lifting_subcat, namely (F : D → category_theory.arrow C) is unused.

view this post on Zulip Patrick Massot (Mar 30 2021 at 19:35):

def right_lifting_subcat (F : D  arrow C) := C

I agree with the linter.

view this post on Zulip Jakob Scholbach (Mar 30 2021 at 19:38):

Thanks, in retrospect this is indeed obvious to spot.

view this post on Zulip Patrick Massot (Mar 30 2021 at 19:39):

The context doesn't help: those CI messages are very intimidating.

view this post on Zulip Greg Price (Mar 30 2021 at 19:45):

I've been curious about the inhabited linter too. Here's one recent explanation:

Johan Commelin said:

the inhabited-linter is there to force us to do some basic checks that we are not making stupid definitions. So when you write an instance to make it happy, it's best to try to make the example as "canonical" as possible. In other words, even if you can give an example for just X = nat, we encourage you to make it for every X, just like you did.

view this post on Zulip Greg Price (Mar 30 2021 at 19:47):

I'd be glad to have found that in docs somewhere. Would a library note be a good home for that kind of explanation? And then the linter output could include a link to that.

view this post on Zulip Greg Price (Mar 30 2021 at 19:47):

Meanwhile here's a somewhat different but perhaps complementary explanation:

Gabriel Ebner said:

The idea with the inhabited instances linter was to make sure that we have the obvious instances for inhabited (finset α), inhabited (α →₀ β), etc. (Quite a few were missing, actually.) You're not expected to add inhabited instances for α ≃ β, etc.

view this post on Zulip Greg Price (Mar 30 2021 at 19:49):

Oh and the latter was followed by:

Gabriel Ebner said:

Some people like the linter because it reminds you to add an example value of your new type.

which I think is a version of the explanation Johan Commelin gave that I quoted above.

view this post on Zulip Bryan Gin-ge Chen (Mar 30 2021 at 19:53):

I think most of the linting documentation we have at the moment is here. We could also expand that to add some motivation for the linters.

view this post on Zulip Patrick Massot (Mar 30 2021 at 19:55):

I also tried to find doc in the linter docstrings before answering and I found them pretty disappointing.

view this post on Zulip Greg Price (Mar 30 2021 at 20:03):

Yeah, the docstrings are pretty terse. I think that's fine as long as the good information is handy when you get the linter message printed at you, though -- that seems like the most important time for it to be shown. And if it's colocated in the code, it's almost as good as a docstring for the case when you're actually looking at the linter implementation, too.

Here's what the instance_priority linter has:

/-- checks whether an instance that always applies has priority ≥ 1000. -/
private meta def instance_priority (d : declaration) : tactic (option string) := do
-- …

/--
Certain instances always apply during type-class resolution. For example, the instance
`add_comm_group.to_add_group {α} [add_comm_group α] : add_group α` applies to all type-class
resolution problems of the form `add_group _`, and type-class inference will then do an
exhaustive search to find a commutative group. These instances take a long time to fail.
Other instances will only apply if the goal has a certain shape. For example
`int.add_group : add_group ℤ` or
`add_group.prod {α β} [add_group α] [add_group β] : add_group (α × β)`. Usually these instances
will fail quickly, and when they apply, they are almost the desired instance.
For this reason, we want the instances of the second type (that only apply in specific cases) to
always have higher priority than the instances of the first type (that always apply).
See also #1561.

Therefore, if we create an instance that always applies, we set the priority of these instances to
100 (or something similar, which is below the default value of 1000).
-/
library_note "lower instance priority"

/-- A linter object for checking instance priorities of instances that always apply.
This is in the default linter set. -/
@[linter] meta def linter.instance_priority : linter :=
{ test := instance_priority,
  no_errors_found := "All instance priorities are good",
  errors_found := "DANGEROUS INSTANCE PRIORITIES.
The following instances always apply, and therefore should have a priority < 1000.
If you don't know what priority to choose, use priority 100.
See note [lower instance priority] for instructions to change the priority.",
  auto_decls := tt }

Last updated: May 08 2021 at 19:11 UTC