let's not put unrelated changes in one PR or commit

Stream: mathlib4

[Bulhwi Cha]

Two weeks ago, I moved the theorem Function.id_def from Mathlib to Std. Then a week ago, I opened #12539, which removed it from Mathlib.Logic.Function.Basic. @Kim Morrison merged std#755 three days ago, which brought the theorem into Std.

I've just found out #12539 hasn't been merged, but @Yury G. Kudryashov included the removal of the theorem in #12660 two days ago, and @Kim Morrison merged it a couple of hours ago. It seemed that the work in his PR wasn't directly related to Function.id_def.

I'm not upset or anything, but I think it's better not to put some unrelated changes into a single PR or commit.

[Eric Wieser]

I think this is a rather special case, and what actually is going on here is that Std bumps should ideally be merged in order

[Ruben Van de Velde]

Maybe something we can learn from this is that if you have a PR open to bump Std, you should insist a bit on zulip that it's merged asap

[Eric Wieser]

Neither of you tagged your PR with dependency-bump, which probably doesn't help with spotting that

[Ruben Van de Velde]

(TIL about the dependency-bump label)

[Eric Wieser]

Similarly, if you are making an Std dependency bump, you should search for open dependency PRs first, and mark yours as depending on it

[Eric Wieser]

Just to be super clear for @Bulhwi Cha's benefit: Yury had only two options here:

• Make the change in their PR
• Be aware that your PR already existed and mark it as a dependency

The path you imply of:

• Don't make this change in their PR, but keep all the other changes

would result in a CI failure, because you can't pick and choose which parts of Std to bump

[Bulhwi Cha]

Ruben Van de Velde said:

Maybe something we can learn from this is that if you have a PR open to bump Std, you should insist a bit on zulip that it's merged asap

I guess you're right. I thought Kim would've spotted #12539 when merging std#755 because GitHub let us know std#755 was mentioned in my Mathlib PR.

[Bulhwi Cha]

Ruben Van de Velde said:

(TIL about the dependency-bump label)

Me too. :sweat_smile: I've been moving stuff from Mathlib to Std several times. I'll use the tag whenever I do it again from now on.

[Bulhwi Cha]

Eric Wieser said:

Just to be super clear for Bulhwi Cha's benefit: Yury had only two options here:

• Make the change in their PR
• Be aware that your PR already existed and mark it as a dependency

The path you imply of:

• Don't make this change in their PR, but keep all the other changes

would result in a CI failure, because you can't pick and choose which parts of Std to bump

In the case where there hasn't been any open dependency bump PR, one can make it themselves and mark it as a dependency. I think that's better.

If you choose to make the change in your PR, it'd be nice to mention the change in your commit message and PR comment.

[Kim Morrison]

If you expect me to find your mathlib adaptation PRs for Std bumps, please make sure they are linked from the Std PR! I try to merge the mathlib adaptation bumps immediately after I merge the Std PRs. However if others are merging the Std PRs, ideally the author of that PR will try to get their mathlib adaptation PR merged expeditously, e.g. by posting about it on zulip (#PR reviews, or #std4, or here)

[Bulhwi Cha]

I added the following comment to my another Std PR, std#756:

Std bump PR in Mathlib: https://github.com/leanprover-community/mathlib4/pull/12540

I guess I've been too quiet. I didn't want to make duplicated notifications, but now I understand that I should mention my PRs on Zulip.

[Yury G. Kudryashov]

I'm sorry for missing your PR. I was preparing a bump PR for my std/batteries PR and fixed the build.

[Bulhwi Cha]

It's okay!

[Yury G. Kudryashov]

@Kim Morrison @Mario Carneiro What do you think about making "Mathlib adaptation PR" a requirement for a Batteries PR? In the case if Mathlib doesn't cleanly compile with this PR.

[Kim Morrison]

Prior to considering it a requirement would be setting up CI to do automatic testing, i.e. to automatically create a batteries-pr-testing-NNNN branch at Mathlib, and then reporting back to the batteries PR about the results of Mathlib CI on that branch.

(i.e. isomorphic to what we do for Lean PRs already)

We need to have the reporting before it's possible to require the successful build.

I don't think I'll have availability to set this up, however. If someone else would like to that would be great.