Zulip Chat Archive

Stream: new members

Topic: Trouble installing Lean (Windows)

Keefer Rowan (May 11 2020 at 15:10):

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 (May 11 2020 at 15:15):

Restarting VSCode seems to have solved the problem.

Jalex Stark (May 11 2020 at 15:15):

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 (May 11 2020 at 15:16):

oh, you beat me to it :)

Jalex Stark (May 11 2020 at 15:16):

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

Last updated: Dec 20 2023 at 11:08 UTC