difficulties with git rebase

Stream: general

[Eric Wieser]

Scott Morrison said:

so as per usual for me the git history is a complete mess.

I'm very confused how you seem to end up with rebased copies of commits from master. What commands are you running?

[Scott Morrison]

git merge origin/master, and git push. But somehow git sometimes starts a rebase all by itself, and I muddle through. :-(

[Eric Wieser]

Git should never do that...

[Eric Wieser]

Is a magic button in vscode secretly doing a rebase? Or do you only touch git from the command line?

[Scott Morrison]

No, command line.
But I have just discovered that git config -l says pull.rebase=true.

[Scott Morrison]

That must be it. I will work out how to turn it off.

[Eric Wieser]

But you said you ran merge not pull!

[Scott Morrison]

That's true. I mean, I pull the branch itself.

[Scott Morrison]

It seems like the mystery rebase is actually triggered by the push.

[Scott Morrison]

i.e. I do git merge origin/master, fix all the conflicts, and then when I git push suddenly I'm in rebase land, and have to look at the conflicts over again.

[Scott Morrison]

This doesn't happen on other repos??

[Joscha Mennicken]

That doesn't sound like normal git behaviour.

[Eric Wieser]

Feel free to split this thread so as not to distract from your bump, Scott

[Notification Bot]

13 messages were moved here from #mathlib4 > bump to nightly-2023-08-17 by Scott Morrison.

[Joscha Mennicken]

What does your git config -l --local for the repo look like?

[Mauricio Collares]

Scott Morrison said:

This doesn't happen on other repos??

Do you have a pre-push hook in .git/hooks?

[Scott Morrison]

I have run git config pull.rebase false and git config --global pull.rebase false and will hope it goes away?

[Scott Morrison]

No hooks.

[Eric Wieser]

Can you paste your mathlib4/.git/config?

[Scott Morrison]

git config -l --local

[Scott Morrison]

.git/config

[Scott Morrison]

(The file actually lives elsewhere because mathlib4 is a submodule of my home directory repo.)

[Eric Wieser]

Here's one theory of how you end up in the previous mess:

• git checkout master
• git pull (ok, should fast-forward)
• git pull --rebase your_branch (big mistake, now you have copies of master on top of your branch
• git checkout your_branch
• git merge master (the copies are now on your branch too)

[Eric Wieser]

Really the mistake her eis running git pull your_branch when you're not already on your_branch

[Scott Morrison]

I'm pretty sure I've never done that.

[Mauricio Collares]

Scott Morrison said:

(The file actually lives elsewhere because mathlib4 is a submodule of my home directory repo.)

What does git rev-parse --git-path hooks say? I wonder if it's different because of the submodule set-up.

[Scott Morrison]

I git merge another branch, but I admit I didn't even know that git pull your_branch was a thing.

[Scott Morrison]

% git rev-parse --git-path hooks
/Users/scott/.git/modules/projects/lean/mathlib4-2/hooks

[Scott Morrison]

and everything in that directory is a *.sample.

[Joscha Mennicken]

Scott Morrison said:

(The file actually lives elsewhere because mathlib4 is a submodule of my home directory repo.)

How does that setup work? I don't think I've seen something like this before

[Scott Morrison]

I just git submodule add rather than git clone. This makes it easy to keep my pool of local checkouts synchronized between machines. Although for the past few years I've been 99% on a single machine, so it is less useful to me than it used to be.

[Damiano Testa]

Scott, I get something like what you describe when I locally undo a commit that is already on the remote branch: could this be what is triggering the rebase?

[Scott Morrison]

@Eric Wieser, would you be able to apply your fix to https://github.com/leanprover/std4/pull/190?

[Eric Wieser]

I don't have permission to push

[Scott Morrison]

git merge origin/main seems to have fixed it, in any case. :-)

[Joscha Mennicken]

Did you maybe run git pull origin/main instead of/before git merge origin/main? That could explain the pattern of rebased commits, I think.

[Eric Wieser]

To clean up the history (and therefore coauthors) of std4#190, I think you can do:

• git rebase -i --rebase-merges upstream/master
• Delete the four std4 PRs from the resulting file
• Hope the rebase succeeds (if not, git rebase --abort)
• git push --force-with-lease

[Scott Morrison]

I promise I never ever manually type git pull X. Only ever git pull. :-(

[Eric Wieser]

(edited the above: i guess it's upstream/master not origin/master for you)

[Joscha Mennicken]

Do you remember how you created commit 030d2b5053bf14063b23b6c9a69fb25d4bf19c30? It seems to come before merge commit 900c26ff71ff56b72c65495b93ee8320de1a50ef with the same commit message (.) and the tip of a weird rebase.

[Joscha Mennicken]

There is also commit 6536408b64ae3db1f5d89e5e181fd4fe3ab16269, which also came after a weird rebase and has commit message . as well. When do you usually use that commit message?

[Eric Wieser]

Delete the four std4 PRs from the resulting file

In fact, git rebase --rebase-merges -i deletes these for you!

[Scott Morrison]

Thank you all for the help diagnosing, but I think the best solution here is to assume for now that turning off pull.rebase is going to make this problem go away. If it doesn't, I'll ask for help again.

[Eric Wieser]

Can you run git rebase --rebase-merges -i $whatever_the_upstream_master_main_branch_is on the two messy PRs to fix up the co-authors?

[Scott Morrison]

Which ones are you concerned about? The latest bump, and another? If you want to do them I don't mind. :-)

[Eric Wieser]

I don't have push permissions for std4, but I guess I can do that on mathlib

[Scott Morrison]

I'd prefer not to push anything on #6019, as I want to see successful CI before I go to bed.

[Eric Wieser]

but it works better if you do it so that you don't end up with the old copy locally to merge back into the fixed one

[Eric Wieser]

Scott Morrison said:

I'd prefer not to push anything on #6019, as I want to see successful CI before I go to bed.

The following shouldn't impact that much:

• cancel CI to get a partial cache
• clean up history
• Push and resume from the previous cache

[Scott Morrison]

I ran git rebase --rebase-merges -i main for https://github.com/leanprover/std4/pull/190, but it seems to have had no effect.

[Eric Wieser]

You probably need upstream/main

[Eric Wieser]

main is likely some ancient copy of upstream/main in your fork

[Scott Morrison]

% git rebase --rebase-merges -i origin/main
Successfully rebased and updated refs/heads/simp_failIfUnchanged.
% git push
Everything up-to-date

[Eric Wieser]

origin/main is 294 commits out of date

[Eric Wieser]

Assuming its https://github.com/semorrison/std4

[Scott Morrison]

No, origin is the leanprover repository.

[Scott Morrison]

fork is my fork.

[Eric Wieser]

Works on my machine...

[Eric Wieser]

$ git --version
git version 2.41.0

[Scott Morrison]

% git --version
git version 2.32.0 (Apple Git-132)

[Eric Wieser]

That could plausibly be it

[Eric Wieser]

That is two years old

[Scott Morrison]

% git --version
git version 2.41.0
% git rebase --rebase-merges -i origin/main
Successfully rebased and updated refs/heads/simp_failIfUnchanged.
% git push
Everything up-to-date

:woman_shrugging:

[Eric Wieser]

Oh, it's because of your last merge!

[Eric Wieser]

I ran that command just before you merged master

[Eric Wieser]

Eric Wieser said:

Delete the four std4 PRs from the resulting file (the ones with #XYZ)

In fact, git rebase --rebase-merges -i deletes these for you!

So this claim was false, you have to do it manually

[Mario Carneiro]

I squash merged std4#190 and manually cleaned up the coauthors list

[Eric Wieser]

I gave up on trying to clean the history of #6019, I think we should just squash it before merging

[Scott Morrison]

I squashed it.