Force push

Stream: mathlib4

[Patrick Massot]

Warning: the mathlib maintainer team just force-pushed to the mathlib4 repository. Expect git turbulence, especially for PRs created after 2023-04-11T13:40:56+00:00. This very exceptional action had to be taken after a user wrote an inappropriate PR description after having received a bors delegation. PR descriptions are transferred by bors to the git history, where they are often looked at years later. They should be appropriate (or better yet, informative) to a research audience.

We apologize for the inconvenience. Of course that user won't be given bors delegation in the foreseeable future.

[David Renshaw]

I got myself (EDIT: I mean my local master branch) back into a better state by doing:

git reset --hard origin/master

[Eric Wieser]

That sounds like a way to lose all your work, you most likely want to git rebase origin/master; git push --force-with-lease if you were caught by this

[Ruben Van de Velde]

Rebasing on top of origin/master is probably more pleasant than merging, fwiw

[Eric Wieser]

It ought to be relatively painless, as the actual file history is unchanged

[Kevin Buzzard]

Help. I was working on !4#3208 and I decided it would be better off if it depended on !4#3593, so I did the usual thing: I merged 3593 into the 3208 branch port/CategoryTheory.Limits.Presheaf, and now I have incomprehensible conflicts like I've never seen before in git: whenever I resolve a merge it goes on to the next of 50 commits which have a conflict (almost always in Mathlib.lean). I suspect that this is due to the force push? I haven't got a clue how to resolve this.

[Ruben Van de Velde]

Do you have any local changes? If not, I can do the git shenanigans

[Patrick Stevens]

Just checking what you mean here: you did git checkout port/CategoryTheory.Limits.Presheaf (that is, 3208, commit f88352fa9513bc418679b03d8b689b22c09894b1), and then did git merge kbuzzard-add-ext-lemmas (that is, 3593, commit 29d0b3e7a0a1fb88282236721d4fe1cae980d56d)? That merged cleanly for me locally. What commits do you have those branches corresponding to? (git merge --abort aborts any in-progress merge and reverts to the status before merge, if you need it.)

[Kevin Buzzard]

I don't have any local changes. I did do what Patrick is suggesting, as far as I know.

[Kevin Buzzard]

Here's the mess I'm in:

$ git status
interactive rebase in progress; onto f88352fa9
Last commands done (26 commands done):
   pick 4bea27d75 feat: port CategoryTheory.Monad.Products (#3553)
   pick 1d9fdc01c feat: port AlgebraicTopology.DoldKan.PInfty (#3539)
  (see more in file .git/rebase-merge/done)
Next commands to do (27 remaining commands):
   pick 510887780 feat: port AlgebraicTopology.DoldKan.FunctorN (#3543)
   pick 9d37e7354 feat: Port CategoryTheory.Monad.Limits (#3533)
  (use "git rebase --edit-todo" to view and edit)
You are currently rebasing branch 'port/CategoryTheory.Limits.Presheaf' on 'f88352fa9'.
  (fix conflicts and then run "git rebase --continue")
  (use "git rebase --skip" to skip this patch)
  (use "git rebase --abort" to check out the original branch)

Unmerged paths:
  (use "git restore --staged <file>..." to unstage)
  (use "git add <file>..." to mark resolution)
    both added:      Mathlib/AlgebraicTopology/DoldKan/PInfty.lean

no changes added to commit (use "git add" and/or "git commit -a")
buzzard@brutus:/media/buzzard/ExternalSSD1TB/lean-projects/mathlib4$

I've since done git rebase --abort.

[Kevin Buzzard]

@Patrick Stevens oh no wait, 3208, commit f88352fa9513bc418679b03d8b689b22c09894b1 is already after the problem had occurred.

[Patrick Stevens]

Have you got anything currently checked out that you care about? I propose doing git rebase --abort, then checking that your branch is indeed port/CategoryTheory.Limits.Presheaf, and then if it is, git reset --hard origin/port/CategoryTheory.Limits.Presheaf just to bring you back into sync with what we're seeing. (That's if you don't mind getting rid of anything you haven't pushed on that branch.)

[Patrick Stevens]

I am surprised you're in the middle of a rebase - does your terminal history tell you exactly what command you ran to start yourself off into getting into this state?

[Kevin Buzzard]

I was using VS Code to fix the merge conflicts, so I have no terminal history.

[Patrick Stevens]

Yeah, it looks to me like something ran git rebase kbuzzard-add-ext-lemmas (possibly on your behalf), rather than the generally-safer-and-easier-to-reason-about git merge kbuzzard-add-ext-lemmas; the rebase in this case is very messy, but the merge is clean. I'd recommend the above procedure to just completely abort the rebase, and go with a merge instead, unless you have a specific reason to want to rebase here

[Patrick Stevens]

I don't know how much Git you know, but the rebase is basically trying to replay the linear history of your branch onto the history of your dependency, and the force-push makes that very hard because git rebase is only seeing the commits one-by-one and there are conflicts between those historical commits. git merge can do a better job because it's just comparing snapshots in time, at the cost of preserving the (messy and conflicting) history on both sides of the merge; but since we use Bors, it'll all be squashed away anyway and the mess of history won't matter.

[Kevin Buzzard]

@Ruben Van de Velde I think I've sorted the problem out. Thanks to both of you.

[Patrick Stevens]

(Consider checking your VS Code settings - I personally would check that git.rebaseWhenSync is false. Someone correct me if there's a good reason we want to rebase by default; rebasing makes commit history slightly nicer at the cost of sometimes having these awful failure modes, but I haven't seen anyone acting as though they care about having meaningful commit histories on branches in mathlib, and it's both confusing and terrifying in the cases where it goes wrong.)

[Kevin Buzzard]

We care about master, and branches are squash-merged.

[Patrick Stevens]

(sorry, by "branches" I specifically meant non-master branches, which is the only thing this affects - all glory to Bors for handling master)

[Ruben Van de Velde]

There's been some discussion about using rebases for port PRs in mathlib4 because the difference between the mathport output and the final code is actually interesting, and that's harder to get if there's merges in between

[Scott Morrison]

I'm definitely pro-messy-branch-histories, anti-rebase-horror. :-)

[Eric Wieser]

Rebase is relevant for this specific case because:

• It produces fewer conflicts than a merge if you get it right
• It prevents bors incorrectly attaching tens of authors to the commit

In cases not relevant to this force push I agree that merging is definitely the right choice for mathlib, as our branches are very often collaborative and rebases only work well when there is a single "owner" of the branch

[Reid Barton]

Rebasing is in general much kinder to reviewers.

[Reid Barton]

Even for "ordinary" PRs it's helpful if there is some logic to the commit history of the PR rather than 100 commits labeled "fix".