This is the Emacs mode for the Lean theorem prover.
lean-mode requires GNU Emacs 24.3 or newer. The recommended way to install it is via MELPA. If you have not already configured MELPA, put the following code in your Emacs init file (typically
(require 'package) ; You might already have this line (add-to-list 'package-archives '("melpa" . "http://melpa.org/packages/")) (package-initialize) ; You might already have this line
See also MELPA: Getting Started.
With MELPA configured, you can
M-x package-install the packages
company-lean. The latter package gives you auto completion and is strongly recommended. There is a third package,
helm-lean, which provides a searchable list of declarations on
C-c C-d using the Helm interface.
helm-lean requires Emacs 24.4 or newer.
company-lean, you should also bind a key to trigger completion, if you have not already done so:
;; Trigger completion on Shift-Space (global-set-key (kbd "S-SPC") #'company-complete)
For updating the Lean MELPA packages, use
package-list-packages. See the section "Updating Packages" on MELPA: Getting Started for details.
Trying It Out
If things are working correctly, you should see the word
Lean in the
Emacs mode line when you open a file with extension
.lean. If you type
#check will be underlined, and hovering over it will show
you the type of
id. The mode line will show
that there are no errors and one piece of information displayed.
Key Bindings and Commands
|M-.||jump to definition in source file (
|M-,||jump back to position before M-. (
|C-c C-k||shows the keystroke needed to input the symbol under the cursor|
|C-c C-x||execute lean in stand-alone mode (
|C-c SPC||run a command on the hole at point (
|C-c C-d||show a searchable list of definitions (
|C-c C-g||toggle showing current tactic proof goal (
|C-c C-n||toggle showing next error in dedicated buffer (
|C-c C-b||toggle showing output in inline boxes (
|C-c C-r||restart the lean server (
|C-c C-s||switch to a different Lean version via elan (
|C-c ! n||flycheck: go to next error|
|C-c ! p||flycheck: go to previous error|
|C-c ! l||flycheck: show list of errors|
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.
To view the output of commands such as
a box appears after the line showing the type of
lean-message-boxes-enabled-captions to choose categories of boxes.
In particular, add
"trace output" to the list to see proof states and other traces in the buffer.
Known Issues and Possible Solutions
If you experience a problem rendering unicode symbols on emacs, please download the following fonts and install them on your machine:
Then, have the following lines in your emacs setup to use
DejaVu Sans Mono font:
(when (member "DejaVu Sans Mono" (font-family-list)) (set-face-attribute 'default nil :font "DejaVu Sans Mono-11"))
You may also need to install the emacs-unicode-fonts package, after which you should add the following lines to your emacs setup:
(require 'unicode-fonts) (unicode-fonts-setup)
Contributions are welcome!
Building from Source
When working on
lean-mode itself, it is much easier to just
require the sources than repeatedly building the MELPA packages:
(add-to-load-path "~/path/to/lean-mode/") (require 'company-lean) (require 'helm-lean)
Make sure you have the packages' dependencies listed on MELPA installed -- the easiest way to do this may be to just install the official Lean MELPA packages and making sure the
require commands above are execute before