Zulip Chat Archive
Stream: new members
Topic: Lean extension not working
Relerx 033 (May 19 2020 at 01:51):
the lean extension is not working for me on Visual Studio Code, Windows, not sure what I've done wrong while installing?
Bryan Gin-ge Chen (May 19 2020 at 01:52):
How did you install lean?
Relerx 033 (May 19 2020 at 01:53):
I followed this: https://leanprover-community.github.io/install/windows.html
and installed Lean through extensions manager or w/e it is called in Visual Studio Code
Bryan Gin-ge Chen (May 19 2020 at 01:54):
Does Lean work from git bash?
Relerx 033 (May 19 2020 at 01:54):
how do I check that?
Bryan Gin-ge Chen (May 19 2020 at 01:55):
Open the git bash terminal and type lean --version and see what you get.
Relerx 033 (May 19 2020 at 01:55):
Lean (version 3.13.2, commit f36f98fba8e7, Release)
Relerx 033 (May 19 2020 at 01:56):
(also it seems to run my test file well when I do "lean xyz.lean")
Bryan Gin-ge Chen (May 19 2020 at 01:57):
Does lean --version work from VS Code's built-in terminal? (Ctrl + `)
Relerx 033 (May 19 2020 at 01:59):
No, says: bash: lean: command not found
Relerx 033 (May 19 2020 at 02:00):
I restarted Visual Studio Code and it seems to work now, my bad, thanks for the help!
Bryan Gin-ge Chen (May 19 2020 at 02:01):
No problem! Just to make sure; you didn't restart VS Code after installing the extension before, right?
Relerx 033 (May 19 2020 at 02:03):
I didn't
Bryan Gin-ge Chen (May 19 2020 at 02:05):
OK, I'll update the instructions to add that as a step.
Last updated: Dec 20 2023 at 11:08 UTC