Zulip Chat Archive

Stream: general

Topic: lintsprint 6 Oct


view this post on Zulip 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.

view this post on Zulip Johan Commelin (Oct 06 2020 at 03:19):

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

view this post on Zulip Johan Commelin (Oct 06 2020 at 03:53):

logic/unique (#4461)

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Oct 06 2020 at 04:01):

What happens if you make the example into an instance?

view this post on Zulip Johan Commelin (Oct 06 2020 at 04:01):

That should do the trick, I think

view this post on Zulip Heather Macbeth (Oct 06 2020 at 04:03):

(edited, not sure this made sense)

view this post on Zulip Heather Macbeth (Oct 06 2020 at 04:06):

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

view this post on Zulip 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]

view this post on Zulip Johan Commelin (Oct 06 2020 at 04:12):

Yes, that sounds fine

view this post on Zulip 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?)

view this post on Zulip 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?)

view this post on Zulip 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.

view this post on Zulip 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 α)

view this post on Zulip 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].

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Anatole Dedecker (Oct 06 2020 at 07:41):

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

view this post on Zulip Johan Commelin (Oct 06 2020 at 07:44):

Not yet, as far as I know

view this post on Zulip Aaron Anderson (Oct 06 2020 at 22:23):

Claiming ring_theory/* #4485

view this post on Zulip Heather Macbeth (Oct 06 2020 at 22:33):

order/bounded_lattice #4484

view this post on Zulip Aaron Anderson (Oct 06 2020 at 22:54):

order/order_iso_nat #4488

view this post on Zulip Aaron Anderson (Oct 06 2020 at 23:14):

order/lexicographic, order/pilex #4489

view this post on Zulip Yury G. Kudryashov (Oct 07 2020 at 02:37):

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

view this post on Zulip Aaron Anderson (Oct 07 2020 at 04:12):

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

view this post on Zulip 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...).

view this post on Zulip Yury G. Kudryashov (Oct 07 2020 at 17:30):

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

view this post on Zulip Yury G. Kudryashov (Oct 07 2020 at 17:31):

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

view this post on Zulip Johan Commelin (Oct 07 2020 at 17:33):

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

view this post on Zulip 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!

view this post on Zulip 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