use mathlib branch in project

Stream: Is there code for X?

[Alena Gusakov]

Hi, sorry if this has been asked before, I searched it and nothing came up. Is it possible to use a branch in mathlib to work on code? I'm interested in the graph theory PRs that have been happening (I wanted to join in but I overcommit to projects, but I do want to try to help if/when I can)?

[Jalex Stark]

i'm not sure i understand your question, but I think the answer is yes

[Jalex Stark]

you can do e.g.
leanproject get mathlib:graphs_and_bigraphs, and that will make a new local copy of mathlib and checkout the graphs_and_bigraphs branch, which is the branch associated to #3458

[Jalex Stark]

if you push to that branch, those commits will show up on the PR. If instead you want to explore in a different direction, you could do e.g. git checkout -b graphs_agusakov. that will make a new branch starting at the same commit as the old one

[Alena Gusakov]

Great, thank you!