## 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!

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.

Last updated: May 08 2021 at 04:14 UTC