Spawning language server with cmd: `lean` failed

Julian / lean.nvim

neovim support for the Lean theorem prover

MIT License

248 stars 25 forks source link

Closed aagontuk closed 6 months ago

aagontuk commented 6 months ago

I have installed lean.nvim using lazy.nvim as described in README. However, I am getting the following error when I am opening a lean file:

Spawning language server with cmd: `lean` failed. The language server is either not installed, missing from PATH, or not executable.

Do I have to install the language server separately?

aagontuk commented 6 months ago

Installing elan solved the issue.