Dependent PRs

Stream: new members

[Yakov Pechersky]

A question re dependent PRs -- if I write lemmas in a PR 3 that depend on other PRs I have (1 and 2), do I place the changes for 1 and 2 in the PR commits for 3 as well? If I don't, do I just propose the incremental change of 3?

[Yakov Pechersky]

What's the correct git flow for this?

[Yakov Pechersky]

Once PRs 1 and 2 are merged, do I rebase on new master in the branch for PR 3, or merge, or cherry pick in? Or just recommit on master and force-push?

[Yakov Pechersky]

Doing a rebase seems to create a PR that has _all_ of the commits to master that happened in the interim. I understand that PR commits are squashed, but it still looks weird within the PR history.

[Thomas Browning]

Usually I just have 3 contain the changes of both 1 and 2, and then fix merge problems as they arise. But I'm no git guru, and this probably isn't the best way to do it.

[Julian Berman]

I don't know if mathlib has its own norms here, but normally yeah if you can't tear 3 independently away from 1 and 2 (which is preferable so that they can get merged independently) then you'd have the PR for 3 be on top of commits for 1 and 2.

[Julian Berman]

If mathlib squashes commits on merge that complicates things -- if it does that for all PRs there isn't much point in rebasing yours, you can equally well just merge master into your branch, and then that will all get squashed again once it merges back to master

[Julian Berman]

(The advantage over rebasing is that you may in some cases have to fix some merge conflicts multiple times, or in places that wouldn't be a conflict if you merged only the 2 HEADs, but if you like doing that you can enable git rerere and it sometimes helps)

[Julian Berman]

git rerere docs are here in case you elect for that: https://www.git-scm.com/book/en/v2/Git-Tools-Rerere