Problems with installation

Stream: new members

[Noam Atar]

Hi,
I tried to install Lean and mathlib on windows using:
https://github.com/leanprover-community/mathlib/blob/master/docs/install/windows.md

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]

Oh nvm, I restarted VSC and it worked

[Kevin Buzzard]

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?