Zulip Chat Archive

Stream: new members

Topic: lean path


view this post on Zulip Hendrik (Sep 22 2018 at 04:14):

I have the following problem: After installing the lean vs code extension and downloading the math library, adding the math library to a workspace results in unresolved imports because the math library is not inside the LEAN_PATH.

Does this mean that the math library needs to be saved inside the lean folder or is there a way to add the path to the math library to LEAN_PATH?

view this post on Zulip Bryan Gin-ge Chen (Sep 22 2018 at 04:25):

Are you using leanpkg add to set up mathlib?

view this post on Zulip Bryan Gin-ge Chen (Sep 22 2018 at 04:26):

There are some detailed instructions here which worked for me.

view this post on Zulip Hendrik (Sep 22 2018 at 04:30):

Oh, I didn't, I simply forked the math library from github. Thank you for the link!

view this post on Zulip Hendrik (Sep 22 2018 at 04:40):

I got to the point where lean --version works well but trying to create a project fails to the "failed to start child process" error also documented here: https://groups.google.com/forum/#!topic/lean-user/a3nphm5h2p4

view this post on Zulip Geoffrey Yeung (Sep 22 2018 at 06:11):

just my 2 cents, in my case it was because git was not in PATH

view this post on Zulip Hendrik (Sep 22 2018 at 07:19):

I'm pretty sure the path variables are set correctly. Maybe I will try the linux installation some time in the future. I think the developers should actually put a lot more attention on making lean accessible to new users. I am comfortable with command line use but doing a project with students would be a nightmare.

view this post on Zulip Bryan Gin-ge Chen (Sep 22 2018 at 13:15):

I have a working setup on windows 10 and I don't recall ever having to deal with this error. I'm using the bash shell that comes with git for windows "C:\Program Files\Git\bin\sh.ext", though I'm using it from the program cmder. The only lean-related thing I have in the path (which I placed in my .bashrc) is the path to my lean-nightly directory which is inside something like users\user\Downloads.

When exactly does the failed to start child process error occur, and does it say anything else? Is it when running leanpkg new? We should at least be able to figure out where it's being triggered...

view this post on Zulip Bryan Gin-ge Chen (Sep 23 2018 at 18:36):

@Hendrik It looks like this issue has been figured out here. One quick solution is simply to try the git-bash shell if you have that installed.


Last updated: May 07 2021 at 00:30 UTC