Dependent PR - merge conflict

Stream: new members

[María Inés de Frutos Fernández]

Is there a way to set up dependent PRs to avoid having to solve a merge conflict once the dependence is merged? (I was half hoping that the bot would take care of this, but it didn't).
This is how I solved my merge conflict in #12939: I did git pull in the master branch, and then back in the padic_add_valuation branch I did a rebase where I resolved the conflict:

git rebase master
git add src/algebra/field_power.lean
git rebase --continue
leanproject get-cache --fallback=download-all
git push -f

and finally I committed the changes (the leanproject get-cache was just so that I could check that the code was still working).
I may be overcomplicating things; could anyone suggest a simpler git workflow to deal with this situation? Thanks!

[Yaël Dillies]

What I did with #12890 was to put only the material for the new PR, meaning that it didn't compile, but one rebase after #12888 was enough to get CI to pass.

[María Inés de Frutos Fernández]

Ah, I see. Thanks!

[Yaël Dillies]

When I want to merge master, I do git fetch; git merge origin/master and solve conflicts in VScode.

[María Inés de Frutos Fernández]

I tried git merge master without doing git fetch first and I ended up with about 200 changed files, so I undid this and tried rebase instead. If I understand correctly, you're saying that if I do git fetch first it should work?

[Yaël Dillies]

No, git fetch and origin/master just ensure that you are merging the most up to date version of master (rather than the one you have in local). What you're describing sounds like you accidentally left the merge mode.

[Yaël Dillies]

Where exactly did you see that you changed 200 files?

[María Inés de Frutos Fernández]

Oh, so you mean I should use git fetch in my branch instead of git pull in master? I don't know what you mean by leaving merge mode.
I saw the changed files in VSCode, right after trying git merge master.

[Yaël Dillies]

Ah! That's perfectly fine then. Just finish the merge, push the commit and you will see on Github that everything is as it should.

[María Inés de Frutos Fernández]

I was afraid that completing that merge with the 200 changes would introduce some mess like I did here.

[Eric Wieser]

The lazy way to do this is:

git fetch
# save and commit all your work first!
git checkout the-branch-that-was-merged-by-bors

# https://stackoverflow.com/a/46741538/102441
git merge -s ours --no-commit origin/master && git read-tree -m -u origin/master

git checkout the-branch-you-want-to-continue-with
git merge the-branch-that-was-merged-by-bors  # git should sort out the conflicts here

[Eric Wieser]

It would be nice if bors did the first two steps for you

[María Inés de Frutos Fernández]

Thanks!

[Eric Wieser]

(I didn't actually test the above, but it approximates the add-hoc approach I usually use)