git rebase

Stream: general

[Scott Morrison]

@Kevin Buzzard, if you're interested in a quick tutorial on git rebase, let me know. I finally worked out how to do it (with some help from Johannes) at Orsay. You might in the end find it easier than what you just went through! Screenshot-2018-09-10-23.30.11.png

[Scott Morrison]

I can see from the history of the zerology branch that you've also merged in lots of "dead" branches, which had in fact already made it into mathlib. This isn't fatal, but it does make the history look a lot more complicated, and make it much harder to judge whether everything has been merged or discarded correctly.

[Kevin Buzzard]

I tried to read up about this business recently. My understanding was that git rebase rewrites history so should not be used on public repos. I understand that we don't want horrible history in mathlib, but if a PR is accepted by mathlib then they can fix things up (e.g. by squishing the entire commit history into one commit). Are you saying I should rebase anyway? Of course anything is fine by me, I'm happy to do what I'm told here.

[Johannes Hölzl]

rebaseing branches in your private repository is okay. But it's dangerous if you rebase in leanprover-community, as others might have commits based on this branch and get into trouble if the branch gets rewritten

[Kevin Buzzard]

Aah so maybe when I notice that leanprover/mathlib has some commits, and leanprover-community/mathlib has a different number, and my clone has some new branch which is not up to date with either of these, I do all the rebasing from upstream in the comfort of my own home, and then push acceptable lies to the community mathlib. Is that how it works? Sorry to ask such basic questions, we don't get taught git in math school.

[Scott Morrison]

I realise that maybe I've been overly aggressive: I was sort of assuming that it was okay to force push branches to leanprover-community that overwrite history.

[Johan Commelin]

@Scott Morrison Do you want Linus Torvalds shouting at you? :lol: