authenticity of github.com can't be established

Stream: general

[Michael Stoll]

When trying to set up a mathlib branch via leanproject get -b mathlib:<name>, I get the message

Cloning from git@github.com:leanprover-community/mathlib.git
The authenticity of host 'github.com (140.82.121.4)' can't be established.
ED25519 key fingerprint is SHA256:+DiY3wvvV6TuJJhbpZisF/zLDA0zPMSvHdkr4UvCOqU.
This key is not known by any other names
Are you sure you want to continue connecting (yes/no/[fingerprint])?

When I take a deep breath and say "yes", it says

Error cloning via SSH, trying HTTPS...
Cloning from https://github.com/leanprover-community/mathlib.git

and then it seems to hang.

Is this a known problem?

[Henrik Böving]

The authenticity of github can't be established error is to be expected when you connect to any SSH server for the first time, depending on your background I can go a bit into detail why it asks you for this step (its related to cryptography and networking) but in general you can mostly just enter yes all the time if you are not paranoid.

The second step menas that it tried to clone the project via SSH but you have most likely not set up and SSH key if you are asking about the first error so it fails doing that and uses HTTPS instead (this is still fine). The reason it hangs is most likely that mathlib is a huge project and takes a while to clone.

[Michael Stoll]

OK, thanks for the info.
(Until recently, I used a very old version of leanproject, which probably did not attempt to use SSH in the first place...)

[Kevin Buzzard]

Yeah, leave it a while, it might not have hung. I had this with an undergraduate at Xena last week, and we waited and waited and eventually it worked.

[Kevin Buzzard]

But just set up an ssh key for the computer you're using and then the problem goes away.

[Henrik Böving]

As for how to do that: https://docs.github.com/en/authentication/connecting-to-github-with-ssh/generating-a-new-ssh-key-and-adding-it-to-the-ssh-agent

[Eric Wieser]

Some networks are configured to block SSH traffic by default; are you on a different network to usual?

[Henrik Böving]

In that case it wouldn't have asked him for the key verification because it woul dnever have gotten access to the server pub key in the first place no?

[Michael Stoll]

After setting up an SSH key with github (following instructions), it seems to work OK now. Thanks again!

[Eric Wieser]

I'm not certain about that, I think that might happen over a different port/protocol (I helped someone at Berkeley whose git network accesses were blocked the other day, but I think we saw that message)