Zulip Chat Archive

Stream: general

Topic: tiny challenge

Johan Commelin (Oct 30 2020 at 11:12):

According to image.png
we are rapidly approaching 450 commits to master in this month.
~~There are 7 PRs running in a bors queue, and 2 more waiting to run in another queue.~~
There are 2 PRs running in a bors queue.
If we merge another 14 high-quality juicy PRs, then we'll have an average of 15 merged PRs per day for this entire month. I think we don't even have to push hard to unlock this one.

Kevin Buzzard (Oct 30 2020 at 12:41):

Currently when I have some review time I go to #queue and choose the first PR which seems to be in an area that I might know something about. Is this the optimal strategy right now?

Bryan Gin-ge Chen (Oct 30 2020 at 15:22):

Yes, I think so. Thanks for helping with the reviews!

Rob Lewis (Oct 31 2020 at 16:35):

Incidentally, we also recently hit 60k declarations (according to however the stats page counts)

Rob Lewis (Oct 31 2020 at 17:14):

If you want a real stretch goal: the mathlib repo has around 421k loc right now. Can we hit 500k by the end of 2020?

Kevin Buzzard (Oct 31 2020 at 17:14):

time for a docstring push

Rob Lewis (Oct 31 2020 at 17:15):

We've been averaging 1k/day for a while. It would be tough, but not out of the realm of possibility.

Last updated: Dec 20 2023 at 11:08 UTC