Zulip Chat Archive

Stream: new members

Topic: Updating mathlib in a PR


Sebastian Monnet (Feb 19 2022 at 11:10):

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 (Feb 19 2022 at 11:37):

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 (Feb 19 2022 at 11:40):

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

Riccardo Brasca (Feb 19 2022 at 11:48):

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

Yaël Dillies (Feb 19 2022 at 11:50):

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

Kevin Buzzard (Feb 19 2022 at 12:01):

Yeah but there won't be a cache

Eric Wieser (Feb 19 2022 at 12:07):

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

Eric Wieser (Feb 19 2022 at 12:07):

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

Riccardo Brasca (Feb 19 2022 at 12:14):

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 (Feb 19 2022 at 12:23):

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 (Feb 19 2022 at 12:45):

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 (Feb 19 2022 at 12:46):

@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 (Feb 19 2022 at 12:47):

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 (Feb 19 2022 at 12:47):

Ah, nice! Thanks

Eric Wieser (Feb 19 2022 at 12:48):

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


Last updated: Dec 20 2023 at 11:08 UTC