This is the Emacs mode for the Lean 3 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 ~/.emacs.d/init.el):
(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 lineSee also MELPA: Getting Started.
With MELPA configured, you can M-x package-install the packages lean-mode and 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.
For 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.
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 idthe 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.
| Key | Function |
|---|---|
| M-. | jump to definition in source file (lean-find-definition) |
| M-, | jump back to position before M-. (xref-pop-marker-stack) |
| 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 (lean-std-exe) |
| C-c SPC | run a command on the hole at point (lean-hole) |
| C-c C-d | show a searchable list of definitions (helm-lean-definitions) |
| C-c C-g | toggle showing current tactic proof goal (lean-toggle-show-goal) |
| C-c C-n | toggle showing next error in dedicated buffer (lean-toggle-next-error) |
| C-c C-b | toggle showing output in inline boxes (lean-message-boxes-toggle) |
| C-c C-r | restart the lean server (lean-server-restart) |
| C-c C-s | switch to a different Lean version via elan (lean-server-switch-version) |
| 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 check and print in boxes in the buffer, enable the feature using C-c C-b.
If you then type
#check ida box appears after the line showing the type of id. Customize 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.
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!
When working on lean-mode itself, it is much easier to just require the sources than repeatedly building the MELPA packages:
(add-to-list 'load-path "~/path/to/lean-mode/")
(require '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 package-initialize.