Zulip Chat Archive

Stream: general

Topic: I broke something...

Bhavik Mehta (May 12 2020 at 13:36):

I've managed to somehow break my lean setup. I did a mathlib pull, then made a branch and edited a bit. Then I restarted lean in vscode and now I get this:

$ leanpkg build
dyld: Library not loaded: /usr/local/opt/gmp/lib/libgmp.10.dylib
  Referenced from: /Users/bmehta/.elan/toolchains/leanprover-community-lean-3.11.0/bin/lean
  Reason: Incompatible library version: lean requires version 15.0.0 or later, but libgmp.10.dylib provides version 14.0.0
Abort trap: 6

What did I do wrong and how do I fix it?

Gabriel Ebner (May 12 2020 at 13:37):

I think you need to install a newer version of gmp.

Gabriel Ebner (May 12 2020 at 13:37):

Maybe brew upgrade gmp (I don't have a mac)?

Gabriel Ebner (May 12 2020 at 13:38):

This probably related to the new CI setup we're using. The binaries are now built on macos 10.15, and the VM probably has a newer version installed than we had on travis.

Bhavik Mehta (May 12 2020 at 13:41):

That seems to have fixed it, thanks!

Bhavik Mehta (May 12 2020 at 13:54):

Yikes something else has gone wrong too now...

$ leanproject get-mathlib-cache
Traceback (most recent call last):
  File "/Users/bmehta/.pyenv/versions/usual/bin/leanproject", line 5, in <module>
    from mathlibtools.leanproject import safe_cli
  File "/Users/bmehta/.pyenv/versions/3.6.2/envs/usual/lib/python3.6/site-packages/mathlibtools/leanproject.py", line 9, in <module>
    import paramiko # type: ignore
  File "/Users/bmehta/.pyenv/versions/3.6.2/envs/usual/lib/python3.6/site-packages/paramiko/__init__.py", line 22, in <module>
    from paramiko.transport import SecurityOptions, Transport
  File "/Users/bmehta/.pyenv/versions/3.6.2/envs/usual/lib/python3.6/site-packages/paramiko/transport.py", line 129, in <module>
    class Transport(threading.Thread, ClosingContextManager):
  File "/Users/bmehta/.pyenv/versions/3.6.2/envs/usual/lib/python3.6/site-packages/paramiko/transport.py", line 190, in Transport
    if KexCurve25519.is_available():
  File "/Users/bmehta/.pyenv/versions/3.6.2/envs/usual/lib/python3.6/site-packages/paramiko/kex_curve25519.py", line 30, in is_available
    X25519PrivateKey.generate()
  File "/Users/bmehta/.pyenv/versions/3.6.2/envs/usual/lib/python3.6/site-packages/cryptography/hazmat/primitives/asymmetric/x25519.py", line 38, in generate
    from cryptography.hazmat.backends.openssl.backend import backend
  File "/Users/bmehta/.pyenv/versions/3.6.2/envs/usual/lib/python3.6/site-packages/cryptography/hazmat/backends/openssl/__init__.py", line 7, in <module>
    from cryptography.hazmat.backends.openssl.backend import backend
  File "/Users/bmehta/.pyenv/versions/3.6.2/envs/usual/lib/python3.6/site-packages/cryptography/hazmat/backends/openssl/backend.py", line 75, in <module>
    from cryptography.hazmat.bindings.openssl import binding
  File "/Users/bmehta/.pyenv/versions/3.6.2/envs/usual/lib/python3.6/site-packages/cryptography/hazmat/bindings/openssl/binding.py", line 195, in <module>
    Binding.init_static_locks()
  File "/Users/bmehta/.pyenv/versions/3.6.2/envs/usual/lib/python3.6/site-packages/cryptography/hazmat/bindings/openssl/binding.py", line 142, in init_static_locks
    __import__("_ssl")
ImportError: dlopen(/Users/bmehta/.pyenv/versions/3.6.2/lib/python3.6/lib-dynload/_ssl.cpython-36m-darwin.so, 2): Library not loaded: /usr/local/opt/openssl/lib/libssl.1.0.0.dylib
  Referenced from: /Users/bmehta/.pyenv/versions/3.6.2/lib/python3.6/lib-dynload/_ssl.cpython-36m-darwin.so
  Reason: image not found

Bhavik Mehta (May 12 2020 at 13:55):

This was in the master branch of mathlib

Kevin Buzzard (May 12 2020 at 14:28):

Did you try updating leanproject? It went to 0.0.6 just the other day. But this doesn't look like it has anything to do with it...

Bhavik Mehta (May 12 2020 at 14:29):

Seems like my pip is broken too :(

Patrick Massot (May 12 2020 at 14:59):

Yes, your python is broken. To be honest, this SSL stuff is a wonderful tool to detect broken systems.

Patrick Massot (May 12 2020 at 15:02):

But now I'm really confused because https://github.com/leanprover-community/mathlib-tools/blob/master/mathlibtools/leanproject.py#L8-L16 is meant exactly for this purpose.

Patrick Massot (May 12 2020 at 15:03):

Could you run leanproject --version and tell us the answer?

Bhavik Mehta (May 12 2020 at 16:46):

What's confusing is that everything worked fine before I did a mathlib pull, and I haven't touched python otherwise

Bhavik Mehta (May 12 2020 at 16:47):

$ leanproject --version
Traceback (most recent call last):
  File "/Users/bmehta/.pyenv/versions/usual/bin/leanproject", line 5, in <module>
    from mathlibtools.leanproject import safe_cli
  File "/Users/bmehta/.pyenv/versions/3.6.2/envs/usual/lib/python3.6/site-packages/mathlibtools/leanproject.py", line 9, in <module>
    import paramiko # type: ignore
  File "/Users/bmehta/.pyenv/versions/3.6.2/envs/usual/lib/python3.6/site-packages/paramiko/__init__.py", line 22, in <module>
    from paramiko.transport import SecurityOptions, Transport
  File "/Users/bmehta/.pyenv/versions/3.6.2/envs/usual/lib/python3.6/site-packages/paramiko/transport.py", line 129, in <module>
    class Transport(threading.Thread, ClosingContextManager):
  File "/Users/bmehta/.pyenv/versions/3.6.2/envs/usual/lib/python3.6/site-packages/paramiko/transport.py", line 190, in Transport
    if KexCurve25519.is_available():
  File "/Users/bmehta/.pyenv/versions/3.6.2/envs/usual/lib/python3.6/site-packages/paramiko/kex_curve25519.py", line 30, in is_available
    X25519PrivateKey.generate()
  File "/Users/bmehta/.pyenv/versions/3.6.2/envs/usual/lib/python3.6/site-packages/cryptography/hazmat/primitives/asymmetric/x25519.py", line 38, in generate
    from cryptography.hazmat.backends.openssl.backend import backend
  File "/Users/bmehta/.pyenv/versions/3.6.2/envs/usual/lib/python3.6/site-packages/cryptography/hazmat/backends/openssl/__init__.py", line 7, in <module>
    from cryptography.hazmat.backends.openssl.backend import backend
  File "/Users/bmehta/.pyenv/versions/3.6.2/envs/usual/lib/python3.6/site-packages/cryptography/hazmat/backends/openssl/backend.py", line 75, in <module>
    from cryptography.hazmat.bindings.openssl import binding
  File "/Users/bmehta/.pyenv/versions/3.6.2/envs/usual/lib/python3.6/site-packages/cryptography/hazmat/bindings/openssl/binding.py", line 195, in <module>
    Binding.init_static_locks()
  File "/Users/bmehta/.pyenv/versions/3.6.2/envs/usual/lib/python3.6/site-packages/cryptography/hazmat/bindings/openssl/binding.py", line 142, in init_static_locks
    __import__("_ssl")
ImportError: dlopen(/Users/bmehta/.pyenv/versions/3.6.2/lib/python3.6/lib-dynload/_ssl.cpython-36m-darwin.so, 2): Library not loaded: /usr/local/opt/openssl/lib/libssl.1.0.0.dylib
  Referenced from: /Users/bmehta/.pyenv/versions/3.6.2/lib/python3.6/lib-dynload/_ssl.cpython-36m-darwin.so
  Reason: image not found

Bhavik Mehta (May 12 2020 at 16:47):

My python environment was working well beforehand, and after that pull everything broke (including tmux, somehow)

Gabriel Ebner (May 12 2020 at 16:56):

Maybe the brew upgrade gmp changed something?

Bhavik Mehta (May 12 2020 at 16:58):

Yeah I think that's what it is too... I've got tmux working at least

Bhavik Mehta (May 12 2020 at 16:59):

Trying to fix my pyenv and pip now

Patrick Massot (May 12 2020 at 17:29):

Ah of course you can't run leanprover --version if the imports are broken. Could you check whether /Users/bmehta/.pyenv/versions/3.6.2/envs/usual/lib/python3.6/site-packages/mathlibtools/leanproject.py looks like what is on GitHub?

Bhavik Mehta (May 12 2020 at 18:11):

It looks similar but not the same, I have 

import sys
import os
import subprocess
from pathlib import Path
from datetime import datetime
from typing import Tuple, Optional

from git.exc import GitCommandError # type: ignore
import paramiko # type: ignore
from paramiko.ssh_exception import AuthenticationException, SSHException # type: ignore

Instead of lines 1-17

Bhavik Mehta (May 12 2020 at 18:11):

I think this is a problem with my pip rather than mathlibtools though!

Bhavik Mehta (May 12 2020 at 18:31):

It seems like I'm having this problem: https://github.com/kelaberetiv/TagUI/issues/86. It doesn't seem to be related to lean or mathlibtools so I'll stop asking about it here

Bhavik Mehta (May 12 2020 at 18:43):

Sorted! Thanks all for help

Bhavik Mehta (May 12 2020 at 18:44):

Gabriel Ebner said:

Maybe the brew upgrade gmp changed something?

I think this was the problem, brew upgrade updates everything which brew installed, which bungled a bunch of stuff I had... brew update is what it should have been!

Reid Barton (May 12 2020 at 18:45):

Classic

Patrick Massot (May 12 2020 at 19:08):

Ok, at least it clears the mystery of why leanproject's defense didn't trigger: you're running an outdated leanproject

Patrick Massot (May 12 2020 at 19:09):

Note those are lame defenses: it simply gives up on using SSH in hostile territory

Bhavik Mehta (May 12 2020 at 19:09):

Yeah I hadn't updated mathlibtools in a little bit of time

Bhavik Mehta (Jul 22 2020 at 14:07):

I've somehow got this error again!

Bhavik Mehta (Jul 22 2020 at 14:31):

To fix it I had to uninstall openssl via brew (forcing it to ignore dependencies), and reinstall an older version

Bhavik Mehta (Jul 22 2020 at 14:31):

Not pleasant :(

Bhavik Mehta (Jul 24 2020 at 14:46):

Alright this is causing issues again. I'm fairly sure it's not an issue with my python now, since the error message (virtually the same as above) is about the imports, but when I try to run any of those imports from a python shell there's no errors

Bhavik Mehta (Jul 24 2020 at 14:46):

I'll just go back to using leanpkg I think

Patrick Massot (Jul 24 2020 at 15:17):

There is hope. @Matt Earnshaw is trying to help getting rid of the Paramiko dependency.

Last updated: Dec 20 2023 at 11:08 UTC