Notes on Lean4 with Emacs

1. Introduction

I had to install elan with

git clone https://github.com/leanprover/elan
cd elan
cargo build --release
target/release/elan-init

This set up everything for me; because I chose not to modify $PATH I had to set up my .profile:

[ -f "$HOME/.elan/env" ] && source "$HOME/.elan/env"

I git-cloned the lean4-mode package in ~/code/git/lean4-mode and configured Emacs with:

;; This mode is tightly integrated with LSP.
(use-package lean4-mode
  :load-path "~/code/git/lean4-mode"
  :ensure nil)

;; This mode uses Eglot instead.
(use-package nael)

;; Suppress workspace/inlayHint/refresh requests from Lean/lake LSP
;; server, see <https://github.com/leanprover/lean4/issues/7488#issuecomment-3559786608>.
(defun my/suppress-lsp-inlayhint-warnings (orig-fun type message &rest args)
  "Suppress LSP inlayHint/refresh warnings."
  (unless (and (eq type 'lsp-mode)
               (string-match-p "workspace/inlayHint/refresh" message))
    (apply orig-fun type message args)))

(advice-add 'display-warning :around #'my/suppress-lsp-inlayhint-warnings)

I also customized lsp-file-watch-ignored-directories to include "[/\\\\]\\.lake\\'".

1.1. Keybindings

View/close goals with C-c TAB.
View errors and warnings with flycheck with C-c ! l.

1.2. Search

Search can be performed with Loogle, either online or locally using lake exe loogle. As the Loogle repository README advises, lake build LoogleMathlibCache will build precompute an index for large libraries like Mathlib to make searching faster.

1.3. Tactics documentation

Tactics are detailed in the Tactics-Reference section of the Lean 4 docs.