lean4-htt/src/emacs

This is the emacs mode for the Lean theorem prover.

Quick-start

If you have built lean from source, all that is necessary is to call the leanemacs_build script which automatically installs all the dependencies and opens up emacs with lean-mode loaded:

~/projects/lean/bin/leanemacs_build

If you have installed lean from a binary package, you can run leanemacs.

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 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.

Key Bindings and Commands

Key	Function
M-.	jump to definition in source file (lean-find-definition)
TAB	tab complete identifier, option, filename, etc. (lean-tab-indent-or-complete)
C-c C-k	shows the keystroke needed to input the symbol under the cursor
C-c C-g	show goal in tactic proof (lean-show-goal-at-pos)
C-c C-x	execute lean in stand-alone mode (lean-std-exe)
C-c C-n	toggle next-error-mode: shows next error in dedicated lean-info buffer
C-c C-r	restart the lean server
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.

Requirements

lean-mode requires Emacs 24 or later and the following packages, which can be installed via M-x package-install: dash, dash-functional, f, s, company, flycheck, and fill-column-indicator.

Installation

You can also include lean-mode permanently in your emacs init file. In this case, just put the following code in your Emacs init file:

;; You need to modify the following two lines:
(setq lean-rootdir "~/projects/lean")
(setq lean-emacs-path "~/projects/lean/src/emacs")

(setq lean-required-packages '(company dash dash-functional f
                               flycheck let-alist s seq))

(require 'package)
(add-to-list 'package-archives '("melpa" . "http://melpa.org/packages/"))
(package-initialize)
(let ((need-to-refresh t))
  (dolist (p lean-mode-required-packages)
    (when (not (package-installed-p p))
      (when need-to-refresh
        (package-refresh-contents)
        (setq need-to-refresh nil))
      (package-install p))))

(setq load-path (cons lean-emacs-path load-path))

(require 'lean-mode)

If you already have the dependencies installed, the following three lines suffice:

;; You need to modify the following two lines:
(setq lean-rootdir "~/projects/lean")
(setq load-path (cons "~/projects/lean/src/emacs" load-path))
(require 'lean-mode)

Known Issues and Possible Solutions

Unicode

If you experience a problem rendering unicode symbols on emacs, please download the following fonts and install them on your machine:

• Quivira.ttf
• Dejavu Fonts
• NotoSans
• NotoSansSymbols

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 emacs-unicode-fonts package.

• Run M-x package-refresh-contents, M-x package-install, and type unicode-fonts.

• Add the following lines in your emacs setup:

(require 'unicode-fonts) (unicode-fonts-setup)

"Variable binding depth exceeds max-specpdl-size" Error
---------------------------------------------------------

See [Issue 906](https://github.com/leanprover/lean/issues/906) for details.
[Moritz Kiefer](https://github.com/cocreature) reported that `proofgeneral`
comes with an old version of `mmm-mode` (0.4.8, released in 2004) on ArchLinux
and it caused this problem. Either removing `proofgeneral` or upgrading
`mmm-mode` to the latest version (0.5.1 as of 2015 Dec) resolves this issue.

Contributions
=============

Contributions are welcome!

Install [Cask](https://github.com/cask/cask) if you haven't already, then:

 $ cd /path/to/lean/src/emacs
 $ cask

Run all tests with:

 $ make