travis / good git practice

Stream: general

[Kevin Buzzard]

I am trying to use all this git/github/community mathlib infrastructure maturely now.

I am in the middle of writing the proof of Hilbert basis, in a branch in my local clone of community mathlib. I've not got very far because I was distracted by (a) not having interface for coefficients of polynomials and (b) the zero ring being a constant special case. In both cases I created new branches (from master, not from my Hilbert basis branch) with small edits to files, and PR'ed directly to mathlib. My Hilbert basis branch is now pushed to community mathlib as a WIP. It depends on both these branches above -- is that a problem? I'm assuming that the system is sufficiently mature to make it not so (I am hoping I can rebase from master if and when these easy PR's are accepted).

I also got involved in a different project -- adding matrices over a general ring -- and made yet another branch for these. I PR'ed this to mathlib too and then Sean almost completely rewrote it (which is great, this is exactly what community mathlib is for) and I see that the PR automatically gets updated. I am hoping that I've just about got these things right now. Scott pointed out that using git merge can cause chaos with history (as indeed it did with a previous zerology branch I'd created, which I've now deleted) and hopefully I've managed to use rebase correctly to make history look reasonable in all these cases. I occasionally update mathlib from upstream and rebase. If anyone has any comments on anything I'm still doing wrong with this set-up I'd be happy to hear them.

As for travis -- apparently it has failed on the matrix PR :-( I can't see why. Is the fault of travis? There were github problems yesterday apparently.

It's this one: https://github.com/leanprover/mathlib/pull/334

[Sean Leather]

It looks like the error is due to a timeout: https://travis-ci.org/leanprover/mathlib/jobs/427142459 . This happens occasionally on Travis-CI.

[Sean Leather]

My Travis-CI build passed for that same branch: https://travis-ci.org/spl/mathlib/builds/427091112

[Reid Barton]

Once the zerology and coefficients PRs have landed in master, you should rebase the Hilbert basis branch on top of master and then PR it (when ready).

[Reid Barton]

The zerology and coefficients patches also exist on your kmb_hilbert_basis branch and you probably shouldn't try to rebase them onto master when the time comes, because it's likely that small changes will have been made to them before merging. I can tell you about how to do that now or later (short version: use git rebase --onto)

[Reid Barton]

Or I guess you can also use git rebase -i and then just delete the lines for all the patches you don't want

[Kevin Buzzard]

Hmm. Once the PR's land in master, are the traditional edits done in mathlib master? If so I can't merge my local branches with upstream changes -- the community branches never see them. But really what I think I want to happen with the kmb_hilbert_basis branch is that I just squash everything down to one commit after I'm finished. I guess I only committed a partially-written proof to back it up in case my laptop dies.

[Reid Barton]

I assume somebody is pulling leanprover/mathlib master into leanprover-community/mathlib master every now and then? At least, I see they are equal right now

[Reid Barton]

Actually it doesn't really matter--I don't know how you have your checkouts set up but you can have both leanprover/mathlib and leanprover-community/mathlib as remotes in the same local mathlib repository. Then you (or anyone) can rebase your kmb_hilbert_basis branch on top of leanprover/mathlib's master

[Scott Morrison]

Yes, I've been pulling leanprover to leanprover-community whenever I notice it out of sync.

[Kenny Lau]

which one is safer, merge or rebase?

[Kenny Lau]

(whatever "safe" means)

[Reid Barton]

I guess merge is kind of "safer"? It retains more information about the history of commits. Usually that's information you don't actually want though.

[Keeley Hoek]

rebase rewrites history
merge just makes yet another (maybe slightly fancy) commit
People argue about what best practice is, and some people zealously say you shouldn't ever rebase anything
A consequence of rewriting history though is that other people who used to have the same history as you can't cleanly just merge their work back together with yours

[Keeley Hoek]

You can never just delete your own work by merging something, but with rebase you can easily drop commits which you might have to go back and find using git reflog...

[Mario Carneiro]

Keep in mind that lean and mathlib both use a rebase workflow. It doesn't necessarily affect what you do as a third party, but mathlib has a linear commit history as a result. I think this is better organizationally than the big tangle it would be otherwise

[Mario Carneiro]

I don't think rebase will cause you to lose work, unless you mess up the merge

[Mario Carneiro]

also if your branch is based on some commits which have since been rebased (so you are sitting on a separate version of the same commits) then if you rebase your branch on the master these commits will disappear

[Keeley Hoek]

If you git rebase -i HEAD~10 and then accidentally drop a line from the resulting file, then the commit will be dangling and you will have to find it

[Mario Carneiro]

oh yes, interactive rebase is basically just editing history, and you can do whatever

[Mario Carneiro]

I meant just plain git rebase

[Mario Carneiro]

which should have roughly the same merge behavior as git merge except that the final commits are arranged linearly