Mathlib linter

Stream: new members

[Jakob Scholbach]

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: -/.

[Patrick Massot]

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.

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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

I agree with the linter.

[Jakob Scholbach]

Thanks, in retrospect this is indeed obvious to spot.

[Patrick Massot]

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

[Greg Price]

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.

[Greg Price]

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.

[Greg Price]

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.

[Greg Price]

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.

[Bryan Gin-ge Chen]

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.

[Patrick Massot]

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

[Greg Price]

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 }

[Nicolò Cavalleri]

In #7803, Lint gives the following error

/- The `has_coe_to_fun` linter reports: -/
/- INVALID/MISSING `has_coe_to_fun` instances.
You should add a `has_coe_to_fun` instance for the following types.
See Note [function coercion]. -/

However, the error is not seen when I write #lint at the end of any of the files involved. Is there a way to work around this? I have multiple ideas to fix the problem, but it will be hard to experiment if each time I need to wait more than 3 hours for Github to build and lint...

[Alex J. Best]

I can see the error locally if I import import combinatorics.simple_graph.basic in bundle.lean and run #lint at the bottom, I guess its an error that only occurs when both (or all) files are imported.

[Nicolò Cavalleri]

Alex J. Best said:

I can see the error locally if I import import combinatorics.simple_graph.basic in bundle.lean and run #lint at the bottom, I guess its an error that only occurs when both (or all) files are imported.

Ok thanks!!

[Nicolò Cavalleri]

@Alex J. Best actually yesterday I said thanks but I did not try it... I can't see the error the way you say neither the other way around, i.e. importing bundle.lean in combinatorics.simple_graph.basic... what Lint error did you see? it might be another one...

[Alex J. Best]

@Nicolò Cavalleri Sorry I think its the other way around :face_palm: if I import data.bundle in cominatorics/simple_graph/basic.lean then do #lint at the end i see:

/- The `has_coe_to_fun` linter reports: -/
/- INVALID/MISSING `has_coe_to_fun` instances.
You should add a `has_coe_to_fun` instance for the following types.
See Note [function coercion]. -/
#print simple_graph.locally_finite /- `has_coe_to_fun` instance is definitionally equal to a transitive instance composed of:
  @right_inv.has_coe_to_fun.{u u}
    (@bundle.total_space.{u u} V
       (λ (v : V),
          fintype.{u}
            (@coe_sort.{(max (u+1) 1) (max 1 (u+1))+1} (set.{u} V) (@set.has_coe_to_sort.{u} V)
               (@simple_graph.neighbor_set.{u} V G v))))
    V
    (@bundle.proj.{u u} V
       (λ (v : V),
          fintype.{u}
            (@coe_sort.{(max (u+1) 1) (max 1 (u+1))+1} (set.{u} V) (@set.has_coe_to_sort.{u} V)
               (@simple_graph.neighbor_set.{u} V G v))))
and
  @coe_base_aux.{u+1 u+1} (@simple_graph.locally_finite.{u} V G)
    (@right_inv.{u u}
       (@bundle.total_space.{u u} V
          (λ (v : V),
             fintype.{u}
               (@coe_sort.{(max (u+1) 1) (max 1 (u+1))+1} (set.{u} V) (@set.has_coe_to_sort.{u} V)
                  (@simple_graph.neighbor_set.{u} V G v))))
       V
       (@bundle.proj.{u u} V
          (λ (v : V),
             fintype.{u}
               (@coe_sort.{(max (u+1) 1) (max 1 (u+1))+1} (set.{u} V) (@set.has_coe_to_sort.{u} V)
                  (@simple_graph.neighbor_set.{u} V G v)))))
    (@bundle_section_to_right_inv.{u u} V
       (λ (v : V),
          fintype.{u}
            (@coe_sort.{(max (u+1) 1) (max 1 (u+1))+1} (set.{u} V) (@set.has_coe_to_sort.{u} V)
               (@simple_graph.neighbor_set.{u} V G v)))) -/