can't run lake update on a new project

Stream: mathlib4

[Nir Paz]

I created a new project with lake +leanprover/lean4:nightly-2024-04-24 new project math and ran lake update inside the project folder. The cmd uses basically no cpu for about 3 minutes and then exits with:

info: project: no previous manifest, creating one from scratch info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git to '.\.\.lake\packages\mathlib' error: external command 'git' exited with code 128
with only an empty mathlib folder in .lake/packages created.

This doesn't happen with other git projects, and I don't know how to get a more specific error message. Would love some help.

[Ruben Van de Velde]

Seems like that's a generic git error, so could be pretty much anything :/

[Kim Morrison]

I think this is covered under lean#4302. In the meantime, can you check that you can do a git clone of mathlib successfully?

[Nir Paz]

@Kim Morrison I just tried again and it works now (possibly because I'm on a different wifi?) Thanks anyways (:

[Nir Paz]

This is popping up again, with a more specific error message:

info: my_project2: no previous manifest, creating one from scratch

info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git to '.\.\.lake\packages\mathlib'
trace: .> git clone https://github.com/leanprover-community/mathlib4.git .\.\.lake\packages\mathlib

trace: stderr:
Cloning into '.\.\.lake\packages\mathlib'...

error: RPC failed; curl 92 HTTP/2 stream 0 was not closed cleanly: CANCEL (err 8)

error: 8116 bytes of body are still expected

fetch-pack: unexpected disconnect while reading sideband packet

fatal: early EOF

fatal: fetch-pack: invalid index-pack output

error: external command 'git' exited with code 128

I tried some fixes I found online but none worked. Regardless of whether this gets resolved, is there anywhere/any way I can download an updated packages folder (except clone all of the projects manually of course)?

[Nir Paz]

Ok this is a git issue on my end, so really I'm just asking about downloading packages, for times when this happens and I can't fix it.