What is ready for upstreaming?

Stream: sphere eversion

[Michael Rothgang]

In some free time, I'd like to help by upstreaming some parts which are already in good shape.
Is it safe to assume that most of the "ToMathlib" directory is safe to PR? (If not, do you know particular parts which I should avoid?) What about OpenEmbedding.{homeomorph,isCompact_preimage} in Global/Gromov.lean? (Mathlib gained IsEmpty.homeomorph recently.)

To start this, I've mostly bumped mathlib locally. (There are ~ten errors left on which I'd appreciate help, due to simp changes or so.) Can I get push access or should I open a PR from a fork?

[Kevin Buzzard]

One of the common mistakes which are made in projects such as this is that there's the push to get the project over the line, and then a bunch of people lose interest and/or move onto other things, and the ToMathlib directory just sits there rotting. However, with some projects like LTE, the ToMathlib directory consisted of many experiments containing material which we all knew was a good fit for mathlib but which sometimes we weren't happy with. A great example is homological algebra, where there are several subtleties getting the ideas into dependent type theory (a cohomology group is both a limit and a colimit, and our initial formalisation did not reflect this well enough); it took over a year, a major refactor, and the heroic efforts of Joël Riou to get this stuff into mathlib [ad: he's talking about his work in about 80 minutes at Lean Together!]

However if there are parts of the formalisation in ToMathlib which you are pretty convinced are in final form, then I would strongly encourage people to PR them to mathlib sooner rather than later, because as we all know mathlib is extremely active, and the longer things are left the harder the job becomes. For example simp changed recently and a bunch of stuff broke; other major changes will I'm sure be coming in the future. Code breaking in your project means that you have to fix it; code which has made it into mathlib is the problem of the people making the changes to mathlib (and they are often in a very good position to fix the problems which show up because they understand the changes).

[Patrick Massot]

Thanks Michael, help is very much appreciated. All the project could go to Mathlib, but some things in the global folder really need to be generalized a lot. The theory of smooth fiber bundles is simply not good enough yet.

[Patrick Massot]

The ForMathlib folder is indeed the easiest target. In particular there is still work about parametric integrals that should really go before someone redo it in Mathlib.

[Patrick Massot]

You should have gotten a GitHub invite. Then you can push your branch and we will work on fixing it.

[Yaël Dillies]

I have a lot of experience upstreaming my projects to mathlib and I have advice to give:

• I have two folders inside my project (see eg github.com/YaelDillies/LeanAPAP):
  • MyProject/Mathlib containing lemmas that belong to existing mathlib files
  • MyProject/Prereqs (or ForMathlib) containing new files that are ready to go to mathlib
• MyProject/Mathlib/X.lean only contains lemmas/definitions that should go in Mathlib/X.lean and only imports Mathlib/X.lean and MyProject/Mathlin/Y.lean where Mathlib/X.lean imports (potentially indirectly) Mathlib/Y.lean.
• On the project website (eg yaeldillies.github.io/LeanAPAP), there is a list of files not importing any other file from MyProject. Those are the files one can upstream.
• Any modification to Mathlib/X.lean which is not a lemma/def addition is recorded as a todo in MyProject/Mathlib/X.lean.

[Yaël Dillies]

This works great because anyone can then upstream anything under MyProject/Mathlib and MyProject/Prereqs without thinking about it much.

[Michael Rothgang]

I just pushed my changes to the MR-bump-mathlib branch.

[Michael Rothgang]

The sorried proofs are marked with "TODO-BUMP"; the other build errors are in ToMathlib/Topology/LocallyFinite.lean and ToMathlib/Analysis/InnerProductSpace/Projection.lean.

[Michael Rothgang]

Last but not least: thanks for the quick response and the invite, by the way!

[Michael Rothgang]

And (no rush!): my first three PRs upstreaming some results are awaiting review.

[Yury G. Kudryashov]

You'll get reviews faster if you write their numbers here.

[Ruben Van de Velde]

#9623 #9624 #9635

[Michael Rothgang]

The first two PRs are merged now; thanks for the fast reviews.

[Michael Rothgang]

I just submitted two more PRs, each treating a single file in ToMathlib:
#9669 a function is ContMDiffAt outside of its tsupport
#9672 a subset of a charted space is open iff its image in each chart is

[Yury G. Kudryashov]

BTW, please don't backport equivariant maps yet. I have a better version in a branch.

[Michael Rothgang]

Sure, noted. I'm awaiting your branch then, whenever you find the time.(By the way, this is extremely helpful advice, thanks a lot.)

[Michael Rothgang]

I think the next files on my list are Geometry/ManifoldMisc, Topology/NhdsSet, Topology/Germ and Geometry/Algebra/SmoothGerm.

[Michael Rothgang]

I just tried upstreaming Topology/NhdsSet, and am getting a strange error. Three lemmas are fine in isolation, but fail then moved into the main NhdsSet file. (This might be related to a similar-sounding mathport warning. I joined mathlib after the port; this might be easy for a somewhat experienced porter.) The code is at branch#MR-sphere-eversion-topology-nhdsset; insights appreciated.

[Yury G. Kudryashov]

Which lemmas cause problems?

[Yury G. Kudryashov]

Note that this file doesn't import Topology.Constructions, so it doesn't know what's the topology on X × Y.

[Yury G. Kudryashov]

We already have docs#nhdsSet_prod_le (in a strange file, probably should be moved)

[Yury G. Kudryashov]

I would rename Filter.eventually_nhdsSet_of_prod to Filter.Eventually.prod_nhdsSet similar to docs#Filter.Eventually.prod_nhds

[Yury G. Kudryashov]

And similarly Filter.Eventually.union_nhdsSet

[Yury G. Kudryashov]

Filter.Eventually.nhdsSet_forall_mem is the same as docs#Filter.Eventually.self_of_nhdsSet

[Yury G. Kudryashov]

eventually_nhdsSet_iUnion: please add a theorem

theorem nhdsSet_iUnion {ι : Sort*} (s : ι → Set X) : 𝓝ˢ (⋃ i, s i) = ⨆ i, 𝓝ˢ (s i)

(not sure if it should be a simp lemma or not)

[Yury G. Kudryashov]

Then theorems about eventually will be by simp [nhdsSet_iUnion]

[Michael Rothgang]

Thanks for the quick help. Next time I'll open a draft PR to make your life easier :-)

[Michael Rothgang]

Yury G. Kudryashov said:

Note that this file doesn't import Topology.Constructions, so it doesn't know what's the topology on X × Y.

:face_palm: I should go to bed...
However, importing Topology.Constructionsyields an import cycle: Constructions imports Topology.Maps, which imports NhdsSet precisely for Inducing.nhdsSet_eq_comap. :thinking:

[Yury G. Kudryashov]

Then these lemmas can go to Topology.Constructions.

[Michael Rothgang]

PR #9674 (NhdsSet) is now ready for review.

[Yury G. Kudryashov]

#9725 is the first step towards equivariant maps

[Anatole Dedecker]

Yury, are you aware of #6057 ? I don’t know if it’s actually related but I just want to make sure there’s no duplication happening…

[Yury G. Kudryashov]

I think that we need a separate type for this case instead of using MulActionHom with some strange actions like "Nat acts on the domain by adding n * a and on the codomain by adding n * b".

[Yury G. Kudryashov]

We can have an equivalence between 2 definitions.

[Yury G. Kudryashov]

Also, the main objects I want to deal with is the types of monotone AddConstMaps and AddConstEquivs.

[Yury G. Kudryashov]

And these don't fit in MulActionHom at all.

[Anatole Dedecker]

Okay fair enough, I just wanted to check!

[Michael Rothgang]

Can I draw some eyes to the build failures in LocallyFinite and Projection in my bump branch? These are blocking a full build of the project, cannot be sorried away (AFAICT) and make it hard to test sweeping changes, such as bumping to the first upstream PRs.
I have submitted PRs upstreaming files depending on each other: bumping over this would be much easier if I could at least build the entire project. In other words: the sorried proofs are not as urgent, but having a workaround for these failures would be quite helpful for efficiently upstreaming.

I understand we're all not paid for this and have little time.

[Michael Rothgang]

Status update:

• #9674 NhdsSet is ready again (with comments from @Yury G. Kudryashov and @Anatole Dedecker applied, thanks!)
• #9747 (germs w.r.t. the neighbourhood filter) is also ready, depends on #9674
• smooth germs is in progress (but requires more clean-up)

[Patrick Massot]

@Michael Rothgang I fixed the build and merged into master. Thanks a lot for your help with this bump!

[Michael Rothgang]

Thanks a lot for the prompt response!

[Michael Rothgang]

PSA: I just pushed directly to master: a few uncontroversial clean-ups (reducing imports in ToMathlib) and another mathlib bump directly to master (of today morning, before the latest wave of PRs was merged). Two files in ToMathlib and two lemmas are superseded now, and more is in the pipeline.

[Michael Rothgang]

Also ready for review: #9775 (finite sums/products of maps into Lie groups)

[Michael Rothgang]

Current updates on open PRs:

• #9775 (Lie groups) is still open
• #9778 (Topology/Support), two short lemmas
• #9813 (Topology/LocallyFinite), another short lemma
• #9872 (Topology/Algebra/Order/Compact), one pretty short lemma
• #9874 (easy, renaming lemmas)merged now and #9873 (cut-off functions)
• #9810 (HausdorffDistance; 25 lines/three lemmas) is blocked on #9809 (splitting that file)

[Michael Rothgang]

And I bumped mathlib twice, for a few merged PRs. Not too bad overall.

[Michael Rothgang]

Huzzah: three upstreaming PRs have been merged again. (I have bumped mathlib again, and pushed a couple of other small clean-ups.)

New PRs waiting for review:

• #9982 (normed spaces, easy)
• #10001 (four small lemmas about extended charts)
• #10005 (preparatory clean-up) and #10004 (two lemmas about parametric interval integrals)
• #10015 (partitions of unity) , blocked on #9813 (easy lemma about LocallyFinite)merged
• #10019 (two small lemmas partitions of unity), blocked on #10020 (easy lemma about LocallyFinite)

Still awaiting review:

• #9873 (cut-off functions)
• #9810 (HausdorffDistance; 25 lines/three lemmas), blocked on #9809 (splitting that file)
• #9747 (germs w.r.t. the neighbourhood filter) is almost ready, but will certainly benefit from another look

[Michael Rothgang]

Status update:

• I have bumped mathlib again, over a few more merged PRs. (Thank you for the reviews.)
• I also took a look at the leftover sorry's from the big bump four weeks ago and squashed all but four sorries: these will need further attention. Two should be easy in principle (some lemmas changed); the other two are broken simp_rw's (which, unlike the others, are not fixed by adding decide=true or unfoldPartialApplication)

Current list of PRs awaiting PR

• #10004 (parametric integrals)
• #10015 (partitions of unity) - 100 lines, but straightforward
• #9810 (HausdorffDistance; 25 lines/three lemmas), blocked on #9809 (splitting that file)
• #9747 (germs w.r.t. the neighbourhood filter), 200 lines

I'll have to focus on other things in the next weeks, so reviews (while appreciated) are not urgent.

[Michael Rothgang]

I just pushed two mathlib bumps, one to Lean 4.6.0-rc1, and another to today's mathlib (including the Funlike refactor).
In the first bump, one proof in Global/Relation breaks; I presume an erw was brittle and broke due to small rw changes in Lean 4.6.
The second one issues two warnings by lake, apparently going back to lean4#3149:

warning: Qq: ignoring missing dependency manifest './.lake/packages/Qq/lake-manifest.json'
warning: Cli: ignoring missing dependency manifest './.lake/packages/Cli/lake-manifest.json'

Reading the PR, I am not sure if any action is required. (I've left it as-is for now; feel free to make follow-up changes.)

[Michael Rothgang]

Status update:

• #10004 is awaiting review (@Moritz Doll's opinion requested)
• #9872 is ready for review again (@Yury G. Kudryashov's comments addressed)
• #9747 is also ready for another look
• #10303 is awaiting-author. Feel free to adopt, if you want to. (Otherwise, I'll get to it in due time.)

[Patrick Massot]

Thanks!

[Michael Rothgang]

Status update: #9474 and #10004 have been merged, thanks for the reviews. This leaves:

• #9872 is still awaiting review
• new PRs awaiting review: #11108 and #11110 (more lemmas about parametric integrals)
• awaiting review: #10977 (first results about smooth germs, in mathlib-suitable generality)

[Michael Rothgang]

Status update: the first three PRs have all been merged (thanks again for the reviews). Here are a few more:

• #11185 (parametric integrals, again)
• #11264 and #11265 (two lemmas about flags of a basis) - each ~10 lines, so a short review
• #11387 (codimension two subspaces have path-connected complement): a prerequisite for the last PR
• #11341 (continuous affine equivalences): new code written to accommodate the next two PRs
• #11344 (ample sets in real vector spaces), which allows
• #11342 (complements of codimension two subspaces are ample)

The last two PRs basically upstream Local/AmpleSet.lean --- this would be the first file outside of ToMathlib being upstreamed (this year). Reviews welcome, as always.

[Michael Rothgang]

I just tried bumped the mathlib, to using Lean 4.8-rc1. As usual, most of it was unspectacular, but four proofs break in new and exciting ways I don't understand. I have added notes referring to the version 4.8-rc1. Help in fixing some of these darker corners is welcome.

[Ruben Van de Velde]

Do you have a link?

[Michael Rothgang]

The commit is here; search for "4.8-rc1". (I forgot to remove WIP from the commit message when pushing, oh well.)

[Michael Rothgang]

Current list of related PRs awaiting review:

• #10977 (germs of smooth functions, part 1)
• #11342 (complements of codimension two subspaces are ample, a small one)
• #12673 (small lemma about C¹ and Lipschitz functions)

#11185 (continuity of primitives for parametric integrals) needs some small review comments to be addressed.

[Ruben Van de Velde]

I was hoping I'd pick up on something without running the code, but no such luck. Maybe I'll have a little time tonight

[Patrick Massot]

Thanks Michael, I’ll take a look. Could you please avoid pushing sorries to the master branch? You can create bump branches in that kind of situation.

[Patrick Massot]

OMG, master is full of sorries! How long have you been doing this?

[Patrick Massot]

Michael, you will probably be interested in reading https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/changes.20to.20apply.20magic.20in.204.2E8.2E0/near/437299067

[Patrick Massot]

I’m done restoring axiom-free main theorems. Please everybody, do not push to master changes that introduce the use of axioms in SphereEversion.Main. Branches are cheap!

[Michael Rothgang]

Patrick Massot said:

Michael, you will probably be interested in reading https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/changes.20to.20apply.20magic.20in.204.2E8.2E0/near/437299067

Oh wow - I had no idea. Thanks for investigating!

[Michael Rothgang]

Thanks for the help and sorry for the mess I inadvertedly created. (To be clear, I only sorried broken proofs, nothing else: to me, that seemed better than not bumping the project - but I will do differently going forward.)

[Michael Rothgang]

Which means: creating a bump branch and posting here if bumping turns up an error I cannot solve.

[Patrick Massot]

Doing this was much better than not helping, but creating a branch would have been even better.

[Michael Rothgang]

I have a WIP branch updating to the most recent mathlib (with one unsolved sorry; I'll ask if I can't solve that). In case you'd like this to land soon, let me know --- otherwise, I'll get to this end of this week or sometimes next week.

[Patrick Massot]

I won't have time soon. I'm leaving Pittsburgh tomorrow and will be back to work only in the middle of next week.

[Michael Rothgang]

Michael Rothgang said:

I have a WIP branch updating to the most recent mathlib (with one unsolved sorry; I'll ask if I can't solve that). In case you'd like this to land soon, let me know --- otherwise, I'll get to this end of this week or sometimes next week.

An update: I have completed the bump to mathlib v.4.9.0 and just pushed this to master.
The MR-bump-4.10-rc1 branch has a WIP bump to 4.10-rc1: LocalisationData fails to build pretty badly; help would be appreciated here.

[Michael Rothgang]

I just saw that CI failed on master, because the lakefile needs some fix-up to build doc-gen4 as well.

[Michael Rothgang]

I realised how to fix the bump to Lean 4.10: I'll push a bump to 4.10-rc2 in a moment. (I'm not sure what is needed for doc-gen4; help on this is still welcome.)

[Yury G. Kudryashov]

I fixed 3 warnings about refine'.

[Yury G. Kudryashov]

I run lake exe shake --fix but it failed to minimize Mathlib imports.

[Michael Rothgang]

Thanks for these clean-ups! Let me bump mathlib to 4.10.0... done and pushed.
And I switched the project to a lakefile.toml.

[Yaël Dillies]

Yes, I have the same problem in all my projects. Seems like shake just doesn't try removing cross-project imports?

[Yury G. Kudryashov]

Found out: you have to call lake exe shake --fix SphereEversion.

[Michael Rothgang]

This branch completes most work towards bumping to mathlib 4.12. Remaining items are

• fix two proofs I sorried for now
• fix the error in InnerProductSpace/Projection.lean
• see which warnings remain afterwards (not many, I think)
• clean up the history, summarise the changes made

[Ruben Van de Velde]

I'm taking a look at the bump

[Ruben Van de Velde]

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

[Michael Rothgang]

Thanks a lot, the PR looks great to me!

[Ruben Van de Velde]

I guess I didn't do the last part of your list (summarise the changes made). Not sure if anyone is waiting for it, though

[Michael Rothgang]

I can do so by Monday

[Patrick Massot]

Thanks a lot Michael and Ruben! I understand that most of the diff is related to the new variable command. I looks a bit painful but I understand that having a nicer fix would be a lot of work. I left three questions about changes that look totally unrelated to this.

[Ruben Van de Velde]

Commented. Agreed that the variable changes aren't fantastic, but I think it would be best to defer more work on making them nicer to a future PR (which, full disclosure, I probably won't be making)

[Michael Rothgang]

I just addressed the last comment, squashed the commits a bit (indicating which overall changes were necessary) and merged the PR.

[Michael Rothgang]

To avoid duplicate work: I'm working on bumping this project to Mathlib 4.13.0. If you need this urgently, please ping me - otherwise, this should get completed within two weeks.

[Patrick Massot]

Thanks!

[Michael Rothgang]

For the record: that bump has been merged three weeks ago.

[Michael Rothgang]

branch#MR-bump-4.14 contains an in-progress bump to current mathlib. There is a bunch of work left; the removal of Smooth{At} was a bit painful. I would prefer to land this bump, before bumping over the upcoming analyticity refactor.

[Michael Rothgang]

I just pushed another round of fixes to that branch. There are 10-20 sorries left; help with these very welcome.

[Michael Rothgang]

Opened https://github.com/leanprover-community/sphere-eversion/pull/88 with the current branch.

[Sébastien Gouëzel]

I'll have a look. I hope it frees you some time for #19696 :-) (it's a joke, please don't feel any pressure here)

[Sébastien Gouëzel]

Everything should be fixed in https://github.com/leanprover-community/sphere-eversion/pull/89 (it's a PR to your branch, not to master). Well, I haven't fixed the files in Unused as their status is not clear to me.

[Sébastien Gouëzel]

I think the bump was much easier to do for me because I know exactly what has changed in Mathlib. I'll also do the bump once #19696 lands, because again it will probably be much faster for me.

[Michael Rothgang]

Thanks a lot! I've merged the bump into my branch. If I don't hear further comments, I'll (aim to) merge my bump tomorrow.

[Patrick Massot]

Thanks a lot Michael and Sébastien. I see that some local notation "∞" => (⊤ : ℕ∞) disappeared. Is it now problematic?

[Yury G. Kudryashov]

Now ∞ is a scoped notation for ((⊤ : ℕ∞) : WithTop ℕ∞)

[Yury G. Kudryashov]

I guess, this may conflict with this local notation.

[Patrick Massot]

Ok, this should be good then. I think I was misled by some Smooth that became ContDiff ℝ ⊤ but actually ContDiff ℝ ∞ should be usable there as well.

[Patrick Massot]

Oh and I see some statement have been actually strengthened to “this map is analytic”. That’s nice!

[Patrick Massot]

Ok, some changes are a bit painful, but less than I feared. Thanks again @Michael Rothgang and @Sébastien Gouëzel. This help is appreciated!

[Michael Rothgang]

#20585 (a re-done version of #10303) is ready for review again

[Michael Rothgang]

Review comments addressed, by the way

[Ruben Van de Velde]

Will check your question when I get on my laptop

[Ruben Van de Velde]

@Michael Rothgang it does compile here

[Michael Rothgang]

Let's see if CI likes it. If it does, I'm also happy :-)

[Patrick Massot]

Thanks!

[Michael Rothgang]

By the way: I took a look at Sebastién's PR https://github.com/leanprover-community/sphere-eversion/pull/90, and think it looks good. I think it could be merged.

[Ruben Van de Velde]

Re: upstreaming, there's now #21884 and companion https://github.com/leanprover-community/sphere-eversion/pull/97

[Michael Rothgang]

I have approved the mathlib PR: if that lands, you could even combine that with a bump removing the entire file :-)

[Ruben Van de Velde]

Replied

[Michael Rothgang]

@Ruben Van de Velde @Pietro Monticone In case you're looking for further upstreaming ideas, I can offer a few:

• ToMathlib.Topology.Path: the strans definition and supporting lemmas could be worth it - i.e., generalising docs#Path.trans in terms of it.
• the estimates in ParametricIntervalIntegrals are worth having in mathlib. There is a comment mentioning different possible designs; maybe Floris or Patrick can provide useful context here.
• the result in Algebra/Ring/Periodic.lean also feels like a doable target: the hardest part is probably figuring out what the right general statement is/what mathlib already has

[Michael Rothgang]

Status update: I've merged Pietro's sphere-eversion#98, am happy to merge Ruben's sphere-eversion#99 after merging in the mathlib bump, and just pushed a bit of fun_prop golfing in sphere-eversion#100.

[Ruben Van de Velde]

Updated sphere-eversion#97

[Patrick Massot]

Thanks everybody!

[Patrick Massot]

But sphere-eversion#97 doesn’t build

[Patrick Massot]

I’ll fix that.

[Patrick Massot]

Fixed

[Patrick Massot]

I also removed a couple of outdated things from the parametric integral file.

[Patrick Massot]

Michael, does this removal answer your question?

[Michael Rothgang]

Thanks for fixing and sorry for the hassle. (If you add CI to PR branches, I'll make sure to only merge building PRs. Or perhaps @Pietro Monticone wants to help? I think one can presumably cargo-cult from the Carleson project.)

[Michael Rothgang]

Patrick Massot said:

Michael, does this removal answer your question?

It certainly helps, thanks!

[Ruben Van de Velde]

Oops, sorry for not re-testing

[Pietro Monticone]

Ok, I’ll do it later today or tomorrow.

[Pietro Monticone]

Done sphere-eversion#101

[Patrick Massot]

That PR does not seem to be about what is mentioned in the description. Did you push the wrong branch?

[Pietro Monticone]

I enabled CI on PR events as asked by @Michael Rothgang:

If you add CI to PR branches, I'll make sure to only merge building PRs. Or perhaps @Pietro Monticone wants to help?

Did I miss anything?

[Patrick Massot]

Oh maybe I was confused because there is only one workflow in this project. It’s a bit confusing to call it blueprint.yml if it’s also checking the project, but I guess this is a historical accident.

[Patrick Massot]

Ok, I merged it since I don’t know how to test it in any other way.

[Bhavik Mehta]

Patrick Massot said:

It’s a bit confusing to call it blueprint.yml if it’s also checking the project, but I guess this is a historical accident.

This has confused me a couple of times too, it's surely not too bad to rename it, especially in templates right?

[Pietro Monticone]

Yes, maybe a more generic build.yml would be better.

[Pietro Monticone]

Here is the related PR: leanblueprint/#67

[Kevin Buzzard]

Talking of things which confuse people, the title of this thread confuses me on a pretty much daily basis

[Patrick Massot]

For some reason, this channel became a single thread channel :man_shrugging:

[Michael Rothgang]

I'm very happy to move most of this thread into a new one "Mathlib bumps". Let me try to do so. Edit: moved what I could.