Zulip Chat Archive

Stream: new members

Topic: Problems with installation

view this post on Zulip Noam Atar (Nov 22 2019 at 16:20):

I tried to install Lean and mathlib on windows using:

However I got in VSCode the following error:
Unable to start the Lean server process: Error: spawn lean ENOENT --- The lean.executablePath "lean" may be incorrect, make sure it is a valid Lean executable

What should I do?

view this post on Zulip Noam Atar (Nov 22 2019 at 16:22):

Oh nvm, I restarted VSC and it worked

view this post on Zulip Kevin Buzzard (Nov 22 2019 at 16:22):

If I do File -> Preferences -> Settings then search for lean I see that my lean executable path just says lean. Did you try switching it off and on again? Did you do all that source .profile stuff? What happens if you type lean on the command line?

Last updated: May 16 2021 at 21:11 UTC