what exactly does `leanproject upgrade-mathlib` do?

Stream: new members

[Chris M]

I've been getting a better understanding of git lately after being asked to do a pull request for mathlib.
Is it correct to say that leanproject upgrade-mathlib (i.e. leanproject up) simply executes a git pull origin to fetch the current remote master branch of mathlib to your local repository and merge it with your master branch?

[Carl Friedrich Bolz-Tereick]

I am not completely sure, I am a complete newbie as well, but I think leanproject up also changes leanpkg.toml to point to the newest mathlib revision

[Carl Friedrich Bolz-Tereick]

(and it also gets oleans for the revision you pulled)

[Kevin Buzzard]

The parenthetical remark is the key difference between leanproject and git.

[Scott Morrison]

If you're working on a non-mathlib repository, then the correct way to update the repository is

git pull
leanproject get-mathlib-cache

You should really only be using leanproject upgrade-mathlib if you have commit access on that repository, and actually want to bump the mathlib version the repository is using.

[Scott Morrison]

If you're working in mathlib directly (which I would actually strongly encourage --- it's so much more likely your work will survive --- i.e. end up in mathlib rather than bit-rotting --- if you never open another repository!)

[Scott Morrison]

then leanproject up is all you need.