Zulip Chat Archive

Stream: new members

Topic: Updating a mathlib branch


Thomas Browning (Jul 01 2022 at 19:54):

I'm running the Berkeley lean seminar again, and I'm wondering what is the best way to update a mathlib branch (potentially with collaborators)? I always do the following. But presumably there's a better way that makes more use of leanproject?

git pull
git checkout master
git pull
leanproject get-cache
git checkout [branch]
git merge master
git push

Kevin Buzzard (Jul 01 2022 at 19:55):

FWIW that's pretty much exactly what I would do, but on the other hand I'm equally confident that there will be a fancier way which I would find harder to remember.

Kyle Miller (Jul 01 2022 at 20:06):

I usually do something like this to merge master and get its cache:

git pull origin master
leanproject get-cache --rev=origin/master

Kyle Miller (Jul 01 2022 at 20:10):

If you're also wanting to pull from your project, merge master, and push it back to the central repository, you could do

git pull
git merge origin/master
leanproject get-cache --rev=origin/master
git push

(These are relying on git pull internally doing git fetch, which updates your repository's idea of what origin/master is.)

Thomas Browning (Jul 01 2022 at 22:23):

Thanks!

Eric Wieser (Jul 01 2022 at 22:44):

Another option is leanproject get-cache --fallback=download-first, which guesses the right --rev argument for you

Eric Wieser (Jul 01 2022 at 22:45):

(for instance if you did a merge yesterday and master has moved since)


Last updated: Dec 20 2023 at 11:08 UTC