## Stream: new members

### Topic: update-mathlib required 'github'?

#### 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?

#### Patrick Massot (Sep 24 2019 at 13:40):

How did you install this update-mathlib script?

#### 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

#### 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

#### 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!

#### 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.

#### 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!

#### Vaibhav Karve (Sep 24 2019 at 14:06):

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

#### 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.

#### Kevin Buzzard (Nov 28 2019 at 20:56):

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

#### 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)

#### 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

#### 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