Zulip Chat Archive

Stream: general

Topic: lintsprint 5 Oct

Johan Commelin (Oct 05 2020 at 07:13):

I am launching the mathlib lintsprint.

As you might know, there is an ongoing effort to document and clean up mathlib. We have a set of linters that run on every pull request, and check whether all definitions have docstrings, whether simp-lemmas are in the right form, whether there are unused arguments, etc....
Such a linter is introduced at a certain point in time, and from then on, all new code has to pass the linter. But we cut the old code some slack. All the old code that doesn't pass the linters, is listed in the file scripts/nolints.txt.
As of today, that file looks like this: https://github.com/leanprover-community/mathlib/blob/f2044a57a2e7347a84c53c0a076355be56e04e9a/scripts/nolints.txt

Johan Commelin (Oct 05 2020 at 07:13):

I've run grep "^-- " scripts/nolints.txt | wc -l, which reports that there are 211 files about which the linter is unhappy. In total there are ~1500 problematic declarations right now, which means about 7~8 per file on average.

Johan Commelin (Oct 05 2020 at 07:13):

I've just submitted #4411 and #4412, which take care of the first two files algebra/direct_limit and algebra/direct_sum.

Johan Commelin (Oct 05 2020 at 07:14):

How can you join?

Johan Commelin (Oct 05 2020 at 07:14):

If we have 10 people that each fix 10 linting errors, and we keep this up for 15 workdays (~3 weeks), then the nolints file will be empty!

Johan Commelin (Oct 05 2020 at 07:18):

If you join, please resist the temptation to refactor code (beyond removing unused arguments, and hence possibly changing the order of variables).
If you see code that ought to be refactored, add a comment explaining this, but don't start the refactor in a lintfix PR.

Kyle Miller (Oct 05 2020 at 07:23):

Should we remove those lines from the nolints.txt file for the PR, too?

Bryan Gin-ge Chen (Oct 05 2020 at 07:24):

No, we have a github action workflow which takes care of those once a day.

Johan Commelin (Oct 05 2020 at 07:26):

For reference: this is how the length of nolints.txt has been shrinking over time: https://leanprover-community.github.io/mathlib_stats/nolints.png

Kyle Miller (Oct 05 2020 at 07:49):

logic/relation

Scott Morrison (Oct 05 2020 at 08:20):

category_theory/adjunction/* #4415

Scott Morrison (Oct 05 2020 at 08:38):

category_theory/whiskering #4417

Kyle Miller (Oct 05 2020 at 08:40):

data/W #4418

Kyle Miller (Oct 05 2020 at 08:47):

data/array/lemmas #4419

Kyle Miller (Oct 05 2020 at 08:51):

data/buffer/basic #4420

Kyle Miller (Oct 05 2020 at 09:02):

data/dlist/{basic,instances} #4422

Anne Baanen (Oct 05 2020 at 09:06):

linear_algebra/*

Kyle Miller (Oct 05 2020 at 09:32):

data/fintype/basic #4424

Kyle Miller (Oct 05 2020 at 09:46):

data/fin2 #4426

Scott Morrison (Oct 05 2020 at 10:04):

category_theory/monad/* #4428

Markus Himmel (Oct 05 2020 at 10:08):

I'll do category_theory/limits/* if @Scott Morrison isn't already on it

Scott Morrison (Oct 05 2020 at 10:08):

Awesome, haven't touched it.

Shing Tak Lam (Oct 05 2020 at 10:15):

data/num (at some point today)

Scott Morrison (Oct 05 2020 at 10:16):

category_theory/yoneda #4429

Heather Macbeth (Oct 05 2020 at 12:05):

order/conditionally_complete_lattice #4434

Johan Commelin (Oct 05 2020 at 14:24):

Everyone who contributed to todays sprint: we just had 14 PRs merged by bors in one batch! That's a record!

Bhavik Mehta (Oct 05 2020 at 15:43):

order/rel_iso #4441

Aaron Anderson (Oct 05 2020 at 17:14):

data/pnat/basic
data/pnat/factors #4443

Aaron Anderson (Oct 05 2020 at 17:50):

algebra/ring/basic - actually @Yury G. Kudryashov took care of this

Aaron Anderson (Oct 05 2020 at 18:07):

data/int/*, data/nat/prime

Kyle Miller (Oct 05 2020 at 18:14):

control/traversable/{basic,equiv,instances,lemmas} #4444

Patrick Massot (Oct 05 2020 at 19:29):

I'll take care of files in topology/algebra

Patrick Massot (Oct 05 2020 at 19:49):

#4446

Patrick Massot (Oct 05 2020 at 19:50):

The bad side of this sprint is it encourages people to fix linting errors without creating module docstrings...

Johan Commelin (Oct 05 2020 at 20:09):

I guess we should have a module docstring linter...

Yury G. Kudryashov (Oct 05 2020 at 20:11):

https://github.com/leanprover-community/mathlib/blob/7f74e6b/src/topology/algebra/uniform_group.lean#L229

Yury G. Kudryashov (Oct 05 2020 at 20:11):

/- TODO: when modules are changed to have more explicit base ring, then change replace `is_Z_bilin`
by using `is_bilinear_map ℤ` from `tensor_product`. -/

Yury G. Kudryashov (Oct 05 2020 at 20:14):

Opened issue #4449

Patrick Massot (Oct 05 2020 at 21:30):

Fixing non-linting issue was forbidden by Johan :innocent:

Floris van Doorn (Oct 05 2020 at 22:57):

measure_theory/* is almost done, I'll finish it.

Scott Morrison (Oct 05 2020 at 22:58):

#4453 should do the rest of the category_theory linting, except for category_theory/limits/* which Markus is going to have a go at, and Kleisli. I'm inclined to generalise that to arbitary monads rather than documenting the existing definition (which is specific to monads in Type).

Scott Morrison (Oct 05 2020 at 23:18):

And getting a start on Patrick's very reasonable suggestion that we work on module-docs as well, #4454, completing the module docs for category_theory/monoidal/*.

Heather Macbeth (Oct 06 2020 at 01:06):

nolints.txt is down 193 lines today! #4456

Bhavik Mehta (Oct 06 2020 at 16:53):

Scott Morrison said:

#4453 should do the rest of the category_theory linting, except for category_theory/limits/* which Markus is going to have a go at, and Kleisli. I'm inclined to generalise that to arbitary monads rather than documenting the existing definition (which is specific to monads in Type).

For the latter, I've got an old version here: https://github.com/b-mehta/topos/blob/master/src/kleisli.lean, which I can move to mathlib pretty easily instead, if you like

Scott Morrison (Oct 06 2020 at 22:06):

yes please!

Last updated: Dec 20 2023 at 11:08 UTC