!4#3388 (revert porting of to_interval_mod)

Stream: mathlib4

[David Loeffler]

Are we any closer to a decision on what should happen about PR !4#3388? It's blocking porting of topology.instances.add_circle, which is otherwise ready to port, and is a dependency many other files.

(As a recap: the issue was whether or not to_interval_mod should be un-ported, and porting of it and its dependents held up, pending completion of mathlib3 PR #17743.)

[Eric Rodriguez]

Wow, the sorries are still there...

[Eric Wieser]

David, do you have a specific target in mind (beyond add_circle) that depends on this file? If so, the dependency graph might be instructive regarding whether this is a small or large blocker

[Eric Wieser]

(for instance if port-status#topology/instances/add_circle can be ported tomorrow but the next file in the chain you care about is 20 dependencies away from a different root, then the urgency is illusory; but if the longest chain of unported files leads to add_circle then your concern is very poignant)

[Eric Wieser]

Eric Rodriguez said:

Wow, the sorries are still there...

The fact that an intuitively obvious statement is so difficult to prove has made Yaël and I consider some larger refactors to the contents of that file; the intent was to try to get those refactors in before the tide ends up half way through them.

[David Loeffler]

Eric Wieser: David, do you have a specific target in mind (beyond add_circle) that depends on this file? If so, the dependency graph might be instructive regarding whether this is a small or large blocker [...] (for instance if port-status#topology/instances/add_circle can be ported tomorrow but the next file in the chain you care about is 20 dependencies away from a different root, then the urgency is illusory)

It's a prerequisite for analysis.complex.arg for instance (which is, in turn, a prereq for Quadratic Reciprocity, which has been one of the chosen targets in the porting-status updates since the beginning of the port).

Consulting the dependency graph (https://leanprover-community.github.io/mathlib-port-status/file/analysis/complex/arg) suggests that the other dependencies for analysis.complex.arg are falling into place quite rapidly, and add_circle will soon be the main blocker here.

[Eric Wieser]

How about we set a deadline of (next) Friday for me to salvage what I can from the mathlib3 PR, and re-evaluate before then if the graph above becomes more lopsided?

[Eric Wieser]

port-status#number_theory/legendre_symbol/quadratic_reciprocity#graph is I assume the other relevant graph

Here, it looks like we don't start to break into blocked-by-to_interval_mod territory until we're through a fair number of painful algebra files

[David Loeffler]

Eric Wieser said:

The fact that an intuitively obvious statement is so difficult to prove has made Yaël and I consider some larger refactors to the contents of that file; the intent was to try to get those refactors in before the tide ends up half way through them.

Eric, I wonder if you have considered the optics of this situation. Plenty of people in this community have (sorry-free and finished) contributions to mathlib which they'd like to get merged, and are having to put up with either long delays, or tedious forward-porting, or both, because the importance of the mathlib4 port overrides that of their personal pet projects.

As a maintainer, shouldn't you be leading by example, rather than assuming that your personal project is exempt from the rules that apply to other contributors?

[David Loeffler]

Eric Wieser said:

port-status#number_theory/legendre_symbol/quadratic_reciprocity#graph is I assume the other relevant graph

Here, it looks like we don't start to break into blocked-by-to_interval_mod territory until we're through a fair number of painful algebra files

I think analysis.special_functions.pow is also relevant; it is a dependency for a huge amount of stuff all across mathlib. See https://leanprover-community.github.io/mathlib-port-status/file/analysis/special_functions/pow#graph

[Eric Wieser]

Eric Wieser said:

Plenty of people in this community have (sorry-free and finished) contributions to mathlib which they'd like to get merged, and are having to put up with either long delays, or tedious forward-porting, or both, because the importance of the mathlib4 port overrides that of their personal pet projects.

I would strongly encourage any contributor with a project about to be swallowed by the tide to post in #PR reviews noting their situation, and to (carefully) add an entry to #port-comments to avoid the message being missed. A mathlib 3 PR merged before the port reaches it is a win for everyone; mathlib gets more powerful, the contributor doesn't have to forward-port, and the reviewers don't have to review a forward-port.

[Eric Wieser]

I am in a bad timezones to continue this discussion today, apologies

[Johan Commelin]

I'm not sure this should wait till Friday. The porting comment has been in place for a pretty long time. The porting comments are meant to be pretty transient I would think. They shouldn't hold things up for weeks on a row. And by now topology.instances.add_circle has been hovering at the top of "Unported files with all their dependencies ported" for a really long time. In one or two days, it will be at the top of "Unported files, period". There's only a handful of files above it that have a few unported dependencies.

[Scott Morrison]

I had an update from Eric earlier today on this --- it seems like things are about to start moving again.

[Eric Wieser]

Note that if the titular PR were abandoned today, it would unblock exactly one file in the graphs above before we end up blocked again by port-status#analysis/normed/group/quotient which has been waiting two weeks for help.

[Yaël Dillies]

And indeed #17743 is now sorry-free, so expect our project to reach mathlib very soon.

[Eric Wieser]

I think to maximize the speed at which we can do so it would be best to merge !4#3388 today; doing so will give us a clean mathport slate tomorrow, rather than having to deal with a nightmare of alignment warnings

[Scott Morrison]

Okay, shall I merge now?

[Eric Wieser]

Please!

[Scott Morrison]

@Eric Wieser , !4#3388 has hit master now.

[Eric Wieser]

Great! #18912 is waiting for a final naming bikeshed, then we should be ready to finalize #17743

[Scott Morrison]

Let's not wait on a name, I'd like to get this out of the way. :-) Change it to add_comm_group.modeq and call it done?

[Yaël Dillies]

I'm working on improving the API right now, btw.

[Eric Wieser]

(in case it's not clear, I made the change Scott suggested)

[Eric Wieser]

Eric Wieser said:

How about we set a deadline of (next) Friday for me to salvage what I can from the mathlib3 PR, and re-evaluate before then if the graph above becomes more lopsided?

Just to give an update on this, since it's Friday:

• We're not really any closer to any of @David Loeffler's targets (port-status#analysis/special_functions/pow#graph, port-status#number_theory/legendre_symbol/quadratic_reciprocity#graph); anything nontrivial related to the additive circle seems blocked by !4#3457 (port-status#analysis/normed/group/quotient), which has been marked help-wanted for quite some time.
• The original PR, #17743, is sorry-free and passes CI
• There is one new mandatory dependent PR, #18942
• #18941 is an extra refactor that doesn't need to be in before #17743, but would be nice to have. Yael and I are still working out some disagreements over this.

[Mauricio Collares]

If you give me mathlib4 commit access (collares on GitHub) I can add the shameful maxHeartbeats bumps to !4#3457 myself :)

[Eric Wieser]

I've granted you access, though I think we should also consider backporting the other changes in that PR

[Notification Bot]

12 messages were moved from this topic to #mathlib4 > maxHeartbeats by Eric Wieser.

[Eric Wieser]

A final update:

• #17743 is ready for a final round of review
• port-status#algebra/modeq will be ready for porting tomorrow (it's a new dependency)
• Thanks presumably to some import pruning, the critical path to https://leanprover-community.github.io/mathlib-port-status/file/analysis/special_functions/pow#graph is now tied between algebra.modeq and is_R_or_C; so it seems the timing was just about right.

[Scott Morrison]

Okay, I hit merge on #17743. Let's get this done. :-)

[Eric Wieser]

Thanks again @Mauricio Collares for tieing off all the sorries so that we could finish this off!

[Jeremy Tan]

!4#3952 is the re-port and is now ready for review

[Eric Wieser]

@David Loeffler, as of earlier today you're now completely unblocked on porting port-status#topology/instances/add_circle :)