learning to branch

Stream: general

[Jalex Stark]

(forked from https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/freek.2Eyaml/near/197722955)

So far I've "cloned mathlib" via leanproject get mathlib and "checked out a branch" via git checkout -b <branch-name>

[Jalex Stark]

Then i edited some files and my git status looks like

On branch freek-42
Changes to be committed:
  (use "git reset HEAD <file>..." to unstage)

    new file:   freek-100/problem-42/inverse-triangle-sum.lean
    new file:   freek-100/problem-82/cubing_a_cube.lean

Changes not staged for commit:
  (use "git add/rm <file>..." to update what will be committed)
  (use "git checkout -- <file>..." to discard changes in working directory)

    deleted:    cubing_a_cube.lean

Untracked files:
  (use "git add <file>..." to include in what will be committed)

    ../.DS_Store

[Jalex Stark]

I think that means I should be writing git commit -m <commit-message>

[Patrick Stevens]

Do you want to delete the top-level cubing_a_cube.lean in this commit? If you do, you want to git rm cubing_a_cube.lean before your git commit

[Jalex Stark]

done

On branch freek-42
Changes to be committed:
  (use "git reset HEAD <file>..." to unstage)

    new file:   freek-100/problem-42/inverse-triangle-sum.lean
    renamed:    cubing_a_cube.lean -> freek-100/problem-82/cubing_a_cube.lean

Untracked files:
  (use "git add <file>..." to include in what will be committed)

    ../.DS_Store

[Patrick Stevens]

tangentially, you might want to add the line .DS_Store/ to the .gitignore file in your home directory (~/.gitignore on a Unix-like system)

[Patrick Stevens]

In that case, yep git commit -m "message" will put a commit onto your local branch with those changes on

[Patrick Stevens]

I'm going to eat now, but git push should cause that commit to show up on a new branch called freek-42 on GitHub

[Jannis Limperg]

(This book is a good intro to Git.)

[Jalex Stark]

Jannis Limperg said:

(This book is a good intro to Git.)

it's a good sign that you and bryan recommend the same book

[Patrick Stevens]

It's the canonical book, I also recommend it

[Jalex Stark]

fatal: The current branch freek-42 has no upstream branch.
To push the current branch and set the remote as upstream, use

    git push --set-upstream origin freek-42

[Jalex Stark]

is this expected?

[Patrick Stevens]

Execute that command

[Patrick Stevens]

I'll dig out the config that makes it do that command automatically and transparently

[Jalex Stark]

Patrick Stevens said:

I'll dig out the config that makes it do that command automatically and transparently

is that per user or per repo?

[Patrick Stevens]

By the way, annoying Git fact you encountered above: Git has no inherent notion of "moving" a file, under the covers it thinks a move is just a deletion and an addition; git status will try and infer that a certain deletion-and-addition is a move, but it's not built into the underlying protocol. If you use git mv instead of mv to rename a file, then you don't have to do the delete-and-add manually

[Jalex Stark]

thanks, I'm sure i learned the git mv trick and forgotten about it at least twice

[Patrick Stevens]

Jalex Stark said:

Patrick Stevens said:

I'll dig out the config that makes it do that command automatically and transparently

is that per user or per repo?

Your choice, really - I'd recommend per user. (There are three levels of Git config: per-repo, per-user, and per-computer. Any config can go in any level.) It's least confusing per-user for most config

[Patrick Stevens]

git config --global push.default current will set the config at the user level, so it applies to all repos you manipulate using your user account on your computer

[Patrick Stevens]

That means "Git: set config, for me-the-current-user on all repos I access on this machine, setting what happens when I push: assume I mean the current branch to appear on the remote with the same name as it has locally"

[Jalex Stark]

sorry, I mean per repo in the other direction

[Jalex Stark]

can you enable it by default for anyone that makes a local clone of mathlib

[Patrick Stevens]

Nope, sorry

[Patrick Stevens]

… actually probably it is possible

[Patrick Stevens]

I've never thought of that

[Jalex Stark]

we either need to enable it for mathlib or put this config command in our instructions

[Patrick Stevens]

However, I would be strongly disinclined to do it because it'll be very unexpected for people who are familiar with git

[Patrick Stevens]

Definitely putting that config command in the instructions is wise

[Jalex Stark]

we don't want to train people like me to always accept the commands the machine feeds out

[Jalex Stark]

(cf earlier in this conversation when not following such a command was key to realizing that I was not using leanproject but should be)

[Mario Carneiro]

that's the way you are supposed to do it

[Jalex Stark]

Patrick Stevens said:

However, I would be strongly disinclined to do it because it'll be very unexpected for people who are familiar with git

okay, i trust you, we'll put it in the instructions

[Mario Carneiro]

you can also write git push -u origin my_branch

[Jalex Stark]

Mario Carneiro said:

that's the way you are supposed to do it

what's the that here?

[Mario Carneiro]

but it's a personal choice how to alias this if you want to make it easier

[Mario Carneiro]

how to push a new branch to mathlib

[Mario Carneiro]

if the branch already exists you can leave off the -u

[Johan Commelin]

if it already exists upstream, is what Mario means

[Jalex Stark]

so now I expect to be able to find the branch on github?

jalex$ git push
Everything up-to-date

[Johan Commelin]

https://github.com/leanprover-community/mathlib/tree/freek-42

[Johan Commelin]

If you click on that link, it will ask you if you want to start a PR

[Mario Carneiro]

If you go to https://github.com/leanprover-community/mathlib github will helpfully tell you if you have just pushed a new branch and allow you to create a PR

[Jalex Stark]

do i want to start a PR?

[Bryan Gin-ge Chen]

Yes.

[Mario Carneiro]

If I recall the reason you created this branch correctly, I think the answer is no

[Mario Carneiro]

well, I guess you could create a [WIP] PR just so you don't lose track of it

[Jalex Stark]

okay, so you want to create a PR once you have code that's ready to be reviewed for merging?

[Mario Carneiro]

basically

[Jalex Stark]

I guess Bryan's answer is "yes" because I was supposed to make a separate PR for changing the folder structure

[Bryan Gin-ge Chen]

Oh yeah, Mario's right. I assumed that your code was ready for review.

[Mario Carneiro]

You can use either a [WIP] PR or just a branch if your only interest is in opening up a collaborative project

[Bryan Gin-ge Chen]

The archive folder isn't very active so we could probably just do the re-organization with your PR / branch.

[Jalex Stark]

is [WIP] PR a formal concept in git?

[Jalex Stark]

or is it a social construct where the title has [WIP] in it and people know to not review the code?

[Mario Carneiro]

there is a "draft PR" in github, but I mean a PR with [WIP] in the title and the WIP tag

[Bryan Gin-ge Chen]

There's a [WIP] label that we add on GitHub. The PR title should follow our requirements, e.g. "feat(archive/*): whatever"

[Patrick Stevens]

(In fact "PR" is not even a concept of Git - rather, it's a concept of GitHub, which is simply a platform that stores git repositories and puts lots of nice features on top of them)

[Mario Carneiro]

I think it's okay to have [WIP] in the title as long as it gets removed before the merge

[Jalex Stark]

an hour ago i was feeling frustrated that learning this stuff requires work, but I guess it's the same sort of work required to e.g. learn linear algebra when you're a mathematician-in-training

[Bhavik Mehta]

there's also a relatively recent option to make a Draft PR, which indicates that the code isn't ready for review

[Ryan Lahfa]

Patrick Stevens said:

(In fact "PR" is not even a concept of Git - rather, it's a concept of GitHub, which is simply a platform that stores git repositories and puts lots of nice features on top of them)

To add further, the real primitive of Git is patches and diffs, commits are just bunch of diffs (with some nice messages, extra metadata) applied in the order to give you the current view depending on whether you are in a branch, or on a specific commit, etc.

[Reid Barton]

Actually the real primitive of Git is the high-dimensional source code phase space

[Ryan Lahfa]

:'D, on a related note, some people wants to apply category theory to version control: https://pijul.org/ to replace Git

[Bhavik Mehta]

What's the connection between pijul and category theory?

[Ryan Lahfa]

Bhavik Mehta said:

What's the connection between pijul and category theory?

https://pijul.org/model/ — The second paragraph

[Bhavik Mehta]

I love it!!

[Jalex Stark]

I think I made a PR

[Jalex Stark]

I guess we have linkifiers like this? #2692

[Johan Commelin]

Jalex Stark said:

I think I made a PR

Congrats!

[Jalex Stark]

i'm currently editing files on my local machine in response to comments that several people left on the PR

[Jalex Stark]

i don't know how that code is supposed to flow back in

[Jalex Stark]

i will probably try just git commit and git push and hope that does the right thing

[Johan Commelin]

It should, yes

[Johan Commelin]

(Once you start working on a branch that other people are also working on, you'll need new tools/tricks. But don't worry about that for now.)

[Jalex Stark]

git pull
Auto-merging archive/100-theorems-list/inverse-triangle-sum.lean
CONFLICT (content): Merge conflict in archive/100-theorems-list/inverse-triangle-sum.lean
Automatic merge failed; fix conflicts and then commit the result.

[Jalex Stark]

how do I see which content is conflicting?

[Jalex Stark]

oh okay i can see it with git diff

[Jalex Stark]

what a sad error

git merge
error: Merging is not possible because you have unmerged files.
hint: Fix them up in the work tree, and then use 'git add/rm <file>'
hint: as appropriate to mark resolution and make a commit.
fatal: Exiting because of an unresolved conflict.

[Jalex Stark]

i manually implemented something similar to the tactic repeat {git pull <|> git push <|> git merge <|> git add * <|> git commit} and it eventually pushed

[Bryan Gin-ge Chen]

I made a suggestion on your PR with more info.

[Jalex Stark]

Thanks! Eventually VSCode gave me little buttons to help me decide whether to take the local, remote, or both changes.

[Johan Commelin]

Jalex Stark said:

i manually implemented something similar to the tactic repeat {git pull <|> git push <|> git merge <|> git add * <|> git commit} and it eventually pushed

That's good. I think it's supposed to be manual.

[Johan Commelin]

Bots still aren't smart enough. So we need brains at some point in the process (-;

[Jalex Stark]

sure, I was emphasizing the fact that I didn't have any clue which one was going to make progress

[Jalex Stark]

that I was acting in a way that is about as dumb as that tactic

[Jalex Stark]

I think I resolved all comments that implied code changes

[Patrick Stevens]

Ryan Lahfa said:

Patrick Stevens said:

(In fact "PR" is not even a concept of Git - rather, it's a concept of GitHub, which is simply a platform that stores git repositories and puts lots of nice features on top of them)

To add further, the real primitive of Git is patches and diffs, commits are just bunch of diffs (with some nice messages, extra metadata) applied in the order to give you the current view depending on whether you are in a branch, or on a specific commit, etc.

This isn't actually true; a commit is a complete snapshot of a mapping of filename to file contents. Diffs are not a primitive of Git; it infers them where necessary, and it sometimes uses them as a perf optimisation, but they are not fundamental either. Pijul and Darcs are based on patches; git is not.

[Patrick Stevens]

And that's why it doesn't do renames

[Ryan Lahfa]

Patrick Stevens said:

Ryan Lahfa said:

Patrick Stevens said:

(In fact "PR" is not even a concept of Git - rather, it's a concept of GitHub, which is simply a platform that stores git repositories and puts lots of nice features on top of them)

To add further, the real primitive of Git is patches and diffs, commits are just bunch of diffs (with some nice messages, extra metadata) applied in the order to give you the current view depending on whether you are in a branch, or on a specific commit, etc.

This isn't actually true; a commit is a complete snapshot of a mapping of filename to file contents. Diffs are not a primitive of Git; it infers them where necessary, and it sometimes uses them as a perf optimisation, but they are not fundamental either. Pijul and Darcs are based on patches; git is not.

I stand corrected, thank you

[Jalex Stark]

ugh I made a mess of making a new PR
https://github.com/leanprover-community/mathlib/pull/2772/files

[Jalex Stark]

i ran git status and it showed just one file with a change

[Jalex Stark]

and then I ran git push and it had junk from my other branches in it

[Bryan Gin-ge Chen]

git status shows the differences since the last commit. So I suspect your branches all share the same set of commits. git log will show you the recent commits on your current branch.

[Bryan Gin-ge Chen]

You might be able to remove commits using git rebase -i. I'd read the section of the git book on rebasing before attempting it though.

[Ryan Lahfa]

You can read also about git stash

[Ryan Lahfa]

It can just store in a stash some changes you don't want right now, you do your stuff, you commit, push, then switch to another branch and apply the stash

[Scott Morrison]

(I'd advise against learning git rebase until you're comfortable with the basics. It's a bit of a tar pit, and often #xy applies, in any case.)

[Scott Morrison]

I find a simple way to "recover" from bad branches is to use git merge --squash.

[Scott Morrison]

Say I have a branch bad, which has the changes I care about, but also some other garbage in other files, that I've accidentally committed, and I can't or don't want to understand the history well enough to cherry pick or rebase.

[Scott Morrison]

I then:

1. git checkout master
2. git checkout -b good (this creates a brand new branch, whose content matches master
3. git merge --squash bad (this dumps all the changes made in the bad branch into my current working copy, but without committing anything)
4. git checkout -- X.lean (to abandon the changes made to a file X.lean, which I realise I don't want, repeat as necessary)
5. git commit -m "feat(algebra/awesome): wow"

[Jalex Stark]

That was helpful, scott! I think i know what i did wrong now
branches are organized in a tree, and git checkout -b new-branch makes a child of whatever branch i'm currently in

[Jalex Stark]

so i thought I made a bunch of parallel branches that were children of master, but in fact I made a line graph of branches

[Jalex Stark]

probably after reading enough of the book i will know how to get git to tell me which branch I am in and which branches are upstream of it

[Scott Morrison]

I don't use it much anymore, but I used to use a GUI often. Sourcetree was the one I used, but there are many others.

[Scott Morrison]

Something that I learnt way too late was to use git worktree. With git worktree you just keep a separate directory for each branch you're interested in at the moment, so much less often do you actually change branches in a given directory.

[Scott Morrison]

Saves on rebuilding oleans, and saves on confusion about which branch you're currently on, and why.

[Jannis Limperg]

Jalex Stark said:

probably after reading enough of the book i will know how to get git to tell me which branch I am in and which branches are upstream of it

git status tells you what branch you're on. git log gives you a list of commits on the current branch. In that list, look for a commit with annotation (master); this is the last commit ('head') of the master branch.

[Bhavik Mehta]

You can also get git to draw you the tree of branches, a quick way is git log --graph --oneline and there's more sophisticated and pretty versions here https://stackoverflow.com/questions/1064361/unable-to-show-a-git-tree-in-terminal

[Jalex Stark]

git log doesn't seem particularly useful in my current state, it's giving me information about everything pushed to mathlib in the past two days
(even though git status says I'm on some local branch)

[Bryan Gin-ge Chen]

You probably haven't committed any changes to that branch then.

[Jalex Stark]

yes, that's true
(I'm worried that this game of "infer what state Jalex's git is in" is not a particularly efficient use of anyone's time; I think we expect me to go off and read and then come back with well-formed questions)

[Bhavik Mehta]

#mwe? :stuck_out_tongue:

[Jalex Stark]

:) I guess one can literally give an example by like making a branch public or something

[Jalex Stark]

it seems insane to me that there wasn't a class about this stuff in my undergrad program, if apparently it's used by anyone that does software development

[Jannis Limperg]

Jalex Stark said:

git log doesn't seem particularly useful in my current state, it's giving me information about everything pushed to mathlib in the past two days
(even though git status says I'm on some local branch)

That's because your local branch contains all these commits. A branch is a list of commits (not really but close enough). When you create a new branch, it initially contains all the commits from the current branch. When you commit changes, you add a commit on top of the current branch. When you create a PR, you're saying, roughly, 'take any commits from my branch which aren't already on master and add them'.

Git's UI is legendarily bad, so there really should be classes about it.

[Patrick Stevens]

I can't speak precisely to the quality of the course because I haven't undergone it, but a friend who I trust technically made https://www.gitscientist.com as a training course aimed at scientists

[Patrick Stevens]

Dunno how much they charge for it

[Ryan Lahfa]

Patrick Stevens said:

Dunno how much they charge for it

No explicit pricing is the worst kind of pricing, I was super interested and know people who would benefit a lot of this but :/

[Patrick Stevens]

I've asked my friend already

[Yury G. Kudryashov]

A branch is a list of commits

No, a branch is a marked commit. Git stores history in a directed graph of states ("commits") with no cycles. While many commits have one parent (the previous commit in the same branch), there are "merge" commits with two or more parents (git merge / git pull). When you run git log, it starts at your current commit (HEAD) and goes backwards in history.

[Yury G. Kudryashov]

So it shows you all ancestors of your current commit.

[Yury G. Kudryashov]

The master branch of mathlib has a linear history because we “squash” branches before merging them back to master.

[Yury G. Kudryashov]

So probably you'll see a few of your commits to the new branch, then the whole history of master.