Zulip Chat Archive

Stream: general

Topic: leanproject get mathlib, https vs ssh


view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jun 28 2020 at 07:45):

It doesn't.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jun 28 2020 at 08:03):

--debug will only help when leanproject crashes.

view this post on Zulip Patrick Massot (Jun 28 2020 at 08:03):

What does leanproject --version says?

view this post on Zulip Yakov Pechersky (Jun 28 2020 at 08:04):

leanproject --version
leanproject, version 0.0.8

view this post on Zulip Patrick Massot (Jun 28 2020 at 08:04):

Also try lauching python and import paramiko

view this post on Zulip Patrick Massot (Jun 28 2020 at 08:05):

and from paramiko.ssh_exception import AuthenticationException, SSHException

view this post on Zulip 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'

view this post on Zulip Yakov Pechersky (Jun 28 2020 at 08:05):

so it works for python3, not python

view this post on Zulip Patrick Massot (Jun 28 2020 at 08:06):

This is 2020, when people say python you need to understand python3.

view this post on Zulip Yakov Pechersky (Jun 28 2020 at 08:07):

This is on a mostly clean new install of 18.04

view this post on Zulip Patrick Massot (Jun 28 2020 at 08:08):

You should upgrade to 20.04 to get rid of python2.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jun 28 2020 at 08:15):

So you have your answer: the problem is in your ssh setup.

view this post on Zulip Patrick Massot (Jun 28 2020 at 08:16):

Do you use a passphrase for the SSH key that you use on GitHub?

view this post on Zulip Yakov Pechersky (Jun 28 2020 at 08:17):

Yes, that's the case

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jun 28 2020 at 08:19):

Feel free to open a PR to mathlibtools fixing that if you can.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jun 28 2020 at 08:21):

I'm sure paramiko's documentation will help.

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Jun 28 2020 at 08:56):

https://github.com/leanprover-community/mathlib-tools/pull/61


Last updated: May 11 2021 at 23:11 UTC