Zulip Chat Archive

Stream: general

Topic: Trying to run update-mathlib

Floris van Doorn (Apr 30 2019 at 17:17):

I'm trying to get update-mathlib to work. I am on Windows, and I usually use the msys2 minGW 64-bit command prompt. I tried installing update-mathlib on both my msys2 terminal, and in a Git Bash terminal.

In msys2, when I try to run the script to get update-mathlib I get an error. The first line in the output that looks like an error is (full output at the bottom of this message)

requests 2.21.0 has requirement urllib3<1.25,>=1.21.1, but you'll have urllib3 1.25.2 which is incompatible.

It seems like one of my packages is too new?

I now also tried using git bash with choco as package manager. Running the install-update-mathlib script works without errors.
However, if I then run update-mathlib I get the error that python3 is not found. (does choco come automatically come with pip but not with python? Is that even possible?)
So I install python3 (choco install python3), but now I get the following error.

Floris@MSI MINGW64 /d/projects/formalabstracts (master)
$ update-mathlib
Traceback (most recent call last):
  File "C:/Users/Floris/.mathlib/bin/update-mathlib", line 6, in <module>
    from github import Github
ModuleNotFoundError: No module named 'github'

How do I continue? pip install github doesn't work.

full output of the msys2 install-update-mathlib script:

Floris@MSI MINGW64 /d/projects
$ curl https://raw.githubusercontent.com/leanprover-community/mathlib/master/scripts/remote-install-update-mathlib.sh -sSf | sh
Installing python dependencies (at user level)
/usr/bin/pip3
Collecting setuptools
  Downloading https://files.pythonhosted.org/packages/ec/51/f45cea425fd5cb0b0380f5b0f048ebc1da5b417e48d304838c02d6288a1e/setuptools-41.0.1-py2.py3-none-any.whl (575kB)
    100% |████████████████████████████████| 583kB 2.0MB/s
Installing collected packages: setuptools
Successfully installed setuptools-41.0.1
Requirement already up-to-date: toml in /home/Floris/.local/lib/python3.7/site-packages (0.10.0)
Collecting PyGithub
  Downloading https://files.pythonhosted.org/packages/f7/48/ec5ef5239f3a4043ee7e07b454b5f3a024a5f22a4e585400ac6caa22c3c4/PyGithub-1.43.7.tar.gz (107kB)
    100% |████████████████████████████████| 112kB 1.1MB/s
Collecting urllib3
  Downloading https://files.pythonhosted.org/packages/39/ec/d93dfc69617a028915df914339ef66936ea976ef24fa62940fd86ba0326e/urllib3-1.25.2-py2.py3-none-any.whl (150kB)
    100% |████████████████████████████████| 153kB 1.5MB/s
Collecting certifi
  Using cached https://files.pythonhosted.org/packages/60/75/f692a584e85b7eaba0e03827b3d51f45f571c2e793dd731e598828d380aa/certifi-2019.3.9-py2.py3-none-any.whl
Collecting gitpython
  Using cached https://files.pythonhosted.org/packages/fe/e5/fafe827507644c32d6dc553a1c435cdf882e0c28918a5bab29f7fbebfb70/GitPython-2.1.11-py2.py3-none-any.whl
Collecting deprecated (from PyGithub)
  Using cached https://files.pythonhosted.org/packages/9f/7a/003fa432f1e45625626549726c2fbb7a29baa764e9d1fdb2323a5d779f8a/Deprecated-1.2.5-py2.py3-none-any.whl
Collecting pyjwt (from PyGithub)
  Using cached https://files.pythonhosted.org/packages/87/8b/6a9f14b5f781697e51259d81657e6048fd31a113229cf346880bb7545565/PyJWT-1.7.1-py2.py3-none-any.whl
Collecting requests>=2.14.0 (from PyGithub)
  Using cached https://files.pythonhosted.org/packages/7d/e3/20f3d364d6c8e5d2353c72a67778eb189176f08e873c9900e10c0287b84b/requests-2.21.0-py2.py3-none-any.whl
Collecting gitdb2>=2.0.0 (from gitpython)
  Using cached https://files.pythonhosted.org/packages/da/30/a407568aa8d8f25db817cf50121a958722f3fc5f87e3a6fba1f40c0633e3/gitdb2-2.0.5-py2.py3-none-any.whl
Collecting wrapt<2,>=1 (from deprecated->PyGithub)
  Using cached https://files.pythonhosted.org/packages/67/b2/0f71ca90b0ade7fad27e3d20327c996c6252a2ffe88f50a95bba7434eda9/wrapt-1.11.1.tar.gz
Collecting chardet<3.1.0,>=3.0.2 (from requests>=2.14.0->PyGithub)
  Using cached https://files.pythonhosted.org/packages/bc/a9/01ffebfb562e4274b6487b4bb1ddec7ca55ec7510b22e4c51f14098443b8/chardet-3.0.4-py2.py3-none-any.whl
Collecting idna<2.9,>=2.5 (from requests>=2.14.0->PyGithub)
  Using cached https://files.pythonhosted.org/packages/14/2c/cd551d81dbe15200be1cf41cd03869a46fe7226e7450af7a6545bfc474c9/idna-2.8-py2.py3-none-any.whl
Collecting smmap2>=2.0.0 (from gitdb2>=2.0.0->gitpython)
  Using cached https://files.pythonhosted.org/packages/55/d2/866d45e3a121ee15a1dc013824d58072fd5c7799c9c34d01378eb262ca8f/smmap2-2.0.5-py2.py3-none-any.whl
requests 2.21.0 has requirement urllib3<1.25,>=1.21.1, but you'll have urllib3 1.25.2 which is incompatible.
Installing collected packages: wrapt, deprecated, pyjwt, chardet, certifi, urllib3, idna, requests, PyGithub, smmap2, gitdb2, gitpython
  Running setup.py install for wrapt ... error
    Complete output from command /usr/bin/python3 -u -c "import setuptools, tokenize;__file__='/tmp/pip-install-ooh4zvm2/wrapt/setup.py';f=getattr(tokenize, 'open', open)(__file__);code=f.read().replace('\r\n', '\n');f.close();exec(compile(code, __file__, 'exec'))" install --record /tmp/pip-record-yk7wu2wz/install-record.txt --single-version-externally-managed --compile --user --prefix=:
    running install
    running build
    running build_py
    creating build
    creating build/lib.mingw64_nt-10.0-3.0.6(0.338
    creating build/lib.mingw64_nt-10.0-3.0.6(0.338/5
    creating build/lib.mingw64_nt-10.0-3.0.6(0.338/5/3)-x86_64-3.7
    creating build/lib.mingw64_nt-10.0-3.0.6(0.338/5/3)-x86_64-3.7/wrapt
    copying src/wrapt/decorators.py -> build/lib.mingw64_nt-10.0-3.0.6(0.338/5/3)-x86_64-3.7/wrapt
    copying src/wrapt/importer.py -> build/lib.mingw64_nt-10.0-3.0.6(0.338/5/3)-x86_64-3.7/wrapt
    copying src/wrapt/wrappers.py -> build/lib.mingw64_nt-10.0-3.0.6(0.338/5/3)-x86_64-3.7/wrapt
    copying src/wrapt/__init__.py -> build/lib.mingw64_nt-10.0-3.0.6(0.338/5/3)-x86_64-3.7/wrapt
    running build_ext
    Traceback (most recent call last):
      File "<string>", line 1, in <module>
      File "/tmp/pip-install-ooh4zvm2/wrapt/setup.py", line 101, in <module>
        run_setup(with_extensions=True)
      File "/tmp/pip-install-ooh4zvm2/wrapt/setup.py", line 71, in run_setup
        setup(**setup_kwargs_tmp)
      File "/usr/lib/python3.7/distutils/core.py", line 148, in setup
        dist.run_commands()
      File "/usr/lib/python3.7/distutils/dist.py", line 966, in run_commands
        self.run_command(cmd)
      File "/usr/lib/python3.7/distutils/dist.py", line 985, in run_command
        cmd_obj.run()
      File "/home/Floris/.local/lib/python3.7/site-packages/setuptools/command/install.py", line 61, in run
        return orig.install.run(self)
      File "/usr/lib/python3.7/distutils/command/install.py", line 545, in run
        self.run_command('build')
      File "/usr/lib/python3.7/distutils/cmd.py", line 313, in run_command
        self.distribution.run_command(command)
      File "/usr/lib/python3.7/distutils/dist.py", line 985, in run_command
        cmd_obj.run()
      File "/usr/lib/python3.7/distutils/command/build.py", line 135, in run
        self.run_command(cmd_name)
      File "/usr/lib/python3.7/distutils/cmd.py", line 313, in run_command
        self.distribution.run_command(command)
      File "/usr/lib/python3.7/distutils/dist.py", line 985, in run_command
        cmd_obj.run()
      File "/tmp/pip-install-ooh4zvm2/wrapt/setup.py", line 25, in run
        build_ext.run(self)
      File "/usr/lib/python3.7/distutils/command/build_ext.py", line 308, in run
        force=self.force)
      File "/usr/lib/python3.7/distutils/ccompiler.py", line 1034, in new_compiler
        return klass(None, dry_run, force)
      File "/usr/lib/python3.7/distutils/cygwinccompiler.py", line 280, in __init__
        CygwinCCompiler.__init__ (self, verbose, dry_run, force)
      File "/usr/lib/python3.7/distutils/cygwinccompiler.py", line 124, in __init__
        if self.ld_version >= "2.10.90":
    TypeError: '>=' not supported between instances of 'NoneType' and 'str'

    ----------------------------------------
Command "/usr/bin/python3 -u -c "import setuptools, tokenize;__file__='/tmp/pip-install-ooh4zvm2/wrapt/setup.py';f=getattr(tokenize, 'open', open)(__file__);code=f.read().replace('\r\n', '\n');f.close();exec(compile(code, __file__, 'exec'))" install --record /tmp/pip-record-yk7wu2wz/install-record.txt --single-version-externally-managed --compile --user --prefix=" failed with error code 1 in /tmp/pip-install-ooh4zvm2/wrapt/

Floris van Doorn (Apr 30 2019 at 17:22):

@Patrick Massot

Patrick Massot (Apr 30 2019 at 17:46):

I don't know anything about Windows but I've seen the requests 2.21.0 has requirement urllib3<1.25,>=1.21.1, warning. I fear this is totally out of our control, see https://github.com/kennethreitz/requests/issues/4673 and dozen of google his when asking about this message

Floris van Doorn (Apr 30 2019 at 17:49):

Can I downgrade urllib3?

Patrick Massot (Apr 30 2019 at 17:50):

This message is a warning only right?

Patrick Massot (Apr 30 2019 at 17:50):

I think it worked anyway

Floris van Doorn (Apr 30 2019 at 17:51):

Also, I don't know if this is Windows-specific, but when I install python, with choco install python3, I only get the python command, not python3:

Floris@MSI MINGW64 /d/projects
$ python --version
Python 3.7.3

Floris@MSI MINGW64 /d/projects
$ which python
/c/Python37/python

Floris@MSI MINGW64 /d/projects
$ which python3
which: no python3 in [...]

Koundinya Vajjha (Apr 30 2019 at 17:51):

On a related note, and more naively, how do I tell if update-mathlib worked? I run the command and it says it extracts the nightly, but which repo can I compare it to?

Floris van Doorn (Apr 30 2019 at 17:52):

It might be only a warning. It was printed red in msys2, so it looked important.

Patrick Massot (Apr 30 2019 at 17:52):

The issue is that I have no way to get a Windows computer anywhere here. I'm always amazed to see how people in the US seem to use Windows. In France I know no mathematician or computer scientist using Windows

Patrick Massot (Apr 30 2019 at 17:54):

My secretary will be on vacation next week, but I can't enter her office and use her Windows computer (I need to become a German professor, I'm sure they can do that)

Floris van Doorn (Apr 30 2019 at 17:56):

that's unfortunate. I have the feeling something is wrong with my setup: the install-update-mathlib script seems to install all dependencies, but then they are not imported when running update-mathlib.

Patrick Massot (Apr 30 2019 at 18:02):

Maybe it's a python2 vs python3 issue

Patrick Massot (Apr 30 2019 at 18:03):

On a related note, and more naively, how do I tell if update-mathlib worked? I run the command and it says it extracts the nightly, but which repo can I compare it to?

If it says extracting then I don't see what could fail after that. And you don't want to compare anything. You want to import stuff from mathlib in your project and see it working (without delay suggesting Lean is rebuilding everything from scratch).