Zulip Chat Archive

Stream: general

Topic: New record


view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Chris Hughes (Jan 05 2019 at 14:50):

I've been making gazillions of hopefully quite easy ones, so it's not that bad.

view this post on Zulip Johannes Hölzl (Jan 05 2019 at 15:16):

I'm not sure about the namespace metric, newly introduced namespaces are usually type oriented

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 05 2019 at 15:43):

and the basic algebraic theorems in groups and rings are all in the root namespace

view this post on Zulip Mario Carneiro (Jan 05 2019 at 15:43):

In particular, metric_space should not be in a namespace

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 05 2019 at 17:15):

things like cauchy_of_metric are renamed to metric.cauchy_iff

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jan 05 2019 at 19:31):

Hoho, a big merging wave is in progress!

view this post on Zulip Johan Commelin (Jan 05 2019 at 21:06):

Oops, we're down to 38...

view this post on Zulip 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 ?

view this post on Zulip Kenny Lau (Feb 27 2019 at 00:07):

We now have 43... on our way to achieve a newer record!

view this post on Zulip 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...

view this post on Zulip Scott Morrison (May 03 2019 at 20:19):

Should I put up some more? :-)

view this post on Zulip Scott Morrison (May 03 2019 at 20:20):

As soon as #886 is merged I have some follow-ups ready to go.

view this post on Zulip Scott Morrison (May 03 2019 at 20:20):

I think #967 is about to be merged, once travis catches up.

view this post on Zulip Johan Commelin (Jun 03 2020 at 09:52):

We have 66 open PRs!

view this post on Zulip Chris Hughes (Jun 03 2020 at 10:37):

67

view this post on Zulip Kevin Buzzard (Jun 03 2020 at 11:52):

After my grant proposal deadlines I really hope to get back into this

view this post on Zulip 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.


Last updated: May 08 2021 at 04:14 UTC