instructions for forward porting mathlib3 changes

Stream: mathlib4

[Kevin Buzzard]

Sorry to ask such a basic question. The tide has now caught up with work that some of my students are doing in mathlib3 and they're going to have to learn how to forward port edits to already-ported mathlib3 files. I want to point them to some wiki page or something, and I was expecting it to be the porting Wiki but I can't see any mention of the description there. On the other hand I'm well aware that people like Eric have posted coherent explanations in the past. My memory is that the first thing I'm supposed to do is to wait until mathport has expressed its opinion, which in the case I have in mind has now happened.

Are the instructions nothing more than "look carefully at the mathlib3 PR, on the files changed tab, and note which files github is flagging as having been ported; now go to the mathlib3port repo and see its opinion; copy the relevant parts over manually and make a PR, and tag it...something". Or are there gotchas I/they need to be careful about?

[Eric Wieser]

You can skip the manual "go to the mathlib3port" step by looking at the relevant page on the #port-dashboard

[Eric Wieser]

That links directly to the relevant diffs for you

[Eric Wieser]

I think there is no such document, but there should be. I posted an explanation in a private channel that I think you saw about how to _review_ forward ports, but nothing really about how to make them.

[Kevin Buzzard]

I guess I figured out how to make them, but I'm always aware that I might have missed a trick or a trap.

[Eric Wieser]

copy the relevant parts over manually and make a PR, and tag it...something

mathlib-pair. The other important step is to update the SHAs, which you can also get from #port-dashboard

[Eric Wieser]

The trap is that you have to be sure that your forward-port is the only one pending on the file

[Kevin Buzzard]

and however do I do that??

[Eric Wieser]

What's the file in question so that I can explain the dashboard page?

[Eric Wieser]

(if you remember the title of the PR you can search on https://leanprover-community.github.io/mathlib-port-status/out-of-sync)

[Kevin Buzzard]

The PR is #18148 , and the relevant files are Algebra.Category.Mon.Basic and category_theory/closed/monoidal

[Eric Wieser]

port-status#category_theory/closed/monoidal

[Eric Wieser]

The left column is what is important here; you want to check there is nothing between the (last sync) marker and the PR you were intending to forward port. If there is, then those things need to be forward-ported first

[Eric Wieser]

The middle column has links to the diffs in mathlib3port. The right column is mostly useful for working out if someone already forward-ported it and forgot to record it

[Kevin Buzzard]

I think I'm just more confused now (hopefully temporarily). The mathlib3 PR in question added two lemmas of_equiv_curry_def and of_equiv_ucurry_def. If I look at mathlib3port I can just see that those declarations have now been autoported. My plan had just been to copy-paste the two autoported declarations, change the sha and PR. What exactly are you suggesting I do instead in this particular case?

[Eric Wieser]

That's the correct thing to do

[Eric Wieser]

But it's correct only because there is only item in the left column and it's the one you care about:

image.png

[Eric Wieser]

If it looks like this:

image.png

then you're not allowed to forward-port the top item (18597) until someone else forward-ports the one below it (18558)

[Kevin Buzzard]

Is the process "one PR per changed file" or "one PR per mathlib3 PR"?

[Eric Wieser]

It doesn't really matter

[Eric Wieser]

Whatever is convenient and easy to review

[Eric Wieser]

In the example above you could make a single PR that forward-ports both 18597 and 18558, or you can make separate PRs for each. What you mustn't do is ignore 18558 (middle), and port 18597 (top) because then you'd be updating the shas past a change without actually porting it, and then it would be forgotten

[Kevin Buzzard]

Thanks, this has been super-helpful.

[Eric Wieser]

The dashboard is currently built to assume that you only port one commit at a time for each file, but it's not a hard rule. None of the tooling really cares how many files you put in a single forward-port PR, but fewer files is an easier review.