git handling of PRs

Stream: new members

[Jakob Scholbach]

Can you recommend a good (git-wise) workflow in the following situation: besides the exp_char PR #6671 (which is currently under review, and which (eventually, possibly) introduces a new file to mathlib) I am working on a separate file in which I apply the newly minted exp_char in order to define and treat the separable degree of a polynomial. I want to make that second file part of another PR. Currently I have my own "private" git repo, and copy things over to the two PR-ready copies of mathlib, but this setup gets annoying ...

So, can one handle multiple PR's in the same git repo? Thanks!

[Mario Carneiro]

Yes, this is what "dependent PRs" are for (mentioned in the PR template)

[Johan Commelin]

@Jakob Scholbach Yes, just create new branches.

[Johan Commelin]

The second branch should start from the branch of the first PR

[Yakov Pechersky]

I would suggest checking out the branch which you PR'd and then doing git checkout -b my_derivative_branch. Then make commits in that branch. If, in the PR process, you have to make edits to your PR, you checkout git checkout PR_branch, make commits, then to update your derivative branch you do git checkout my_derivative_branch; git merge PR_branch.

[Johan Commelin]

We should probably document this somewhere as a tiny tutorial "How do I git multiple dependent PRs to mathlib?"

[Yakov Pechersky]

Note, if one has a long complex chain (not a long chain complex) of branches, then merging in master as the PRs get approved can get a little hairy, if the derivative branches used some feature that is now gone/edited away. It is hairy because you have to be careful not to accidentally bring it back.

[Johan Commelin]

Yakov Pechersky said:

a long complex chain (not a long chain complex)

:rofl: :stuck_out_tongue_wink:

[Thomas Browning]

Johan Commelin said:

We should probably document this somewhere as a tiny tutorial "How do I git multiple dependent PRs to mathlib?"

I could use a tiny tutorial. I'm still using a separate mathlib folder for each PR, which is a bit painful.

[Johan Commelin]

I'll see if I can find some time to write something this week

[Julian Berman]

Thomas Browning said:

Johan Commelin said:

We should probably document this somewhere as a tiny tutorial "How do I git multiple dependent PRs to mathlib?"

I could use a tiny tutorial. I'm still using a separate mathlib folder for each PR, which is a bit painful.

There's possibly a related not-so-widely-known git trick that maybe one of you will find useful for mathlib development, which is git worktree -- it's not a thing I use often because compiling things in Python is not so useful, it's more useful in languages like JS where there's an annoying node_modules directory for you to manage -- but basically git worktree lets you have separate branches checked out at the same time into separate folders but the repo is "aware" of the other directories (so you can list them, delete them, etc.) -- https://www.youtube.com/watch?v=cRunWRC8ye0 is a good short video tutorial

[Scott Morrison]

I use git worktree all the time. I have mathlib for quick and dirty visits to branches, and then mathlib-X, mathlib-Y all set up using git worktree, and so on for branches that hold my attention for more than a day.