install problems

Open FrederickPu opened this issue 10 months ago • 1 comments

when i run lake exe get cache i get the following error message:

info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git to '.\.\.lake/packages\mathlib'
info: batteries: cloning https://github.com/leanprover-community/batteries to '.\.\.lake/packages\batteries'
info: Qq: cloning https://github.com/leanprover-community/quote4 to '.\.\.lake/packages\Qq'
error: external command 'git' exited with code 128

Feb 11 '25 05:02 FrederickPu

I think this happens when you try to lake exe cache get before the Lean server starts.

What I had before I tried to start the server:

$ lake exe cache get info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git error: external command 'git' exited with code 128

What I had after:

$ lake exe cache get Attempting to download 6014 file(s) Downloaded: 6014 file(s) [attempted 6014/6014 = 100%] (100% success) Decompressing 6014 file(s) Unpacked in 4351 ms Completed successfully!

Jul 10 '25 12:07 lakesare