## Stream: general

### Topic: lintsprint 6 Oct

#### Johan Commelin (Oct 06 2020 at 03:12):

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 (Oct 06 2020 at 03:19):

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

#### Johan Commelin (Oct 06 2020 at 03:53):

logic/unique (#4461)

#### Heather Macbeth (Oct 06 2020 at 03:55):

@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 (Oct 06 2020 at 04:01):

What happens if you make the example into an instance?

#### Johan Commelin (Oct 06 2020 at 04:01):

That should do the trick, I think

#### Heather Macbeth (Oct 06 2020 at 04:03):

(edited, not sure this made sense)

#### Heather Macbeth (Oct 06 2020 at 04:06):

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

#### Heather Macbeth (Oct 06 2020 at 04:07):

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 (Oct 06 2020 at 04:12):

Yes, that sounds fine

#### Johan Commelin (Oct 06 2020 at 04:12):

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

#### Kyle Miller (Oct 06 2020 at 04:13):

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 (Oct 06 2020 at 04:15):

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 (Oct 06 2020 at 04:23):

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 (Oct 06 2020 at 04:50):

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 (Oct 06 2020 at 07:04):

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 (Oct 06 2020 at 07:06):

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

#### Anatole Dedecker (Oct 06 2020 at 07:41):

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

#### Johan Commelin (Oct 06 2020 at 07:44):

Not yet, as far as I know

#### Aaron Anderson (Oct 06 2020 at 22:23):

Claiming ring_theory/* #4485

#### Heather Macbeth (Oct 06 2020 at 22:33):

order/bounded_lattice #4484

#### Aaron Anderson (Oct 06 2020 at 22:54):

order/order_iso_nat #4488

#### Aaron Anderson (Oct 06 2020 at 23:14):

order/lexicographic, order/pilex #4489

#### Yury G. Kudryashov (Oct 07 2020 at 02:37):

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

#### Aaron Anderson (Oct 07 2020 at 04:12):

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

#### Patrick Massot (Oct 07 2020 at 07:05):

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 (Oct 07 2020 at 17:30):

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

#### Yury G. Kudryashov (Oct 07 2020 at 17:31):

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

#### Johan Commelin (Oct 07 2020 at 17:33):

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

#### Yury G. Kudryashov (Oct 07 2020 at 17:34):

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

#### Yury G. Kudryashov (Oct 07 2020 at 17:36):

I want linear_map.unique_of_left/right for #4407

Last updated: May 13 2021 at 18:26 UTC