Zulip Chat Archive

Stream: new members

Topic: git handling of PRs


view this post on Zulip Jakob Scholbach (Mar 17 2021 at 20:06):

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!

view this post on Zulip Mario Carneiro (Mar 17 2021 at 20:06):

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

view this post on Zulip Johan Commelin (Mar 17 2021 at 20:07):

@Jakob Scholbach Yes, just create new branches.

view this post on Zulip Johan Commelin (Mar 17 2021 at 20:07):

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

view this post on Zulip Yakov Pechersky (Mar 17 2021 at 20:08):

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.

view this post on Zulip Johan Commelin (Mar 17 2021 at 20:09):

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

view this post on Zulip Yakov Pechersky (Mar 17 2021 at 20:11):

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.

view this post on Zulip Johan Commelin (Mar 17 2021 at 20:31):

Yakov Pechersky said:

a long complex chain (not a long chain complex)

:rofl: :stuck_out_tongue_wink:

view this post on Zulip Thomas Browning (Mar 17 2021 at 20:55):

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.

view this post on Zulip Johan Commelin (Mar 17 2021 at 21:19):

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

view this post on Zulip Julian Berman (Mar 17 2021 at 21:57):

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

view this post on Zulip Scott Morrison (Mar 17 2021 at 22:31):

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.


Last updated: May 17 2021 at 21:12 UTC