Stream: new members
Topic: Problems with installation
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?
Noam Atar (Nov 22 2019 at 16:22):
Oh nvm, I restarted VSC and it worked
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