lean path

Stream: new members

[Hendrik]

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?

[Bryan Gin-ge Chen]

Are you using leanpkg add to set up mathlib?

[Bryan Gin-ge Chen]

There are some detailed instructions here which worked for me.

[Hendrik]

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

[Hendrik]

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

[Geoffrey Yeung]

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

[Hendrik]

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.

[Bryan Gin-ge Chen]

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...

[Bryan Gin-ge Chen]

@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.