Zulip Chat Archive

Stream: general

Topic: lintsprint 7 Oct

Johan Commelin (Oct 07 2020 at 04:47):

Thanks again to everyone who has contributed to the lintsprint in the past two days!
You can clearly see the result of our efforts in https://leanprover-community.github.io/mathlib_stats/nolints.png

Johan Commelin (Oct 07 2020 at 04:49):

grep "^[^-]" scripts/nolints.txt | wc -l
1175

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

How does one add a docstring to an automatically-generated definition like con.to_setoid on group_theory/congruence?

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

You can use add_decl_doc.

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

Ok then, #4493 on group_theory/abelianization, presented_group, congruence.

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

~~group_theory/perm/*~~

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

Johan Commelin said:

group_theory/perm/*

I already submitted one for that, at the end of the 6 Oct thread, #4492

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

Ooh, good point, thanks

Markus Himmel (Oct 07 2020 at 05:54):

category_theory/equivalence #4495

Kyle Miller (Oct 07 2020 at 06:27):

control/functor #4496

Kyle Miller (Oct 07 2020 at 06:46):

data/hash_map #4498

Kyle Miller (Oct 07 2020 at 06:59):

data/tree #4499

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

data/quot #4500

Kevin Buzzard (Oct 07 2020 at 14:01):

Is there a graph of commits by time? It would be interesting to see what the sprint has done. I'm sorry I'm not helping, I'm recording lean videos for undergraduates!

Markus Himmel (Oct 07 2020 at 14:02):

Do you mean something like https://github.com/leanprover-community/mathlib/graphs/commit-activity?

Kevin Buzzard (Oct 07 2020 at 15:09):

oh yeah! Looks like it was 3rd and 4th highest day for commits the last two days

Mario Carneiro (Oct 07 2020 at 19:43):

I'm also sorry for not contributing. The worst part is that I had actually prepared a big docs commit cleaning up all my old files like data.hash_map, but it got bogged down and I left it on my work machine, and when the internship ended I forgot to save it :sad:

Johan Commelin (Oct 07 2020 at 19:45):

Well... we aren't done yet...

Johan Commelin (Oct 07 2020 at 19:45):

There's probably still > 800 declarations out there waiting for docstrings

Johan Commelin (Oct 07 2020 at 19:46):

And tactic/ is particularly bad

Kyle Miller (Oct 07 2020 at 19:46):

@Mario Carneiro would you take a look at #4498? The documentation I added is mostly an educated guess...

Kyle Miller (Oct 07 2020 at 19:48):

I also wouldn't mind if you took that one over :smile:

Johan Commelin (Oct 08 2020 at 04:19):

#4521 :tada: we've made nolints.txt 164 lines shorter :surprise: :octopus:

Last updated: Dec 20 2023 at 11:08 UTC