Emacs

Note

There are many existing solutions for using Emacs with Lean such as leanprover-community/lean4-mode and mekeor/nael. You probably want to use one of these rather than Lspleank or Webleank.

You can try Lspleank with Emacs's built-in LSP client (Eglot), by adding the following lines to your ~/.emacs.d/init.el file:

(define-derived-mode lean-mode fundamental-mode "Lean")

(add-to-list 'auto-mode-alist '("\\.lean\\'" . lean-mode))

(with-eval-after-load 'eglot
  (add-to-list 'eglot-server-programs
               '(lean-mode . ("lspleank" "lake"))))

(add-hook 'lean-mode-hook 'eglot-ensure)

See https://www.gnu.org/software/emacs/manual/eglot.html for more information.