Enabling lean4-lsp in Emacs

Stream: lean4

[Craig McLaughlin]

I have followed the instructions at: https://github.com/leanprover-community/lean4-mode/blob/master/README.md, and made the required changes to my .emacs file. When I load a *.lean file, I am met with the following message in the minibuffer:

LSP :: The following servers support current file but do not have automatic installation: lean4-lsp
You may find the installation instructions at https://emacs-lsp.github.io/lsp-mode/page/languages.

However, lean4-lsp is not listed at the provided web address. Any suggestions?

[Richard Copley]

There isn't a lean4-lsp file (Lean 4 support isn't provided by lsp-mode). The files in lean4-mode are supposed to provide everything you need.

Is your elan bin directory on the path in the environment of the emacs process? (What does M-! lake --version say?)

[Craig McLaughlin]

Ah, I see. Yeah, my path wasn't updated for the Emacs process. Thanks Richard