equivalent of `leanprojet get-cache`

Stream: mathlib4

[Antoine Chambert-Loir]

What is the equivalent for Lean 4 of the useful leanproject get-cache?
I just did lake exe cache get after switching to a branch, but this did not prevent Lean to start recompiling the whole mathlib…

[Ruben Van de Velde]

That's the right command, but maybe you ran it while Vs code was active?

[Ruben Van de Velde]

(I assume your mean a branch of mathlib)

[Antoine Chambert-Loir]

Right. (and right)
So that means I have to quit VSCode when I want to switch between mathlib4 branches?

[Ruben Van de Velde]

The issue is that you can't have lean processes running at the same time, because they interfere with the cache

[Antoine Chambert-Loir]

I don't understand what happens : I did that, and when I launched VSCode, it started recompiling everything…

[Antoine Chambert-Loir]

Maybe I should pay attention to this error message:

Attempting to download 3142 file(s)
Downloaded: 0 file(s) [attempted 3142/3142 = 100%] (0% success)
No cache files to decompress

[Jireh Loreaux]

Even closing vs code isn't enough. You need to kill all the Lean processes manually if you get it accidentally compiling everything. It's a pain.

[Yury G. Kudryashov]

I run killall lean; sleep 1; killall lean; lake exe cache get

[Scott Morrison]

I mean, when it says "No cache files to decompress", I don't think the problem is stray processes. Usually if there are no oleans available in the cache at all, that means you've edited your lakefile.lean, or your lean-toolchain, or (please don't do this unless you know what you're doing) used elan override.

[Mauricio Collares]

Or ran lake update (it's a footgun)

[Antoine Chambert-Loir]

On the doc, there is something suggesting to type curl ... -o lean-toolchain if the rest does not work, and I did that, and it changed the version of Lean4 which was then incompatible with that of the branch, etc.

[Sebastian Ullrich]

That is in the instructions on how to use mathlib4 as a dependency

[Sebastian Ullrich]

@Scott Morrison We really need to move that; it's not just about update