downloading build artifacts

Stream: lean4

[Paige Thomas]

If I check out code from a github Lean library repo that depends on mathlib and does not have any build artifacts in it, what do I need to do to be able to build it without rebuilding all of mathlib?

[Paige Thomas]

Is it just lake exe cache get?

[Paige Thomas]

Thank you.

[Paige Thomas]

Hmm. It seems that it still builds a bunch of stuff that looks like it is in mathlib?
messages.txt

[Paige Thomas]

Oh, it looks like this is what is being discussed in "Updating to 4.15.0".