forward porting

Stream: mathlib4

[Scott Morrison]

I'm a bit worried that https://leanprover-community.github.io/mathlib-port-status/out-of-sync currently has 87 entries, and would like to pay down some of this debt.

[Scott Morrison]

@Eric Wieser, would it be possible to make the list sortable by the age of the "verified at" commit, rather than the sha itself?

This would be useful for identifying the egregious cases where the forwarding porting should have happened long ago.

[Scott Morrison]

Otherwise, I was thinking to take the following steps:

• make an effort to approve forwarding port PRs that are ready to go, which will hopefully reduce the list some
• collate the out-of-sync files according to the author of the mathlib3 PR, and then message them reminding them about their list of forwarding porting jobs
• start dealing with the ones that appear to be abandoned by their authors.

[Scott Morrison]

If anyone has advice on how I could move this along more effectively, I'm happy to hear. :-)

[Eric Wieser]

https://github.com/leanprover-community/mathlib4/pull/2926 will shrink that number by 5, and has already been reviewed :)

[Eric Wieser]

What do you mean by "age of the verified at" commit?

[Eric Wieser]

Is that interesting? Doesn't that just mean that the original port was long ago, not the mathlib3 PR that since made it out of sync?

[Eric Wieser]

Adding authors to the out-of-sync table was in the back of my mind; not least because I'm sure there are forward-ports I've forgotten about myself

[Eric Wieser]

@Yaël Dillies forward-porting #17961 (which only just landed) will knock down the list by another 8.

[Scott Morrison]

Yes, you're right, sorry, I want to sort by the age of the mathlib3 PR, which I now understand I can already do, by sorting on the mathlib3 changes column.

Am I right, then, that category_theory.structured_arrow is the "longest out-of-sync" file, then?

[Eric Wieser]

I think sorting on the "changes in mathlib3" columns sorts by "most out of sync"

[Eric Wieser]

As in "has the most independent PRs touching this file"

[Eric Wieser]

Ah I see the confusion

[Eric Wieser]

"newest first" means "within the cell, the commits are in this order" not "the rows are sorted this way"

[Eric Wieser]

So the conclusion is that set_theory.zfc.basic is massively out of sync; but that's probably fine because the porting PR was abandoned anyway, and we should throw it out and start over

[Eric Wieser]

algebra.star.self_adjoint is next most out of sync, which is my fault and I intend to address by reporting the file from scratch

[Eric Wieser]

"date of oldest unsynced mathlib3 change" would be a reasonable new column to add

[Scott Morrison]

Ugh, this is such a mess.

As an example: https://leanprover-community.github.io/mathlib-port-status/file/data/list/perm shows that there are three different mathlib3 PRs that touched this file.

There is an open PR for mathilb4, namely !4#3076, which updates the SHA, but does not make any mention of those three PRs.

In fact, the three mathlib3 PRs mentioned there have all actually been forward ported, but apparently in PRs that did not update the SHA, e.g. https://github.com/leanprover-community/mathlib4/pull/1509.

But it takes 20 minutes to decipher this and work out what to do, let alone do it. And there are 86 others on this list.

[Scott Morrison]

Unless I'm misunderstanding how bad this is, I think we need to hard freeze already ported files.

[Eric Wieser]

I would guess that about 1/3 of the mess is actually backports of refactors that happened during porting

[Eric Wieser]

Those are the ones that usually take longest to decipher

[Eric Wieser]

Which is to say; you picked a particularly nasty example

[Eric Wieser]

!4#3005 is an example of what the easy end of the spectrum looks like

[Scott Morrison]

Okay, I've dealt with everything on the #queue4 with label mathlib-pair, except for

• https://github.com/leanprover-community/mathlib4/pull/3101, which @Eric Wieser had self-assigned, and
• https://github.com/leanprover-community/mathlib4/pull/3077, which I've assigned to @Yaël Dillies, who I think wants to make further mathlib3 changes before resolving this one.

[Scott Morrison]

Now on to the things not on the #queue4, I guess. :-)

[Yaël Dillies]

!4#3077 is now on the queue. The fixes were already made on the mathlib side.

[Scott Morrison]

Thanks!

[Scott Morrison]

https://leanprover-community.github.io/mathlib-port-status/file/algebra/order/absolute_value

is ... not looking healthy. It is way out of date with master. @Yaël Dillies, would you be able to update us on what should happen here?

[Yaël Dillies]

The open forward-porting PR (!4#1238) is completely stuck due to obscure errors I have no idea how to fix.

[Yaël Dillies]

Incidentally, we since found out that docs#mul_ring_norm was mathematically a duplicate of docs#absolute_value. So I think the correct thing to do here is to give up on my current porting PR, fix mathlib3, then report.

[Eric Wieser]

Scott Morrison said:

https://leanprover-community.github.io/mathlib-port-status/file/algebra/order/absolute_value

is ... not looking healthy. It is way out of date with master. Yaël Dillies, would you be able to update us on what should happen here?

This one is particularly bad because the change happened before we were tracking SHAs properly (see github comment)

[Yaël Dillies]

And Jireh forward-ported part of the changes. So there isn't a SHA that you can meaningfully track.

[Eric Wieser]

So I think the correct thing to do here is to give up on my current porting PR

agreed

fix mathlib3

possible not worth it

then report.

Agreed, I think it would be easiest to start from a clean mathport oneshot output

[Yaël Dillies]

There's a separate reason why we should fix mathlib3: We are missing absolute_value_class, which seems to have hindered the original port.

[Scott Morrison]

I don't like that things like https://github.com/leanprover-community/mathlib4/pull/1470 are labelled as mathlib-pair at this point. They are empty placeholder PRs, and should be labelled to reflect this. Maybe future-mathlib-pair?

I want to try and deal with as much of the mathlib-pair list as possible, and these ones are just a distraction (and my preferred solution to them is "close the underlying mathlib3 PR", but I'm not necessarily advocating that today :-).

[Yaël Dillies]

Well, they aren't labelled awaiting-review

[Scott Morrison]

Yes, but we are so far behind on dealing with forward porting issues, that we need to be going through all these PRs, to understand their status and get them moving again. So it's not good enough to just say "it's not labelled awaiting-review, so we can ignore it".

[Scott Morrison]

The point being that once we don't have a backlog of mathlib-pair PRs, we can start following up with the "owners" of forward porting obligations. While there is a backlog this is hard to do.

[Scott Morrison]

I might add blocked-by-other-PR labels to mathlib-pair PRs where the mathlib3 PR has yet to be merged? Or should I just add an explicit label for this?

[Yaël Dillies]

I don't understand. Surely the presence of matching up PRs helps, right?

[Scott Morrison]

Yes! I want the matching up PRs

[Scott Morrison]

I just want to know that they are only there as placeholders for future work.

[Eric Wieser]

If we remove mathlib-pair labels from the placeholders then they won't show up in the dashboard, which in turn means that people might recreate them

[Yaël Dillies]

Do you know about the mathlib4 project Eric made?

[Eric Wieser]

I consider that a failed experiment

[Scott Morrison]

I do want to keep the mathlib-pair label on them.

[Scott Morrison]

I just want some additional label that shows that the mathlib3 PR hasn't even been approved yet.

[Eric Wieser]

I think in practice the need to create placeholder PRs is now gone

[Eric Wieser]

We should keep around the old ones to fulfill the promises in the mathlib3 commits that reference them

[Yaël Dillies]

In https://github.com/orgs/leanprover-community/projects/4 there already is a place for matching up PRs whose mathlib PR hasn't gone through yet.

[Scott Morrison]

I don't understand what https://github.com/orgs/leanprover-community/projects/4 is useful for, sorry. It seems to be showing me the things I don't care about, rather than the things I do. :-)

[Eric Wieser]

I built it as an attempt to be useful, but concluded it didn't really hit the mark. @Jon Eugster's improvements to the dashboard largely replace it.

[Eric Wieser]

The data there is all out of date now because I stopped updating it

[Eric Wieser]

Eric Wieser said:

Adding authors to the out-of-sync table was in the back of my mind; not least because I'm sure there are forward-ports I've forgotten about myself

Done. @Yaël Dillies, @Yury G. Kudryashov, and I are each responsible for about 15 files 18, 13, and 9 files respectively

[Yury G. Kudryashov]

I'll have a look later tonight.