Stream: new members
Danila Kurganov (Mar 12 2020 at 18:24):
I am having issues with lean on vscode; I have a
leanpkg.path doesn't exist error, and then a
failed to start child process once vscode tries to fix it. How do I get lean up and running?
Gabriel Ebner (Mar 12 2020 at 18:26):
How did you install lean? Did you see the installation instructions: https://github.com/leanprover-community/mathlib/tree/master/docs/install
Danila Kurganov (Mar 12 2020 at 19:12):
No more issues now, Kevin has helped me by just getting lean project up and running and now no issues persist!
Dan Stanescu (Mar 16 2020 at 18:02):
After having installed
mathlib on Linux, all seemed fine (i.e. I could use it) until today I tried to update:
./update-mathlib Traceback (most recent call last): File "./update-mathlib", line 6, in <module> from github import Github File "/home/dan/.local/lib/python3.7/site-packages/github/__init__.py", line 44, in <module> from github.MainClass import Github, GithubIntegration File "/home/dan/.local/lib/python3.7/site-packages/github/MainClass.py", line 57, in <module> import jwt ModuleNotFoundError: No module named 'jwt'
Anyone can advise? I think I used
update-mathlib before on this machine, but am not quite 100% positive.
Dan Stanescu (Mar 16 2020 at 18:28):
Never mind, figured it out.
Dan Stanescu (Mar 16 2020 at 18:29):
It was not a
Kevin Buzzard (Mar 16 2020 at 19:21):
Just to let you know that there is now
leanproject which supercedes
update-mathlib. You can download it with
pip install mathlibtools or similar -- see the installation instructions for your OS.
Last updated: May 13 2021 at 18:26 UTC