update-mathlib required 'github'?

Stream: new members

[Vaibhav Karve]

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]

How did you install this update-mathlib script?

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

The answer to your specific question is PyGithub.

[Vaibhav Karve]

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]

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]

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

[Vaibhav Karve]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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.