Zulip Chat Archive

Stream: new members

Topic: failed to start child process?

Joseph O (Apr 24 2022 at 01:02):

I keep getting this error when trying to add mathlib.
image.png

Kevin Buzzard (Apr 24 2022 at 07:25):

If you're using lean 3 then you should be using leanproject not leanpkg to make a project which depends on mathlib, and if you're using lean 4 then you're in the wrong stream.

Joseph O (Apr 24 2022 at 12:14):

Ah ok, I will use leanproject

Joseph O (Apr 24 2022 at 13:33):

Seems like it can't find leanproject, yet I'm using lean 3
image.png
image.png

Kevin Buzzard (Apr 24 2022 at 14:14):

Follow the installation instructions on the community website.

Mauricio Collares (Apr 24 2022 at 14:49):

https://leanprover-community.github.io/install/windows.html

Arthur Paulino (Apr 24 2022 at 15:02):

leanproject is a Python package so you will need to make it available in your PATH as you'd usually do with any other Python package

Arthur Paulino (Apr 24 2022 at 15:10):

(the Python package is actually mathlibtools if I recall correctly)

Joseph O (Apr 24 2022 at 15:20):

hmm, im using leanproject, but it still cant find mathlib
image.png

Kevin Buzzard (Apr 24 2022 at 15:21):

There is a handy URL in the error message which lists some of the many things which you could have done wrong

Joseph O (Apr 24 2022 at 15:21):

Oh I see.

Joseph O (Apr 24 2022 at 15:23):

I ran leanproject get-mathlib-cache and the problem persists

Mauricio Collares (Apr 24 2022 at 15:53):

What are the contents of your leanpkg.toml file?

Mauricio Collares (Apr 24 2022 at 15:55):

And what folder did you open VS Code in?

Last updated: Dec 20 2023 at 11:08 UTC