Zulip Chat Archive

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 (Feb 13 2025 at 16:48):

Thanks for the suggestion, pushed it now

Michael Rothgang (Feb 13 2025 at 17:40):

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 (Feb 13 2025 at 18:29):

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

Michael Rothgang (Feb 15 2025 at 18:58):

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

Notification Bot (Feb 18 2025 at 17:15):

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

Michael Rothgang (Mar 03 2025 at 17:19):

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 (Mar 03 2025 at 18:03):

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

Ruben Van de Velde (Mar 03 2025 at 18:17):

Same

Floris van Doorn (Mar 04 2025 at 11:26):

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 (Mar 04 2025 at 11:39):

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

Ruben Van de Velde (Mar 04 2025 at 11:57):

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 (Mar 04 2025 at 12:39):

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

Pietro Monticone (Mar 04 2025 at 12:42):

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 (Mar 04 2025 at 14:25):

CI passes for the bump

Pietro Monticone (Mar 04 2025 at 22:44):

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

Ruben Van de Velde (Mar 04 2025 at 22:46):

Do you want to remove the existing file?

Pietro Monticone (Mar 04 2025 at 22:59):

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

Ruben Van de Velde (Apr 01 2025 at 08:38):

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

Michael Rothgang (Apr 01 2025 at 10:23):

Thanks, LGTM!

Patrick Massot (Apr 02 2025 at 07:11):

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

Ruben Van de Velde (Apr 02 2025 at 07:39):

Replied there

Ruben Van de Velde (May 01 2025 at 19:58):

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

Patrick Massot (May 01 2025 at 20:05):

Thanks a lot!

Patrick Massot (May 01 2025 at 20:06):

Did you check it builds locally?

Michael Rothgang (May 01 2025 at 20:08):

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

Michael Rothgang (May 01 2025 at 20:09):

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

Patrick Massot (May 01 2025 at 20:12):

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 (May 01 2025 at 20:25):

Done - it's just orthogonalProjection that moved

Patrick Massot (May 01 2025 at 20:29):

Why not opening it before line 232?

Ruben Van de Velde (May 01 2025 at 21:02):

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

Michael Rothgang (Jun 04 2025 at 07:22):

PSA: I just merged a few PRs fixing (almost) all mathlib linter warnings in the project. For instance, it turns out the two remaining maxHeartbeat bumps can just be removed. If you disagree with some linter fixes, please speak up --- I'm happy to revert any controversial parts.

Michael Rothgang (Jun 04 2025 at 07:23):

sphere-eversion#112 bumps mathlib a bit and enables all mathlib linters on the project (which is really easy to do now). I'm also happy with not merging the second part.

Michael Rothgang (Jun 10 2025 at 17:51):

I just bumped the PR a bit more: if I don't hear objects, I'll merge this soon.

Pietro Monticone (Jul 01 2025 at 08:54):

sphere-eversion#115

Pietro Monticone (Jul 16 2025 at 08:45):

sphere-eversion#116

Ruben Van de Velde (Aug 14 2025 at 09:42):

I'm working on a bump

Ruben Van de Velde (Aug 14 2025 at 09:59):

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

Michael Rothgang (Aug 14 2025 at 11:01):

Thanks, LGTM!

Ruben Van de Velde (Nov 14 2025 at 22:50):

https://github.com/leanprover-community/sphere-eversion/pull/127 to 4.25

Michael Rothgang (Nov 17 2025 at 21:41):

The PR itself looks good for me, but fails the "compile blueprint" step (for reasons that seem related to pip/Python changes). Anybody recognise this error? @Pietro Monticone maybe?

Bhavik Mehta (Nov 17 2025 at 22:28):

This blueprint error is familiar, let me remind myself how to fix it

Ruben Van de Velde (Nov 17 2025 at 22:30):

I think it can be solved by copying the github action from (say) FLT

Bhavik Mehta (Nov 17 2025 at 22:30):

Ah, this should get fixed by bumping the docgen-action version, to anything at least as new as the second most recent commit, which fixed this: deed0cdc44dd8e5de07a300773eb751d33e32fc8