Zulip Chat Archive
Stream: general
Topic: record
Johan Commelin (Jul 20 2020 at 04:38):
Shing Tak Lam (Jul 20 2020 at 04:53):
There was 77 PRs open 26 hours ago :)
Scott Morrison (Jul 20 2020 at 05:29):
I briefly saw it at 78.
Johan Commelin (Jul 20 2020 at 05:54):
Screenshot or it didn't happen :rofl:
Chris Hughes (Aug 15 2020 at 20:36):
94
Screenshot-2020-08-15-at-21.35.46.png
Chris Hughes (Aug 15 2020 at 20:39):
95 Screenshot-2020-08-15-at-21.39.29.png
Anatole Dedecker (Aug 15 2020 at 20:41):
And 24 today, one per hour !
Bryan Gin-ge Chen (Aug 15 2020 at 20:44):
Is 10 the record size of a bors batch? Screen-Shot-2020-08-15-at-4.43.19-PM.png
Johan Commelin (Aug 15 2020 at 20:48):
95
image.png
will we make it to :100: ?
Johan Commelin (Aug 15 2020 at 20:48):
Ooh, Chris already had the 95 record...
Rob Lewis (Aug 15 2020 at 20:49):
I was hoping the giant bors batch would land before midnight so we'd get a daily commit record
Rob Lewis (Aug 15 2020 at 20:49):
I don't know what the current record is, but pretty sure 10 more would put us over
Rob Lewis (Aug 15 2020 at 20:50):
But I think it's gonna just miss.
Chris Hughes (Aug 15 2020 at 20:55):
Three hours until UTC midnight.
Anatole Dedecker (Aug 15 2020 at 20:59):
Capture-du-2020-08-15-22-59-23.png 96 !
Anatole Dedecker (Aug 15 2020 at 22:05):
Capture-du-2020-08-16-00-04-04.png I was able to capture it at the last moment
Rob Lewis (Aug 15 2020 at 22:08):
Ooh, they counted for today because GitHub tracks the commit time, not when it was pushed to master!
Rob Lewis (Aug 15 2020 at 22:09):
Or maybe it's a time zone thing, I dunno. Either way, 31 commits today from my perspective.
Rob Lewis (Aug 15 2020 at 22:10):
And we still have 87 open :fear:
Johan Commelin (Aug 20 2020 at 20:53):
Number of PRs is rising rapidly again... can we break the old record of last saturday?
Scott Morrison (Aug 20 2020 at 23:36):
I do wonder if we should start "cleaning out" the abandoned backlog more. I'm not really sure it's necessary, but I have noticed that recently I only look at the request-review list, so if authors forget to switch labels back after they make changes, I may not notice the PR again...
Johan Commelin (Sep 10 2020 at 08:57):
I just kicked PR #4000 onto the merge queue (-;
(Doesn't mean that we have merged 4000 PRs, I know... but still, it's a nice record :smiley:)
Johan Commelin (Sep 11 2020 at 13:36):
This is going to be a pretty crazy day: https://github.com/leanprover-community/mathlib/pulse/daily
image.png
Kenny Lau (Sep 11 2020 at 13:40):
does it say that @Scott Morrison made 20 PR's today?
Kenny Lau (Sep 11 2020 at 13:40):
or am I reading it wrong
Johan Commelin (Sep 11 2020 at 13:41):
commits
Johan Commelin (Sep 11 2020 at 13:42):
but ~2000 lines added... and a lot more to come (-;
Eric Wieser (Nov 11 2020 at 10:22):
Now up to 113...
Johan Commelin (Nov 11 2020 at 10:24):
I blame the triage bot
Kevin Buzzard (Nov 11 2020 at 10:25):
I thought that was supposed to be _decreasing_ the number of issues/open PR's!
Eric Wieser (Nov 11 2020 at 10:27):
I suppose it sometimes results in issues spawning PRs?
Eric Wieser (Nov 11 2020 at 10:27):
It would be cool if we had a graph of the length of #queue over time
Johan Commelin (Nov 11 2020 at 10:31):
/me was tongue in cheek
Aaron Anderson (Dec 02 2020 at 20:38):
123, but several are ready-to-merge
Eric Wieser (Dec 14 2020 at 12:03):
125...
Anne Baanen (Dec 14 2020 at 12:06):
Working on it directly and lively :)
Anne Baanen (Mar 26 2021 at 11:28):
177 open PRs and 42 on the #queue...
Scott Morrison (Mar 26 2021 at 11:36):
I saw 48 on the queue earlier today. :-) I don't think any are actually egregiously old (in the sense of not-touched-recently).
Thomas Browning (Apr 05 2021 at 17:18):
185 open, and 60 on #queue
Johan Commelin (Apr 05 2021 at 18:27):
The queue is down to 44 now
Kevin Buzzard (Apr 05 2021 at 19:29):
Thank you to all the new maintainers -- and to the old ones too of course -- who spend a lot of their time making sure that our mathematics library is of a really high quality. Having watched from the sidelines for several years i can really see what a tricky job this is. In particular the way that people decide that we could do something better and then they embark on a big refactor which then needs to be quickly reviewed -- this is hard work and often very delicate but it's also extremely important to make the library the best it can be. Thanks to all the maintainers.
Johan Commelin (Apr 06 2021 at 11:22):
Queue is now down to 24 :octopus:
Last updated: Dec 20 2023 at 11:08 UTC