adele refactor (github issue)

Stream: FLT

[Kevin Buzzard]

OK so I made some progress on the adele refactor in FLT but now I'm facing the issue that stuff is being PRed from FLT to mathlib and changes to mathlib are breaking FLT, so I would like to have FLT main and the mathlib branch kbuzzard-finite-adele-ring-refactor both depending on the same commit of mathlib master, which may as well be tag v4.19.0-rc2 because this is what FLT main is on, and the mathlib branch kbuzzard-finite-adele-ring-refactor is behind this. In mathlib I tried

git checkout kbuzzard-finite-adele-ring-refactor
git rebase v4.19.0-rc2

and things looked good:

Successfully rebased and updated refs/heads/kbuzzard-finite-adele-ring-refactor.

But then if I try

git push

I get

error: failed to push some refs to 'github.com:leanprover-community/mathlib4.git'
hint: Updates were rejected because the tip of your current branch is behind
hint: its remote counterpart. If you want to integrate the remote changes,
hint: use 'git pull' before pushing again.
hint: See the 'Note about fast-forwards' in 'git push --help' for details.

I'm confused about how after a merge the tip of my current branch can be behind its remote counterpart. If I try git pull I get another error:

hint: You have divergent branches and need to specify how to reconcile them.
hint: You can do so by running one of the following commands sometime before
hint: your next pull:
hint:
hint:   git config pull.rebase false  # merge
hint:   git config pull.rebase true   # rebase
hint:   git config pull.ff only       # fast-forward only
hint:
hint: You can replace "git config" with "git config --global" to set a default
hint: preference for all repositories. You can also pass --rebase, --no-rebase,
hint: or --ff-only on the command line to override the configured default per
hint: invocation.
fatal: Need to specify how to reconcile divergent branches.

I am confused now because I thought I already rebased. Is the idea that I need to rebase both kbuzzard-finite-adele-ring-refactor and origin/kbuzzard-finite-adele-ring-refactor separately??

[Ruben Van de Velde]

Okay, so what you did wasn't a merge but a rebase

[Ruben Van de Velde]

That means you took the commits on your branch and replayed them on top of ´v4.19.0-rc2`, but now there's no longer a connection between the new commits and the old ones, as far as git is concerned

[Ruben Van de Velde]

Short answer if it's fine to use git push -f origin kbuzzard-finite-adele-ring-refactor

[Julian Berman]

It's slightly better to internalize using git push --force-with-lease instead at this point (the help has details on what the difference is, but basically it is designed for exactly this case of "I rebased or added some stuff on top, but the thing in GitHub should exactly match what I'm pushing" -- but if that weren't the case and someone had been collaborating with you and put other commits on top of your branch unknowingly, it will not wipe out their wok.)