Zulip Chat Archive
Stream: general
Topic: leanproject get mathlib, https vs ssh
Yakov Pechersky (Jun 28 2020 at 07:39):
Is there a reason why leanproject get mathlib defaults to https instead of ssh, for the git repo remote url? I was having issues pushing, which were resolved once I switched the origin url to use ssh. Maybe there should be a --ssh flag to pull in the repo with the ssh url.
Patrick Massot (Jun 28 2020 at 07:45):
It doesn't.
Patrick Massot (Jun 28 2020 at 07:46):
If leanproject used https it's because it failed when trying to use ssh, either because your python install is broken or your ssh setup is broken or there is a bug in leanproject.
Yakov Pechersky (Jun 28 2020 at 08:00):
I tried using --debug to show the codepath, but didn't see anything regarding ssh:
➜ python3 --version
Python 3.6.9
➜ pip3 --version
pip 9.0.1 from /usr/lib/python3/dist-packages (python 3.6)
➜ leanproject --debug get mathlib
Cloning from https://github.com/leanprover-community/mathlib.git
configuring mathlib 0.1
Looking for local mathlib oleans
Found local mathlib oleans
➜ cd mathlib
➜ git log | head
commit a220286ac49a16bee74e85d9d2b308ce0d30d858
Author: Floris van Doorn <fpvdoorn@gmail.com>
Date: Sun Jun 28 06:01:24 2020 +0000
feat(subtype): standardize (#3204)
Add simp lemma from x.val to coe x
Use correct ext/ext_iff naming scheme
Use coe in more places in the library
Yakov Pechersky (Jun 28 2020 at 08:01):
git remote show origin | grep mathlib
Fetch URL: https://github.com/leanprover-community/mathlib.git
Push URL: https://github.com/leanprover-community/mathlib.git
mathlib-cache tracked
Patrick Massot (Jun 28 2020 at 08:03):
--debug will only help when leanproject crashes.
Patrick Massot (Jun 28 2020 at 08:03):
What does leanproject --version says?
Yakov Pechersky (Jun 28 2020 at 08:04):
leanproject --version
leanproject, version 0.0.8
Patrick Massot (Jun 28 2020 at 08:04):
Also try lauching python and import paramiko
Patrick Massot (Jun 28 2020 at 08:05):
and from paramiko.ssh_exception import AuthenticationException, SSHException
Yakov Pechersky (Jun 28 2020 at 08:05):
➜ mathlib git:(master) python -c 'import paramiko'
Traceback (most recent call last):
File "<string>", line 1, in <module>
ImportError: No module named paramiko
➜ mathlib git:(master) python3 -c 'import paramiko'
Yakov Pechersky (Jun 28 2020 at 08:05):
so it works for python3, not python
Patrick Massot (Jun 28 2020 at 08:06):
This is 2020, when people say python you need to understand python3.
Yakov Pechersky (Jun 28 2020 at 08:07):
This is on a mostly clean new install of 18.04
Patrick Massot (Jun 28 2020 at 08:08):
You should upgrade to 20.04 to get rid of python2.
Patrick Massot (Jun 28 2020 at 08:08):
Anyway, please open ipython, type the two import lines I wrote, and then try typing https://github.com/leanprover-community/mathlib-tools/blob/master/mathlibtools/leanproject.py#L167-L170
Yakov Pechersky (Jun 28 2020 at 08:14):
In [7]: client.connect('github.com', username='git')
---------------------------------------------------------------------------
PasswordRequiredException Traceback (most recent call last)
<ipython-input-7-f64e6b4b50fa> in <module>()
----> 1 client.connect('github.com', username='git')
/usr/local/lib/python3.6/dist-packages/paramiko/client.py in connect(self, hostname, port, username, password, pkey, key_filename, timeout, allow_agent, look_for_keys, compress, sock, gss_auth, gss_kex, gss_deleg_creds, gss_host, banner_timeout, auth_timeout, gss_trust_dns, passphrase, disabled_algorithms)
444 gss_deleg_creds,
445 t.gss_host,
--> 446 passphrase,
447 )
448
/usr/local/lib/python3.6/dist-packages/paramiko/client.py in _auth(self, username, password, pkey, key_filenames, allow_agent, look_for_keys, gss_auth, gss_kex, gss_deleg_creds, gss_host, passphrase)
762 # if we got an auth-failed exception earlier, re-raise it
763 if saved_exception is not None:
--> 764 raise saved_exception
765 raise SSHException("No authentication methods available")
766
/usr/local/lib/python3.6/dist-packages/paramiko/client.py in _auth(self, username, password, pkey, key_filenames, allow_agent, look_for_keys, gss_auth, gss_kex, gss_deleg_creds, gss_host, passphrase)
733 try:
734 key = self._key_from_filepath(
--> 735 filename, pkey_class, passphrase
736 )
737 # for 2-factor auth a successfully auth'd key will result
/usr/local/lib/python3.6/dist-packages/paramiko/client.py in _key_from_filepath(self, filename, klass, password)
584 cert_path = filename + cert_suffix
585 # Blindly try the key path; if no private key, nothing will work.
--> 586 key = klass.from_private_key_file(key_path, password)
587 # TODO: change this to 'Loading' instead of 'Trying' sometime; probably
588 # when #387 is released, since this is a critical log message users are
/usr/local/lib/python3.6/dist-packages/paramiko/pkey.py in from_private_key_file(cls, filename, password)
233 :raises: `.SSHException` -- if the key file is invalid
234 """
--> 235 key = cls(filename=filename, password=password)
236 return key
237
/usr/local/lib/python3.6/dist-packages/paramiko/rsakey.py in __init__(self, msg, data, filename, password, key, file_obj)
53 return
54 if filename is not None:
---> 55 self._from_private_key_file(filename, password)
56 return
57 if (msg is None) and (data is not None):
/usr/local/lib/python3.6/dist-packages/paramiko/rsakey.py in _from_private_key_file(self, filename, password)
173
174 def _from_private_key_file(self, filename, password):
--> 175 data = self._read_private_key_file("RSA", filename, password)
176 self._decode_key(data)
177
/usr/local/lib/python3.6/dist-packages/paramiko/pkey.py in _read_private_key_file(self, tag, filename, password)
306 """
307 with open(filename, "r") as f:
--> 308 data = self._read_private_key(tag, f, password)
309 return data
310
/usr/local/lib/python3.6/dist-packages/paramiko/pkey.py in _read_private_key(self, tag, f, password)
332
333 if keytype == tag:
--> 334 data = self._read_private_key_pem(lines, end, password)
335 pkformat = self._PRIVATE_KEY_FORMAT_ORIGINAL
336 elif keytype == "OPENSSH":
/usr/local/lib/python3.6/dist-packages/paramiko/pkey.py in _read_private_key_pem(self, lines, end, password)
384 # raise an exception pointing out that we need one
385 if password is None:
--> 386 raise PasswordRequiredException("Private key file is encrypted")
387 cipher = self._CIPHER_TABLE[encryption_type]["cipher"]
388 keysize = self._CIPHER_TABLE[encryption_type]["keysize"]
PasswordRequiredException: Private key file is encrypted
Patrick Massot (Jun 28 2020 at 08:15):
So you have your answer: the problem is in your ssh setup.
Patrick Massot (Jun 28 2020 at 08:16):
Do you use a passphrase for the SSH key that you use on GitHub?
Yakov Pechersky (Jun 28 2020 at 08:17):
Yes, that's the case
Patrick Massot (Jun 28 2020 at 08:19):
Then you're in totally untested territory. Arguably this should be possible, but I'm not surprised at all that it fails.
Patrick Massot (Jun 28 2020 at 08:19):
Feel free to open a PR to mathlibtools fixing that if you can.
Patrick Massot (Jun 28 2020 at 08:21):
Note there is no need to dig into leanproject code, you simply need to make the above lines to work.
Patrick Massot (Jun 28 2020 at 08:21):
I'm sure paramiko's documentation will help.
Patrick Stevens (Jun 28 2020 at 08:37):
FWIW my workflow where I just explicitly leanproject get-cache Just Works (tm), I've got a passphrase on my SSH key on macOS
Yakov Pechersky (Jun 28 2020 at 08:56):
https://github.com/leanprover-community/mathlib-tools/pull/61
Last updated: Dec 20 2023 at 11:08 UTC