lintsprint 6 Oct

Stream: general

[Johan Commelin]

Thank you so much! With concerted efforts, we removed more than 10% of the nolints.txt file, yesterday.
Here is what the file looks like now: https://github.com/leanprover-community/mathlib/blob/bc06cef96855ccf689d4ae26d2eb5cd131965b7a/scripts/nolints.txt

Note that there are still 7 lintfix PRs that are open: https://github.com/leanprover-community/mathlib/labels/lintfix
So if you want to contribute, please take a look to see that you aren't duplicating efforts.

[Johan Commelin]

I'll start on data/equiv/ring (#4460) and eckmann_hilton (#4459)

[Johan Commelin]

logic/unique (#4461)

[Heather Macbeth]

@Johan Commelin How do you get rid of an inhabited instance lint error? Eg, in docs#topological_space.closeds, I have tried variants on

/-- The type of closed subsets is inhabited, with default element the empty set. -/
example : inhabited (closeds α) := ⟨⟨∅, is_closed_empty ⟩⟩

but can't figure out the exact format to satisfy the linter.

[Johan Commelin]

What happens if you make the example into an instance?

[Johan Commelin]

That should do the trick, I think

[Heather Macbeth]

(edited, not sure this made sense)

[Heather Macbeth]

I think I'm mixing up a few unrelated pieces of good advice ...

[Heather Macbeth]

And second question: it's ok to fix an inhabited instance lint error with nolint plus a docstring, right?

/-- .... The type is not necessarily inhabited, for example (1) if `α` is empty,
(2) if `α` is infinite and has the trivial topology. -/
@[nolint has_inhabited_instance]

[Johan Commelin]

Yes, that sounds fine

[Johan Commelin]

(Although I'm for the moment maths-confused about (2). Why doesn't the empty set work in that case?)

[Kyle Miller]

It seems the linter is happy with any instance, even if it only exists conditionally. (I don't fully understand the motivation to lint for inhabited instances. Maybe you're supposed to think about having some amount of useful coverage?)

[Heather Macbeth]

Johan Commelin said:

(Although I'm for the moment maths-confused about (2). Why doesn't the empty set work in that case?)

This is to fix the other inhabited instance error, on "nonempty compacts". But I think (2) is wrong for other reasons.

[Heather Macbeth]

topology/closeds #4462

thanks to @Kyle Miller 's trick, no need for the nolint:

instance nonempty_compacts_inhabited [inhabited α] : inhabited (nonempty_compacts α)

[Floris van Doorn]

I also don't really see the point of the inhabited instances linter. It's good to have inhabited instances for things where it is easy to determine whether they are inhabited (like ℕ or α × β) but not really useful when it's not so easy to determine (like α ≃ β).
I think we should be very liberal with adding @[nolint has_inhabited_instance].

[Gabriel Ebner]

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.

[Gabriel Ebner]

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

[Anatole Dedecker]

Is anyone taking care of data/matrix/basic ? Otherwise I'll do it

[Johan Commelin]

Not yet, as far as I know

[Aaron Anderson]

Claiming ring_theory/* #4485

[Heather Macbeth]

order/bounded_lattice #4484

[Aaron Anderson]

order/order_iso_nat #4488

[Aaron Anderson]

order/lexicographic, order/pilex #4489

[Yury G. Kudryashov]

I'm going over topological monoids and group with API&doc review.

[Aaron Anderson]

group_theory/perm/*. I hope I accurately described all the sign_aux functions, @Chris Hughes

[Patrick Massot]

Yury G. Kudryashov said:

I'm going over topological monoids and group with API&doc review.

Note that the situation with uniform structure of topological groups is still something of a mess. It has been on my TODO list since the end of the perfectoid project to refactor this. If you are interested I can tell you the plan (but I get to choose I would much prefer you work on convexity...).

[Yury G. Kudryashov]

I don't want to do a big refactor there.

[Yury G. Kudryashov]

Just move some lemmas go topology/algebra/monoid, rename vars.

[Johan Commelin]

That's ok, but just don't label it lintfix.

[Yury G. Kudryashov]

I won't. BTW, I'm fixing logic/unique, including lintfix. E.g., we didn't have pi.unique instance!

[Yury G. Kudryashov]

I want linear_map.unique_of_left/right for #4407