Zulip Chat Archive
Stream: general
Topic: New record
Patrick Massot (Jan 05 2019 at 13:17):
I think we have a new record:
50_PR.png
It's a bit unfair to take advantage of Mario traveling to add five more PR...
Patrick Massot (Jan 05 2019 at 13:26):
@Johannes Hölzl an easy way to make sure Mario won't be depressed by this when landing would be to incorporate #573 into #568, merge the later and close the former
Chris Hughes (Jan 05 2019 at 14:50):
I've been making gazillions of hopefully quite easy ones, so it's not that bad.
Johannes Hölzl (Jan 05 2019 at 15:16):
I'm not sure about the namespace metric, newly introduced namespaces are usually type oriented
Mario Carneiro (Jan 05 2019 at 15:42):
I agree. Although some of the theorems could benefit from a namespace, most are already disambiguated in the name by referring to dist or metric
Mario Carneiro (Jan 05 2019 at 15:43):
and the basic algebraic theorems in groups and rings are all in the root namespace
Mario Carneiro (Jan 05 2019 at 15:43):
In particular, metric_space should not be in a namespace
Mario Carneiro (Jan 05 2019 at 17:13):
I put a counter proposal at https://github.com/leanprover/mathlib/compare/master...leanprover-community:metric_namespace . @Johannes Hölzl @Sebastien Gouezel @Patrick Massot Let me know what you think - I'm not planning on forcing this if people don't like it. The gist of it is: stuff about dist and edist are in the root namespace, stuff about topological characterizations in a metric space are in metric namespace, ball, closed_ball, bounded are all in the metric namespace. Similar for the emetric namespace.
Mario Carneiro (Jan 05 2019 at 17:14):
I tried putting stuff in the metric_space namespace instead, but then there are collisions with metric space axioms
Mario Carneiro (Jan 05 2019 at 17:15):
things like cauchy_of_metric are renamed to metric.cauchy_iff
Sebastien Gouezel (Jan 05 2019 at 17:26):
Looks very good to me. I felt the need for a metric namespace when I started introducing more concepts, like isometries: it felt wrong to put them in the root namespace. Things that could have a different meaning in a different context, like bounded or balls, should also definitely go in the namespace, just like you do in your proposal. I also tried first with a metric_space namespace, but it created collisions as you just mentioned.
Patrick Massot (Jan 05 2019 at 17:51):
I think the root namespace should be really clean. But of course it's much less important in mathlib than in core's init since you can always choose what to import (especially after we'll split those huge files). And metric_space sounds uncontroversial, so Mario's version looks good to me.
Patrick Massot (Jan 05 2019 at 19:31):
Hoho, a big merging wave is in progress!
Johan Commelin (Jan 05 2019 at 21:06):
Oops, we're down to 38...
Patrick Massot (Jan 05 2019 at 21:07):
But I still can't shuffle files because the metric namespace PR is not merged. @Johannes Hölzl ?
Kenny Lau (Feb 27 2019 at 00:07):
We now have 43... on our way to achieve a newer record!
Johan Commelin (May 03 2019 at 18:25):
If we get one more PR merged all the PRs fit on one page again on Github...
Scott Morrison (May 03 2019 at 20:19):
Should I put up some more? :-)
Scott Morrison (May 03 2019 at 20:20):
As soon as #886 is merged I have some follow-ups ready to go.
Scott Morrison (May 03 2019 at 20:20):
I think #967 is about to be merged, once travis catches up.
Johan Commelin (Jun 03 2020 at 09:52):
We have 66 open PRs!
Chris Hughes (Jun 03 2020 at 10:37):
67
Kevin Buzzard (Jun 03 2020 at 11:52):
After my grant proposal deadlines I really hope to get back into this
Kevin Buzzard (Jun 03 2020 at 11:55):
anything which is related to any undergraduate level maths I could try pushing on the discord. The summer project doesn't start for almost a month, but I am slowly getting on top of my administrative duties for the year.
Johan Commelin (Oct 01 2021 at 20:16):
September set another record: https://leanprover-community.github.io/mathlib_stats.html
510 commits!
Yaël Dillies (Oct 01 2021 at 20:18):
I had the feeling everything got faster!
Kevin Buzzard (Oct 01 2021 at 20:54):
What does that mean? Mathlib PRs are squash-merged, right? So is that 510 PRs (as opposed to 50 PRs each with 10 commits)?
Yaël Dillies (Oct 01 2021 at 20:57):
Yes, that's right! Else, we would be at much much more. I myself must have generated around 200 such unsquashed commits this month.
Scott Morrison (Oct 01 2021 at 23:04):
Pretty impressive. We had a good balance of new material and some important refactors. As we go into the mathlib4 port, I think it's great if we can do as much refactoring / cleaning up / paying down technical debt as possible!
Rob Lewis (Oct 29 2021 at 13:52):
We've already broken September's record with three days to go this month!
Yaël Dillies (Oct 29 2021 at 13:52):
Time to file some more PR to secure it!
Johan Commelin (Jan 01 2022 at 12:44):
Happy new year everyone! We broke two records last night:
• In Dec 2021 we had 565 commits to mathlib. That beats the 558 from Oct 2021.
• In all of 2021 we had 5209 commits to mathlib. That's ~ 100 per week!
Last updated: Dec 20 2023 at 11:08 UTC