Zulip Chat Archive

Stream: new members

Topic: update-mathlib required 'github'?


view this post on Zulip Vaibhav Karve (Sep 24 2019 at 13:38):

Hello everyone. I am just starting out. I have installed Lean and it seems to be working correctly (using Emacs). The "update-mathlib" script however is throwing an error:

Traceback (most recent call last):
  File "/home/vaibhav/.mathlib/bin/update-mathlib", line 6, in <module>
    from github import Github
ModuleNotFoundError: No module named 'github'

I looked around and did not find this 'github' package -- neither on the Anaconda repositories nor on the Python Package Index. What am I missing?

view this post on Zulip Patrick Massot (Sep 24 2019 at 13:40):

How did you install this update-mathlib script?

view this post on Zulip Patrick Massot (Sep 24 2019 at 13:41):

https://github.com/leanprover-community/mathlib-tools/blob/master/scripts/remote-install-update-mathlib.sh should have installed all the python dependencies

view this post on Zulip Patrick Massot (Sep 24 2019 at 13:41):

Anyway, the PyPi package names you are looking for are all listed at https://github.com/leanprover-community/mathlib-tools/blob/master/scripts/remote-install-update-mathlib.sh#L5

view this post on Zulip Patrick Massot (Sep 24 2019 at 13:42):

The answer to your specific question is PyGithub.

view this post on Zulip Vaibhav Karve (Sep 24 2019 at 13:50):

Thanks @Patrick Massot, I was able to pip-install all the dependencies myself and it worked correctly.

To answer your previous question -- I installed update-mathlib using the quick method given in the readme (the one that uses install_debian.sh). I am not sure why this method did not work, might be because I use miniconda environments.

Either way, thanks for your help!

view this post on Zulip Patrick Massot (Sep 24 2019 at 13:51):

Oh, I have no clue about miniconda, and I guess @Simon Hudon also doesn't use it. So yes, you ventured into totally untested territory.

view this post on Zulip Patrick Massot (Sep 24 2019 at 13:52):

If you feel you can fix those scripts to work in your environment, then you are very welcome to contribute!

view this post on Zulip Vaibhav Karve (Sep 24 2019 at 14:06):

Good idea. I will try to figure out what went wrong.

view this post on Zulip Kevin Buzzard (Nov 28 2019 at 20:54):

I'm with an undergraduate who is on a mac and followed the instructions to the letter and has also got this error -- no module named github -- when running update-mathlib for the first time.

view this post on Zulip Kevin Buzzard (Nov 28 2019 at 20:56):

I think I've fixed this by typing pip install toml PyGithub certifi gitpython requests

view this post on Zulip Kevin Buzzard (Nov 28 2019 at 20:57):

I will note that when I typed this I got an error "ERROR: pygithub 1.44.1 has requirement requests>=2.14.0 but you'll have requests 2.12.4 which is incompatible" (I've typed that error manually because the student isn't on the Lean chat)

view this post on Zulip Bhavik Mehta (Nov 28 2019 at 20:58):

I also had this issue (also on a mac), basically the same thing fixed it for me at the time

view this post on Zulip Kevin Buzzard (Nov 28 2019 at 20:59):

Ok so update-mathlib is definitely working, she has the olean files, all is well, but there's perhaps something wrong with the installation instructions.


Last updated: May 09 2021 at 18:17 UTC