Question about updating mathlib4

Stream: new members

[Ching-Tsun Chou]

I have a local mathlib4 clone on my laptop (an M1 MacBook Air) which I have not touched for a while. After "git pull" to the latest master, is lake exe cache get the only thing I need to do?
I'm trying to review a Lean file in a PR. But it seems that Lean is "re-building" a lot of files, judging from messages like the following I see in VScode. What is it "re-building"? Is it possible to skip or expedite the "re-building"?

image.png

[Kevin Buzzard]

That doesn't look like a lot of files, it looks like about 25 files. But yes, lake exe cache get should be the only thing you need to do, assuming you didn't edit mathlib locally (does git report any locally changed files?). Then you should have to rebuild 0 files.

[Kevin Buzzard]

Just to be clear here, if you're reviewing a PR then you first switch to the branch and then get the cache afterwards, as you want the cache for the branch rather than for master.

[Ching-Tsun Chou]

Thanks for the explanation! It does take quite a while (maybe 15 min or so on my M1 MBA) to go through those "Built ..." messages (perhaps 600 files or so). What exactly is Lean doing during that? Not re-checking those proofs, right? I guess re-checking them will take much longer.

[Ruben Van de Velde]

That's way too long. Try lake exe cache get! first (with the exclamation mark)