How to disable Lean server in Emacs lean4-mode?

Stream: Emacs

[Ching-Tsun Chou]

I mainly use VScode to edit Lean file and interact with Lean server. But sometimes I also use Emacs, because the search-and-replace functionality in VScode is just too painful to use. So I would like to use Emacs lean4-mode to edit Lean files without starting a Lean server. How do I do that?

[Kevin Buzzard]

I've used Emacs in the past to edit lean files when I want to use macros and have a more powerful editing experience. But because I mainly use VS Code I just deleted all lean-related things from my Emacs setup and so when I open a lean file my Emacs treats it like a text file. I can then hack away in Emacs whilst having the same file open in VS Code to view the changes with the server running.

[Mekeor Melire]

Thoughts from reading the source code; without having tested: I'd guess that what triggers lsp-mode is: lean4-mode thenlean4-mode-setup then lean4-create-lsp-workspace then lsp-workspace-folders-add. You could thus for example define an advice overriding lean4-create-lsp-workspace like this:

(define-advice lean4-create-lsp-workspace (:override ()))

---

Beyond lean4-mode:

As @Kevin Buzzard mentioned, you can also deinstall lean4-mode. Or use my fork Nael which is carefully engineered to not depend on lsp-mode and to not even load any LSP client unless one is spawned. There's also lean-ts-mode which seems to not start Eglot automatically.

[Ching-Tsun Chou]

Thanks for the comments! I found an easy solution: I just used Emacs's customization interface to set lean4-executable-name to "nil" for the current and future sessions. (This will save the change in the ~/.emacs file.) Then Emacs will fail to launch Lean when I edit a Lean file. This generates some error messages, which can be easily ignored by typing ^G.

I don't want to uninstall lean4-mode, because I still want all the syntax highlighting and the ability to type Lean's unicode characters via the standard key binding.

BTW, I also use this VScode extension:
https://github.com/whitphx/vscode-emacs-mcx
This makes the key bindings of VScode close to those of Emacs, even though there are still many situations where the two editors behaves differently.

[Britt Anderson]

I find using emacs for lean more pleasant than vs code, probably because I am so embedded in emacs for everything else. With an lsp and the lean4 mode things work pretty smoothly for me. I think these are the sections from my init file that are relevant. Not much of a set up really:

(use-package lsp-mode
  :init (setq lsp-keymap-prefix "C-c s")
  :config
  (require 'lsp-haskell)
  (setq lsp-rename-use-prepare nil ; temp fix for broken rename in haskell on emacs jan 18 2026
    lsp-enable-snippet t
        lsp-enable-symbol-highlighting t
        lsp-enable-on-type-formatting nil
        lsp-headerline-breadcrumb-enable t
        lsp-modeline-code-actions-enable t
        lsp-modeline-diagnostics-enable t
        lsp-completion-provider :capf))

(use-package lsp-ui
  :config (setq lsp-ui-doc-use-childframe nil)
  )

(use-package lean4-mode
  :commands lean4-mode
  :vc (:url "https://github.com/leanprover-community/lean4-mode.git"
       :rev :last-release
       )
  :hook (lean4-mode . lsp))

;; trying to get my path variables for this user emacs version
;; the same as the system environment
(use-package exec-path-from-shell
  )

(exec-path-from-shell-initialize)

(use-package dash
  );;dependency for lean4-mode

;;for lsp to work I need to increase the gc-cons level. It is suggested to make
;; this a big number, and also I need the lean stuff on my emacs path,
;;which is not always the same as my system path. To be safe I am
;;adding it here

(setq gc-cons-threshold 100000000)
(add-to-list 'exec-path "/home/britt/.elan/bin")

Good luck.