To use lean4-mode in Emacs, add the following to your init.el:
;; You need to modify the following line
(setq load-path (cons "/path/to/lean4/lean4-mode" load-path))
(setq lean4-mode-required-packages '(dash f flycheck lsp-mode magit-section s))
(require 'package)
(add-to-list 'package-archives '("melpa" . "http://melpa.org/packages/"))
(package-initialize)
(let ((need-to-refresh t))
(dolist (p lean4-mode-required-packages)
(when (not (package-installed-p p))
(when need-to-refresh
(package-refresh-contents)
(setq need-to-refresh nil))
(package-install p))))
(require 'lean4-mode)
If things are working correctly, you should see the word Lean 4 in the Emacs mode line when you open a file with extension .lean. Emacs will ask you to identify the “project” this file belongs to. If you then type
#check id
the word #check will be underlined, and hovering over it will show you the type of id. The mode line will show FlyC:0/1, indicating that there are no errors and one piece of information displayed.
Set these with e.g. M-x customize-variable.
lsp-headerline-breadcrumb-enable: show a “breadcrumb bar” of namespaces and sections surrounding the current location (default: off)| Key | Function |
|---|---|
| C-c C-k | show the keystroke needed to input the symbol under the cursor |
| C-c C-d | recompile & reload imports (lean4-refresh-file-dependencies) |
| C-c C-x | execute Lean in stand-alone mode (lean4-std-exe) |
| C-c C-i | toggle info view showing goals and errors at point (lean4-toggle-info-buffer) |
| C-c ! n | flycheck: go to next error |
| C-c ! p | flycheck: go to previous error |
For lsp-mode bindings, see https://emacs-lsp.github.io/lsp-mode/page/keybindings/ (not all capabilities are supported currently).
In the default configuration, the Flycheck annotation FlyC:n/n indicates the number of errors / responses from Lean; clicking on FlyC opens the Flycheck menu.