Zulip Chat Archive

Stream: new members

Topic: leanpkg issues (no more issue)


view this post on Zulip Danila Kurganov (Mar 12 2020 at 18:24):

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?

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Dan Stanescu (Mar 16 2020 at 18:28):

Never mind, figured it out.

view this post on Zulip Dan Stanescu (Mar 16 2020 at 18:29):

It was not a mathlib issue.

view this post on Zulip Kevin Buzzard (Mar 16 2020 at 19:21):

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.


Last updated: May 13 2021 at 18:26 UTC