Zulip Chat Archive

Stream: Is there code for X?

Topic: use mathlib branch in project


view this post on Zulip Alena Gusakov (Aug 05 2020 at 00:36):

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)?

view this post on Zulip Jalex Stark (Aug 05 2020 at 00:48):

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

view this post on Zulip Jalex Stark (Aug 05 2020 at 00:49):

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

view this post on Zulip Jalex Stark (Aug 05 2020 at 00:51):

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

view this post on Zulip Alena Gusakov (Aug 05 2020 at 00:55):

Great, thank you!


Last updated: May 16 2021 at 05:21 UTC