Zulip Chat Archive

Stream: mathlib4

Topic: merging


Scott Morrison (Dec 14 2022 at 10:24):

@Patrick Massot, when I've been merging mathlib4 porting PRs, I've been editing the #port-status wiki to change Yes to No at the same time. I noticed you didn't do this on https://github.com/leanprover-community/mathlib4/pull/996, so this is the friendly reminder that it is helpful to do so. :-)

Hopefully soon this step won't be needed, in any case.

Patrick Massot (Dec 14 2022 at 11:44):

Should I do that as soon as I tell bors to merge? I was waiting for the actual merge (but then I went to do something else of course)

Chris Hughes (Dec 14 2022 at 11:55):

I haven't been doing that either. What do I have to do?

Johan Commelin (Dec 14 2022 at 12:01):

Update https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status from No to Yes

Johan Commelin (Dec 14 2022 at 12:01):

Hopefully this won't be needed anymore in 2 or 3 days.

Scott Morrison (Dec 14 2022 at 12:26):

I've been doing it as soon as I hit merge. I found that I have fewer accidents where I forget to follow up that way.

Chris Hughes (Dec 14 2022 at 23:20):

I haven't been doing that. Do I need to go back and do this to all the PRs I've merged?

Scott Morrison (Dec 14 2022 at 23:46):

Probably? I've caught some, but mostly only when they appear on the high priority graphs.

Scott Morrison (Dec 14 2022 at 23:47):

If we look at the output of scripts/port_status.py, and look for PR numbers that have already been closed, that should identify any that have slipped through like this.


Last updated: Dec 20 2023 at 11:08 UTC