leanpkg issues (no more issue)

Stream: new members

[Danila Kurganov]

Hi,

I am having issues with lean on vscode; I have aleanpkg.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]

How did you install lean? Did you see the installation instructions: https://github.com/leanprover-community/mathlib/tree/master/docs/install

[Danila Kurganov]

No more issues now, Kevin has helped me by just getting lean project up and running and now no issues persist!

[Dan Stanescu]

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]

Never mind, figured it out.

[Dan Stanescu]

It was not a mathlib issue.

[Kevin Buzzard]

Just to let you know that there is now leanproject which supercedes leanpkg and update-mathlib. You can download it with pip install mathlibtools or similar -- see the installation instructions for your OS.