Zulip Chat Archive

Stream: new members

Topic: Dependent PRs

Yakov Pechersky (Dec 25 2020 at 00:27):

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 (Dec 25 2020 at 00:27):

What's the correct git flow for this?

Yakov Pechersky (Dec 25 2020 at 00:28):

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 (Dec 25 2020 at 00:29):

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 (Dec 25 2020 at 00:30):

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 (Dec 25 2020 at 00:51):

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 (Dec 25 2020 at 00:52):

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 (Dec 25 2020 at 00:53):

(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 (Dec 25 2020 at 00:55):

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

Last updated: Dec 20 2023 at 11:08 UTC