Updating a mathlib branch

Stream: new members

[Thomas Browning]

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]

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]

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]

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]

Thanks!

[Eric Wieser]

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

[Eric Wieser]

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