broken lake with new computer

Stream: lean4

[Etienne Marion]

Hello! I changed my computer and I have to reinstall stuff. Lean is working fine in VSCode but when I ran lake exe cache get, I got:

Attempting to download 5026 file(s)
Downloaded: 5026 file(s) [attempted 5026/5026 = 100%] (100% success)
Decompressing 5026 file(s)
could not execute external process '/Users/etienne/.cache/mathlib/leantar-0.1.13'
uncaught exception: resource vanished (error code: 32, broken pipe)

I suppose I'm missing something uninstalled, any ideas? (I'm on a mac with apple silicon)

[Etienne Marion]

I solved it by deleting /Users/etienne/.cache/mathlib and running lake exe cache get!.

[Shreyas Srinivas]

Did you migrate from an intel mac?

[Etienne Marion]

Yes