Trouble installing Lean (Windows)

Stream: new members

[Keefer Rowan]

I'm trying to install Lean and followed https://github.com/leanprover-community/mathlib/blob/master/docs/install/windows.md exactly. I got to the end and when I try to test it in VSCode, I get:

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

In my git bash terminal, if I type "which lean" I get: /c/Users/keefe/.elan/bin/lean, so I think lean is installed and all, but VSCode is having trouble finding it I guess. Any help is much appreciated.

[Keefer Rowan]

Restarting VSCode seems to have solved the problem.

[Jalex Stark]

Is that the first error message? What happened when you did this part?
"""
Click on the extension icon (image of icon) (or (image of icon) in older versions) in the side bar on the left edge of the screen (or press ShiftCtrlX) and search for leanprover.
Click "install" (In old versions of VSCode, you might need to click "reload" afterwards)
"""

[Jalex Stark]

oh, you beat me to it :)

[Jalex Stark]

"restart VSCode" will remain shockingly useful through the rest of your time using Lean