Mathlib bumps

Stream: sphere eversion

[Michael Rothgang]

I just reviewed https://github.com/leanprover-community/sphere-eversion/pull/94: except for one comment (which could be a follow-up if needed), this looks good to me. Thanks for writing it, @Ruben Van de Velde!

[Ruben Van de Velde]

Thanks for the suggestion, pushed it now

[Michael Rothgang]

Thanks! I just merged the PR: now, the documentation build fails. I think I know why and pushed a fix (you also need to bump docbuild to the right version).

[Ruben Van de Velde]

Thanks, I don't understand how to deal with docgen

[Michael Rothgang]

To avoid duplicate work: I'm working on bumping to current mathlib (edit: now merged)

[Notification Bot]

A message was moved here from #sphere eversion > What is ready for upstreaming? by Michael Rothgang.

[Notification Bot]

A message was moved here from #sphere eversion > What is ready for upstreaming? by Michael Rothgang.

[Notification Bot]

A message was moved here from #sphere eversion > What is ready for upstreaming? by Michael Rothgang.

[Notification Bot]

A message was moved here from #sphere eversion > What is ready for upstreaming? by Michael Rothgang.

[Notification Bot]

A message was moved here from #sphere eversion > What is ready for upstreaming? by Michael Rothgang.

[Notification Bot]

2 messages were moved here from #sphere eversion > Math by Michael Rothgang.

[Michael Rothgang]

https://github.com/leanprover-community/sphere-eversion/pull/102 bumps mathlib to 4.17.0, which is great. This made a naming question arise: should ContMDiff.inr really be called like this, or rather ContMDiff.prod_left?

There is a naming collision now (because in the mean-time, mathlib gained ContMDiff.inr, which is actually about Sum.inr). I'd tend towards prod_left, as Sum.inr is not mentioned in the statement at all. What do e.g. @Floris van Doorn and @Patrick Massot think?

[Patrick Massot]

I don’t think anything about this. Every name is ok for me.

[Ruben Van de Velde]

Same

[Floris van Doorn]

I also don't have a strong opinion, inr is probably not the right name. I'm not even sure if that should become a Mathlib lemma itself, or that the Mathlib spelling should be contDiff_const.prod contDiff_id

[Michael Rothgang]

Alright, thanks for the input! Accordingly, I propose at least switching to prod_left.

[Ruben Van de Velde]

I pushed the change. I don't know what's wrong with the doc build, and not excited to try and figure it out

[Pietro Monticone]

It’s just a matter of pinning the stable version of doc-gen in the docbuild toml.

[Pietro Monticone]

I’ll open a PR both on SphereEversion and Carleson to incorporate the new workflow we use in FLT that completely solves this type of issue. I’ll do it later today or tomorrow.

[Ruben Van de Velde]

CI passes for the bump

[Pietro Monticone]

Done :check: https://github.com/leanprover-community/sphere-eversion/pull/103

[Ruben Van de Velde]

Do you want to remove the existing file?

[Pietro Monticone]

Ops, sorry. Yes, I'm going to do it right now.

[Ruben Van de Velde]

4.18: https://github.com/leanprover-community/sphere-eversion/pull/104

[Michael Rothgang]

Thanks, LGTM!

[Patrick Massot]

Thanks a lot Ruben! I asked two questions on GitHub.

[Ruben Van de Velde]

Replied there

[Ruben Van de Velde]

4.19: https://github.com/leanprover-community/sphere-eversion/pull/105

[Patrick Massot]

Thanks a lot!

[Patrick Massot]

Did you check it builds locally?

[Michael Rothgang]

I left two small comments: with these addressed, LGTM (assuming CI builds).

[Michael Rothgang]

Update: PR CI built the project successfully (and is now generating documentation, etc.)

[Patrick Massot]

Yes, it looks good. The only question I had was about the things that moved to the Submodule namespace. Did you consider opening that namespace? Does it create name clashes?

[Ruben Van de Velde]

Done - it's just orthogonalProjection that moved

[Patrick Massot]

Why not opening it before line 232?

[Ruben Van de Velde]

Sure, that works too, or I could open it at the top of the file