!4#3155

Stream: PR reviews

[Scott Morrison]

@Violeta Hernández, I just merged your forward porting PR at !4#3155, thanks!

Two notes:

• It's really helpful if you include the link to the page on the #port-status dashboard for the relevant out-of-sync file --- this makes it much easier for reviewers. If you go to the relevant page on the dashboard, it handily provides something you can cope and paste.
• Better to use the mathlib3-pair label, rather than mathlib-port label for forward porting.

[Eric Wieser]

If you go to the relevant page on the dashboard, it handily provides something you can cope and paste.

This can be a trap and isn't always the right thing to copy paste

[Eric Wieser]

There is a github CI bot that adds a comment that links to these porting pages, which has the nice bonus of verifying that you actually edited the SHAs the way you thought you did!

[Eric Wieser]

Sometimes it doesn't work properly; merging master fixes this

[Eric Wieser]

image.png

[Eric Wieser]

Better to use the mathlib3-pair label, rather than mathlib-port label for forward porting.

Note that it won't show up on the #port-dashboard out-of-sync page unless you use the pair label

[Kevin Buzzard]

Are there instructions on how to forward port a mathlib3 PR anywhere? Sounds like the community has now put in a bunch of effort to make doing/reviewing these things easier

[Jon Eugster]

Kevin Buzzard said:

Are there instructions on how to forward port al a PR anywhere? Sounds like the community has now put in a bunch of effort to make doing/reviewing these things easier

@Eric Wieser @Scott Morrison I made a draft of writing this into the port wiki (link). Could you two have a read through and make changes as necessary, please?

[Eric Wieser]

That looks pretty good to me, thanks!