!4#2148

Stream: mathlib4

[Matthew Ballard]

FWIW !4#2148 should be ready to go including forward ports of the ML3 changes. It appears that the file was ready to go in early Feb (ie all green and marked for review) but the author was waived off due to wip #17743. The following month, #17483 and #18427 were merged into ML3. It was marked help-wanted and wip two weeks ago.

[Eric Wieser]

I'd still prefer to wait for #17743

[Jeremy Tan]

@Matthew Ballard can you help make #17743 pass CI again?

[Eric Wieser]

Jeremy, it never did pass CI

[Jeremy Tan]

It did: https://github.com/leanprover-community/mathlib/pull/17743/commits/b478cb2047f6516cca2930978749d8e7352f808f

[Eric Wieser]

But until to_interval_mod is near the top of the porting dashboard, I see no reason to rush ahead with porting it

[Yaël Dillies]

Jeremy, this branch is trying to provide an instance of circular_order for add_circle. Never has this instance been sorry-free.

[Yaël Dillies]

But indeed if we remove the 36 commits that this branch is adding, then it passes CI.

[Yaël Dillies]

Please stop jumping to conclusion and try understanding the context.

[Notification Bot]

11 messages were moved here from #general > New policy regarding mathlib3 PRs that touch ported files by Eric Wieser.

[Eric Wieser]

It appears that the file was ready to go in early Feb (ie all green and marked for review) but the author was waived off due to wip

Note that #port-dashboard has always said "please don't port this file yet"; so the fact that the author ported only to realize that they should wait for #17743 is on them

[Eric Wieser]

Note right now that there are still 50 higher priority files to port, so I don't think we need any urgency here until that number reaches around 10

[Matthew Ballard]

Whatever people want to do with it is fine with me. It was vigorously pointed at in the other thread so I took a look. Only was about 15 minutes of (non-focused) time.

[Ruben Van de Velde]

It landed, fwiw

[Eric Wieser]

Why did we merge it when #port-dashboard says "please wait"? I don't see any discussion saying "let's override that"

[Matthew Ballard]

Odd. Never got an email with updated comments.

[Eric Wieser]

!4#3388 reverts the landing; the file isn't urgent, there were multiple comments against merging it, it being merged makes forward-porting harder, and we always can revert the revert if it becomes urgent

[Matthew Ballard]

What is top 10?

Would be nice to finish mathlib3#17743 first

is this British for "touch it and lose a finger" :lol: ?

[Eric Wieser]

In hindsight I should have used stronger wording, this is certainly partly on me!

[Matthew Ballard]

Yeah, I probably shouldn't have marked it awaiting-review also.

[Matthew Ballard]

I thought it would start a conversation but I should have at least left a comment after

[Matthew Ballard]

I think turning it back into a PR makes sense though I imagine people will want clear triggers for future action, which is why I asked about the meaning of top 10.

[Eric Wieser]

I meant "there are fewer than 10 unported files with at least as many dependents as it"

[Matthew Ballard]

Not just counting open PRs?

[Eric Wieser]

Open PRs isn't really an interesting metric. "Openable" PRs (dependencies all ready but no PR open yet) might be.

[Matthew Ballard]

Ie green?

[Eric Wieser]

I think "in the top 10 on #port-status" amounts to that

[Matthew Ballard]

I think it might be # 10 right now.

[Jeremy Tan]

Un-port the file, then we'll see

[Matthew Ballard]

It has 270 dependientes. So it’s # 11. Probably around # 60 overall

[Matthew Ballard]

I think higher cutoff., eg top 5, would work also.

[Matthew Ballard]

Or top 10 overall as long as it’s clear

[Eric Wieser]

I think the first to be relevant of those two conditions is reasonable

[David Loeffler]

I just woke up (in US west coast time) and saw that overnight, !4#2148 had been merged and then unmerged, with the comment

We should wait; there is no urgency to merge this, and no discussion took place that argued against waiting.

I think merging the port PR was the right decision, and I am strongly against unmerging it.

The general policy regarding mathlib3 PR's during the port has always been that the port takes priority, and it is the obligation of mathlib3 contributions to avoid getting in the way of the porting effort; and this policy has been tightened up repeatedly (e.g. in yesterday's announcement). Yet somehow all the rules are being suspended for #17743, and porting of the file it touches is being put on hold. Given the effort that authors of other mathlib3 PR's – including myself – have put into jumping through all the forward-porting hoops, it seems highly unfair that this particular PR is being feather-bedded.

This is all the more puzzling given that #17743 is, quite frankly, a mess. As has been pointed out elsewhere in this thread, it does not pass CI, and never has done. Development there has been stalled since mid-January. It is built on shaky foundations since there are unresolved design issues with an instance diamond in circular_order. Finally, the mathematical structure it deals with seems something of a niche interest: the file circular_order has precisely zero imports in the library.

Please, let's un-revert and merge !4#2148 so we get to_interval_mod ported. It's a prerequisite for lots of important stuff: e.g. the complex log function, and add_circle, which is foundational for the whole Fourier theory library and also for a bunch of number-theory results around Diophantine approximation.

[Johan Commelin]

It would have been nice to have a short discussion before merging the PR. But I agree that I don't think this needed to be reverted.

[Jeremy Tan]

@David Loeffler I closed the mathlib4 PR that would have reverted the merge, !4#3388

[Jeremy Tan]

It has not been unmerged. It is in there. And we can proceed with Topology.Instances.AddCircle

[Sebastien Gouezel]

Jeremy Tan said:

David Loeffler I closed the mathlib4 PR that would have reverted the merge, !4#3388

It is not your responsability to close someone else's PR. You can try to convince the PR author to close it, or the maintainers not to merge it, but closing it right away is disrespectful and should be forbidden.

[Sebastien Gouezel]

(For the record, I wouldn't unmerge !4#2148, but that's not the question here).

[Eric Wieser]

The general policy regarding mathlib3 PR's during the port has always been that the port takes priority, and it is the obligation of mathlib3 contributions to avoid getting in the way of the porting effort;

In this case, it feels a bit like plowing through a road closed sign on a side street instead of staying on the main road. This file was not at any point raised as blocking the port.

While we have the ability to steer the port (ie, we remain bottlenecked by review time not available files), IMO all other things equal we should steer it to minimize conflicts with open mathlib3 PRs that to maximize them.

[Jeremy Tan]

Loeffler has given a more convincing argument for his side of the case

[Jeremy Tan]

That we should not wait for the mathlib3 PR to be merged

[David Loeffler]

In this case, it feels a bit like plowing through a road closed sign on a side street instead of staying on the main road.

To push the metaphor a little further, that side street does need to be plowed at some point, and the parts of mathlib that I personally most care about (and would be interested in helping to port) are snowed-in beyond it :-). :snowy:

[Eric Wieser]

In that case, my objection is that your concern was not ever voiced; with a day or two of warning I would have swept up the parts of the mathlib3 PR that were salvageable and tabled the rest

[Jeremy Tan]

What do you mean, sweep up?

[Jeremy Tan]

Which parts of the mathlib3 PR are salvageable at this point?

[Jeremy Tan]

In any case though, sorry @Eric Wieser for disturbing your revert PR