lean4-htt/lean4-mode

Installation

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 dash-functional f flycheck 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)

Trying It Out

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. 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
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 C-n	toggle showing next error in dedicated buffer (lean-toggle-next-error)
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.