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: May 11 2021 at 00:31 UTC