Developing on mathlib itself

Stream: new members

[Yakov Pechersky]

Let's say I'm trying to develop a new lemma for mathlib itself (thanks @Bryan Gin-ge Chen for the invite). Do I use leanproject get-mathlib-cache after every git pull, when trying to stay up-to-date with top-of-tree?

[Kevin Buzzard]

I just do leanproject up once, make a new branch, and then don't update mathlib any more when developing.

[Kevin Buzzard]

I would never do git pull because that would put me in a situation where I had an uncompiled mathlib, and I don't have 2 hours to spare

[Bryan Gin-ge Chen]

A common task is git fetch && git merge origin/master to update your branch, fix merge conflicts locally, and then git push to let Github actions build mathlib for you. After an hour or so, leanproject up should be able to fetch working oleans.