Merging mathlib3 PRs before creating forward-ports

Stream: mathlib4

[Eric Wieser]

As discussed in the meeting, our current approach of

Every mathlib3 PR that touches a ported file must come with an accompanying mathlib 4 forward-port PR before either can be merged

doesn't mesh well with the fact that mathport doesn't produce the auto-ported output in CI until the mathlib 3 commit is merged. In practice, this means that all forward-ports end up being ad-hoc ports rather than mathport-guided ports.

Given that it sounds like mathport is already well-equipped to track what is and isn't ported, is there any reason to continue with this approach? I would argue we should just merge the mathlib3 PRs, let mathport rerun, and then request that the author make a forward-port PR now that mathport has done 90% of the work.

[Eric Wieser]

While mathport already tracks things that haven't been ported yet, we could also create a needs-forward-port label to attach to closed PRs, so that we have an easy way to ping authors who forget to follow up.

[Scott Morrison]

I'm just worried that responsibility for tracking down unported changes doesn't have a clear owner.

[Eric Wieser]

We already have this problem though, it's all the items on the "modified since the commit at which they were verified" list in #port-status

[Scott Morrison]

Indeed.

[Eric Wieser]

These can happen due to race conditions where the mathlib3 PR is approved, then someone starts porting the file to mathlib4, then the mathlib3 file is merged, and then the port of the old version is merged

[Eric Wieser]

I'd argue the responsibility for tracking down unported changes is mathport itself, which should have the information to do so even if we haven't fully built the UX yet (this was discussed a bit in todays meeting)

[Scott Morrison]

Here's a thought: can updating the git shas in the headers in mathlib4 become the responsibility of the authors who make the matching PRs?

Something like:

• create your PR for mathlib3
• either notice yourself, or have someone point out, that it touches files that have been synchronized
• create a PR for mathlib4: it's okay if you either port the changes by hand, or create an empty PR with the intention of doing it using mathport after the mathlib3 PR is merged. However if you do this, it needs to have a special label deferred-mathlib3-pair, or something.
• that PR for mathlib4 should update the git shas in the headers, after the mathlib3 PR has been merged but before it gets merged.

Ideally then the only time there are ever discrepancies between mathlib4 and the corresponding files in mathlib3, there is an deferred-mathlib3-pair PR open.

Rather than looking at the output of port_status.py (which is painful, unfun, and easy to hope someone else will do), we can instead just stay on top of PRs marked deferred-mathlib3-pair.

[Scott Morrison]

Separately and more simply than that, is it okay if when I bors d+ any of the current mathlib3-pair PRs, I explicitly say: "please update the git shas in the headers of these files, after the mathlib3 PR has been merged"?

[Reid Barton]

I think "update the mathlib4 sha after making a change to mathlib3" is sort of the wrong way to think about it.
The problem is there might be other changes to the same mathlib3 file (either simultaneously, or that just weren't noticed).

[Reid Barton]

The better approach is "pick a file in mathlib4, and make sure all the mathlib3 changes in the range old_commit..HEAD have been ported"

[Scott Morrison]

Okay, sure, that's right. But whose job is that?

[Scott Morrison]

I'm suggesting that when you make a PR to mathlib3 that changes a ported file, it is also your responsibility to make a PR to mathlib4 that then checks all the changes in the range old_commit..HEAD have been ported.

[Scott Morrison]

I'm going through the output of the # The following files have been modified since the commit at which they were verified. section of port_status.py now, but my intention is to make the authors of these changes fix things, not do it myself. :-)

[Reid Barton]

Yes that seems okay to an extent, but the worry is that someone might just not do it (since the mathlib3 PR then has to be merged first anyways)

[Yaël Dillies]

Scott Morrison said:

Okay, sure, that's right. But whose job is that?

It happened a few times that I've opened a mathlib4 PR and noticed there was more stuff missing than what I just added, and it was fine to deal with.

[Yaël Dillies]

So I think it's fine to make the PR author responsible of adding everything that's missing until their PR.

[Scott Morrison]

Reid Barton said:

Yes that seems okay to an extent, but the worry is that someone might just not do it (since the mathlib3 PR then has to be merged first anyways)

Hence my suggestion that we ask authors of mathlib3 PRs to open mathlib4 PRs before we merge their mathlib3 PR, even if we allow that mathlib4 PR to be empty. If all such empty mathlib4 PRs get labelled deferred-mathlib3-pair (or whatever), then the main task becomes to periodically ping the owners of such PRs asking them to do the update.

Maybe this is too much overhead; but I think we need something to avoid accumulating too much in the # The following files have been modified since the commit at which they were verified section.

[Winston Yin (尹維晨)]

Or we make it part of the whole community's porting workflow. Add a flag on an item of ... all dependencies ported ... ready to port if one of its upstream files is an item of ... modified since ... verified. The PR for that flagged file will then blocked by another PR updating the port (and SHA) on mathlib4 side. The latter PR can be shown next to the corresponding ... modified since ... verified item.

[Winston Yin (尹維晨)]

If the mathlib3 contributor makes a paired mathlib4 PR that updates the SHA properly, we're all good. If not, SHA is not updated, but any further ports relying on the outdated mathlib4 file will have reminder attached. No pinging would be needed

[Eric Wieser]

Scott Morrison said:

• create a PR for mathlib4: it's okay if you either port the changes by hand, or create an empty PR with the intention of doing it using mathport after the mathlib3 PR is merged. However if you do this, it needs to have a special label deferred-mathlib3-pair, or something.

It is not possible to create empty PRs, is it?

[Johan Commelin]

You can create empty commits. Can't you PR them?

[Eric Wieser]

I don't remember, I guess I'll try!

[Ruben Van de Velde]

This discussion makes me wonder if we should be stricter about accepting mathlib 3 changes to ported files/files near the shore of the rising tide

[Eric Wieser]

I don't think we need to; but I think it would be good to make people aware that it is happening, by:

• Listing open mathlib3 PRs in #port-status to indicate "you might want to ping the author of this PR before starting a mathlib4 port"
• Detected open mathlib4 PRs in mathlib3 CI, to indicate "this isn't ported yet but the port is ongoing"