Cloning mathematics in lean repo

Stream: general

[Greg Shuflin]

I'm trying to clone the https://github.com/leanprover-community/mathematics_in_lean repository from github, and I've been consistently running into some git errors I've never seen before:

Cloning into 'mathematics_in_lean'...
remote: Enumerating objects: 2396, done.
remote: Counting objects: 100% (110/110), done.
remote: Compressing objects: 100% (53/53), done.
error: RPC failed; curl 92 HTTP/2 stream 5 was not closed cleanly: CANCEL (err 8)
error: 335 bytes of body are still expected
fetch-pack: unexpected disconnect while reading sideband packet
fatal: early EOF
fatal: fetch-pack: invalid index-pack output

I'm not sure if this is an issue with github or this particular repo or my own network. Is anyone else running into something like this?

[Julian Berman]

Does cloning over SSH work? git clone git@github.com:leanprover-community/mathematics_in_lean.git if not, try git clone --filter=blob:none git@github.com:leanprover-community/mathematics_in_lean.git and see if that works.

[Bolton Bailey]

I am experiencing a similar error, not just with lean-related projects - git clone is doing this to me across the board. Cloning over ssh seems to work in other contexts where cloning over https does not. Is there some way to configure lake to use ssh for its cloning needs?

[Greg Shuflin]

I should say taht I've seen this http-related error with multiple lean projects cloned from github (or more accurately attempted to be cloned from github, the clone doesn't succeed). I dont' think I"ve seen it with other github projects cloned over https

[Bolton Bailey]

Greg Shuflin said:

I should say taht I've seen this http-related error with multiple lean projects cloned from github (or more accurately attempted to be cloned from github, the clone doesn't succeed). I dont' think I"ve seen it with other github projects cloned over https

Have you experienced the error when trying to clone large repositories not associated with lean? (Sorry, to be more clear, have you tried cloning any repositories larger or as large as mathlib over http or ssh and avoided the error?)

[Greg Shuflin]

Bolton Bailey said:

Greg Shuflin said:

I should say taht I've seen this http-related error with multiple lean projects cloned from github (or more accurately attempted to be cloned from github, the clone doesn't succeed). I dont' think I"ve seen it with other github projects cloned over https

Have you experienced the error when trying to clone large repositories not associated with lean? (Sorry, to be more clear, have you tried cloning any repositories larger or as large as mathlib over http or ssh and avoided the error?)

I don't think so - I actually went and tested cloning from Github some other non-Lean-related repos I work with, that were at least not trivally-sized