Updating mathlib in a PR

Stream: new members

[Sebastian Monnet]

I'm working on a PR, and I want to make use of a recent change to mathlib (the change took place after I created the PR). When I run leanproject up in the project of the PR, it doesn't seem to bring in the change I'm trying to use. Can anyone explain why this is happening and what I can do about it?

[Ruben Van de Velde]

leanproject up updates mathlib if it is a dependency of the current project, so it doesn't work in mathlib itself. git merge master is what you're after - assuming master is up to date

[Yaël Dillies]

git fetch; git merge origin/master is a safer bet.

[Riccardo Brasca]

And don't forget to run leanproject get-mathlib-cache!

[Yaël Dillies]

leanproject get-cache rather, assuming it's on a branch of the mathlib repo

[Kevin Buzzard]

Yeah but there won't be a cache

[Eric Wieser]

So you should always push after a merge so that github can start building a cache!

[Eric Wieser]

get-cache --fallback=download-first will try to pick a "close" cache

[Riccardo Brasca]

What I usually do, if I want to quickly be able to work after merging master is the following:

• git checkout master and git pull.
• leanproject get-mathlib cache, so I have master's olean.
• git checkout mybranch and git merge master.
  Now I don't have the oleans for my branch, but usually the changes are small and I can immediately work.

[Kevin Buzzard]

I usually type get-m rather than get-mathlib-cache; this works. Note that this now works even if you're working on mathlib itself (which Sebastian is, I believe), because get-m defaults to get-c if in mathlib itself (assuming your leanproject is relatively new).

[Eric Wieser]

Note that get-m doesn't support --rev or --fallback because that doesn't make sense for the intended use of get-mathlib-cache

[Eric Wieser]

@Riccardo Brasca, there's no need to do that - either get-cache --rev origin/master or get-cache --fallback=download-first will have the same effect

[Eric Wieser]

And that approach avoids you risking losing your work when you checkout, as unlike your approach it doesn't touch any of your files.

[Riccardo Brasca]

Ah, nice! Thanks

[Eric Wieser]

(I guess you still need git fetch origin; git merge master before that - but you get to skip the checkout step)