password for encrypted SSH private key

Stream: new members

[Scott Morrison]

This sounds right. If you are _sure_ you've never set up an ssh key at github, do let us know, because this is an annoying obstacle in the setup.

[Dan Stanescu]

Kevin Buzzard said:

Ok so GitHub is perhaps saying "instead of providing your github password, just let me know that you are you, because you set up an ssh key at some point". I'm not an expert, this is kind of a guess.

I'm pretty sure this is exactly what happens. @Emiel Lanckriet must have set up his GitHub account to use an SSH key sometime in the past. That key is stored in his online GitHub account under Settings/SSH and GPG keys. He can connect from his machine to GitHub (to do git push for example) without further authentication, as long as he types the password to access the key on his local machine. This password is usually stored in a key ring which is many times activated by just logging into the local machine, depending on the settings, so he may have forgotten about it. Just my two cents.

Nevertheless, as opposed to other Lean-related repositories, it is very inconvenient that mathematics_in_lean asks for authentication when attempting a git clone. In my experience, this happens irrespective of whether the person who attempts to clone is set up to use Git with SSH or HTTPS. This must be a setting on the repository itself that should be changed IMO, because it is a deterrent to using the book.

[Reid Barton]

It seems like this code is responsible. I don't see how the behavior could be dependent on the repository (name).

[Reid Barton]

By the looks of it, if you don't want to push to the repository anyways, then you can just not enter a password and it should fall back to http.

[Scott Morrison]

So at the very least we should add a message that says you can just fall back (and perhaps provide the link on github explaining how to use ssh keys?)

[Yakov Pechersky]

I added the password prompt, since before, there'd be no way to properly use ssh based git if it was password protected

[Yakov Pechersky]

But I can totally understand how those that are unfamiliar with git could be confused why they are being asked for a password if they don't recall setting up an sshe keyed login

[Yakov Pechersky]

Perhaps the default should be https with a ssh optional flag

[Jeremy Avigad]

I can confirm that the ssh issue caused difficulties with some lftcm users last week, who had set up git in the past and then forgot about it. I can also confirm that we didn't do anything to configure the mathematics_in_lean repository; we just asked github to create a new repository and kept the defaults. (I also just checked the account settings and don't see anything that might help.)

[Dima Pasechnik]

Reid Barton said:

It seems like this code is responsible. I don't see how the behavior could be dependent on the repository (name).

I don't quite understand what the code there is doing. IMHO if it is about unlocking a ssh keypair it ought to work with the passphrase rather than password. Certainly, there is also a Github password (for the github account), but as far as I know this password is not used to commincate with a git server, if the comminication is going via ssh.

[Dima Pasechnik]

and there is also the password for the local user account (on the client host).

[Yakov Pechersky]

It's the passphrase that unlocks the ssh keypair, not the user account. I could have written a more specific prompt. It has nothing to do with any repository and solely has to do with the way git is setup to connect to github on the user's machine.

[Dima Pasechnik]

Yakov Pechersky said:

It's the passphrase that unlocks the ssh keypair, not the user account. I could have written a more specific prompt. It has nothing to do with any repository and solely has to do with the way git is setup to connect to github on the user's machine.

but why is it then sent to github as password, rather than passphrase?
[client.connect('github.com', username='git', password=password)]
(https://github.com/leanprover-community/mathlib-tools/blob/77c707eaead3732d0a1527478602649c7e82874e/mathlibtools/leanproject.py#L191)

[Yakov Pechersky]

Because that is the name of the kwarg in the paramiko library: http://docs.paramiko.org/en/stable/api/keys.html

[Dima Pasechnik]

Yakov Pechersky said:

Because that is the name of the kwarg in the paramiko library: http://docs.paramiko.org/en/stable/api/keys.html

Isn't it rather http://docs.paramiko.org/en/stable/api/client.html ?
Indeed, you invoke connect method of paramiko.client.SSHClient, which has both password= and passphrase= keyword args

[Dima Pasechnik]

It says

• password (str) – Used for password authentication; is also used for private key decryption if passphrase is not given.
• passphrase (str) – Used for decrypting private keys.

so it looks as if they are different beasts.

[Dima Pasechnik]

It's not 100% clear to me what "used for private key decryption" means there. Perhaps it means "treat it as passphrase" - hard to tell without either doing a test of reading the source - but in any event the prompt should ask for passphrase, not password.

[Dan Stanescu]

It can ask for either. The ssh key is encrypted with a passphrase. But that passphrase can be stored (at least on Linux machines) in the default key ring of the user, which is either unlocked when the user logs in or can be unlocked later with the local user login password.

[Dan Stanescu]

At least that's what I gather.

[Dan Stanescu]

The big question though is: why does the mathematics_in_lean repository behave differently than others. Because it really looks like it does.

[Yakov Pechersky]

And you did leanproject get mathematics_in_lean; leanproject get other_repo

[Dan Stanescu]

Exactly. And it looks like other people have the same experience of different behavior. The first asks the user to authenticate, the second doesn't for whatever other_repo.

This should, however, be checked again on a fresh clone, as things are fluctuating.

The demand for authentication is not a problem for me, but might be a problem for people not familiar with git.

[Dan Stanescu]

I just tested it now, and I wasn't prompted for a password/passphrase any more. But this may just be due to my setup.

[Reid Barton]

Whatever one you do first will add the passphrase to the ssh agent, then you won't be prompted again (for a while at least).

[Dima Pasechnik]

Dan Stanescu said:

It can ask for either. The ssh key is encrypted with a passphrase. But that passphrase can be stored (at least on Linux machines) in the default key ring of the user, which is either unlocked when the user logs in or can be unlocked later with the local user login password.

sending to github the password for the local keyring makes no sense to me - and that's what happens there, if I am not mistaken.

[Yakov Pechersky]

My ssh-passphrase is what works here, not my keyring password, in my usage so far.

[Yakov Pechersky]

Really, if the user has an SSH key that requires a passphrase, the prompt should indicate which key it is trying to use. This is what happens when I use git manually:

➜  mathlib-tools git:(master) ✗ git pull
Enter passphrase for key '/home/user/.ssh/id_rsa':
Already up to date.

However, as far as I can tell, paramiko does not expose directly what keyfile it is using to connect (https://github.com/paramiko/paramiko/blob/690d142321f53ae82f49a57b7f6716fb947d5687/paramiko/client.py#L712). I might PR that into Paramiko.

[Reid Barton]

I don't understand why any of this is necessary in the first place--doesn't leanproject invoke git pull or something?

[Kevin Buzzard]

leanproject get invokes git clone

[Patrick Stevens]

Reid Barton said:

I don't understand why any of this is necessary in the first place--doesn't leanproject invoke git pull or something?

git pull requires my SSH key anyway, because I connect to GitHub using SSH:

➜  mathlib git:(bertrand-postulate) ✗ git remote -v
origin  git@github.com:leanprover-community/mathlib (fetch)
origin  git@github.com:leanprover-community/mathlib (push)

[Reid Barton]

Right but e.g. invoking git pull from a shell script would result in the passphrase prompt if needed.

[Matt Earnshaw]

this is giving me (non-pebkac) problems too, I have made an issue at https://github.com/leanprover-community/mathlib-tools/issues/72

[Kevin Buzzard]

Thanks. This has come up a few times recently.