Zulip Chat Archive

Stream: PR reviews

Topic: 88 bottles of maths on the wall

Scott Morrison (Aug 15 2020 at 05:17):

Is 88 a new record for open PRs? Everyone is welcome to help review, whether or not you're a maintainer!

Whether it's comments on documentation or style, or suggestions for major revisions, or even just a LGTM, everything is helpful!

Anatole Dedecker (Aug 15 2020 at 19:17):

And... this is no longer the record :laughter_tears:

Johan Commelin (Aug 15 2020 at 19:18):

It hit 92 a couple of moments ago, but it's down to 90 again.

Anatole Dedecker (Aug 15 2020 at 19:25):

I saw it at 93

Johan Commelin (Aug 15 2020 at 19:57):

image.png

Johan Commelin (Aug 15 2020 at 19:58):

We are 4 PRs away from a 1PR/hr average :oops:

Johan Commelin (Aug 15 2020 at 20:06):

And... only 3 to go

Johan Commelin (Aug 15 2020 at 20:28):

#3806, hence only 2 PRs left...

Anatole Dedecker (Aug 15 2020 at 20:35):

Just to boost stats (while doing something useful), here's #3807

Rob Lewis (Aug 15 2020 at 20:37):

"boost stats" / stress out the maintainers :p

Johan Commelin (Aug 15 2020 at 20:38):

We made it! :grinning_face_with_smiling_eyes:
image.png

Rob Lewis (Aug 15 2020 at 20:38):

I remember the days when a queue of 30 felt like a lot! Those days weren't very long ago.

Bhavik Mehta (Aug 15 2020 at 20:53):

It's at 95 now!

Johan Commelin (Aug 15 2020 at 20:59):

Sorry, I think you meant 96...

Floris van Doorn (Aug 15 2020 at 21:50):

There are also 10 PRs in the current batch :) https://github.com/leanprover-community/mathlib/compare/staging

Scott Morrison (Aug 16 2020 at 06:08):

We still have 84 open PRs, but only 8 are currently in request-review.

Rob Lewis (Aug 16 2020 at 10:24):

Another milestone we hit during yesterday's craziness: GitHub says mathlib now has 100 contributors. In December when we wrote the mathlib paper, we said we had 73, and this included a bunch of names that had author attribution in file headers but no git credit.

Bhavik Mehta (Oct 04 2020 at 19:31):

Are we at a new record? 97 right now

Heather Macbeth (Oct 05 2020 at 00:38):

98! @Yury G. Kudryashov will you do enough to get us to 3 digits?

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

Done (by @Joseph Myers and me)

Heather Macbeth (Oct 05 2020 at 01:24):

Screen-Shot-2020-10-04-at-9.23.33-PM.png

Yury G. Kudryashov (Oct 05 2020 at 01:25):

Feel free to review some of them.

Yury G. Kudryashov (Oct 05 2020 at 01:26):

I'll review #4399 now

Bryan Gin-ge Chen (Oct 05 2020 at 01:32):

There are "only" 31 awaiting-review, so not too much more than usual.

Johan Commelin (Oct 05 2020 at 10:54):

112!

Anne Baanen (Oct 05 2020 at 10:56):

Obligatory "haha factorial, wow 197450685722107402353682037275992488341277868034975337796656295094902858969771811440894224355027779366597957338237853638272334919686385621811850780464277094400000000000000000000000000 prs" comment.

Last updated: Dec 20 2023 at 11:08 UTC