Lean4-Mode - Emacs major mode for Lean language

This package extends GNU Emacs by providing a major mode for editing code written in version 4 of the programming language and theorem prover Lean.

The Lean4-Mode source code is developed at Github and its issues tracked there too. Further discussions and question-answering takes place in the #Emacs channel of Lean’s Zulip chat.

For legacy version 3 of Lean, use the archived Lean3-Mode (also known as Lean-Mode).

Installation

Brief and Generic Instructions

First, install the dependencies of Lean4-Mode:

• Lean (version 4)
• Emacs (version 27 or later)
• Emacs packages Dash (available on GNU-Elpa), lsp-mode, and Magit-Section (available on Melpa)

Second, install Lean4-Mode itself:

• Clone the Git repository of Lean4-Mode.
• In your Emacs initialization file, add the path to that local repository to the load-path list.

Detailed and Concrete Instructions

Install Lean version 4.

Install Emacs version 27 or later.

Install the Emacs packages Dash, lsp-mode and Magit-Section. Dash is the only one of these packages that is available in the default GNU Elpa package-archive. You can install the remaining packages either from source or from Melpa package-archive. For later approach, add the following to your Emacs initialization file (e.g. ~/.emacs.d/init.el):

(require 'package)

(add-to-list 'package-archives
             '("melpa" . "https://melpa.org/packages/"))

(add-to-list 'package-selected-packages 'dash)
(add-to-list 'package-selected-packages 'lsp-mode)
(add-to-list 'package-selected-packages 'magit-section)

(package-refresh-contents)
(package-install-selected-packages 'no-confirm)

Clone the Git repository of Lean4-Mode:

git clone https://github.com/leanprover-community/lean4-mode.git ~/path/to/lean4-mode

In your Emacs initialization file, add the path to your local Lean4-Mode repository to the load-path list:

(add-to-list 'load-path "~/path/to/lean4-mode")

Lean4-Mode should now already be enabled when you open a file with .lean extension. But you can optionally also already load Lean4-Mode on Emacs startup, e.g. in order to customize variables:

(require 'lean4-mode)

Instructions for Source-Based Use-Package

If you use a source-based package-manager (e.g. package-vc.el, Straight or Elpaca), then make sure to list the "data" directory in your Lean4-Mode package recipe.

If you use the use-package macro and intent to defer loading of packages in order to improve your Emacs startup time, then make sure to specify lean4-mode as a :command.

Following subsections show concrete examples.

Native :vc (Emacs 30 or later)

GNU Emacs comes with use-package.el built-in since version 29. And since version 30, it also comes with a built-in :vc keyword for the use-package macro that utilizes package-vc.el to install Emacs packages from remote source repositories.

(require 'package)
(add-to-list 'package-archives
             '("melpa" . "https://melpa.org/packages/"))
(package-initialize)

(use-package lean4-mode
  :commands lean4-mode
  :vc (:url "https://github.com/leanprover-community/lean4-mode.git"
       :rev :last-release
       ;; Or, if you prefer the bleeding edge version of Lean4-Mode:
       ;; :rev :newest
       ))

Doom-Emacs

If you use Doom-Emacs, you can place the following code in your Doom initialization file:

(package! lean4-mode
  :recipe (:host github
           :repo "leanprover-community/lean4-mode"
           :files ("*.el" "data")))

Straight

If you use the Straight package manager through Use-Package, then place the following code in your Emacs initialization file:

(use-package lean4-mode
  :commands lean4-mode
  :straight (lean4-mode :type git :host github
                        :repo "leanprover-community/lean4-mode"
                        :files ("*.el" "data")))

Usage

If things are working correctly, you should see the word “Lean 4” in Emacs mode-line when you open a file with .lean extension. 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.

To view the proof state, run lean4-toggle-info (C-c C-i). This will display the *Lean Goals* buffer (like the Lean Info-View pane in VS-Code) in a separate window.

Key	Description	Command
C-c C-k	Echo the keystroke needed to input the symbol at point	quail-show-key
C-c C-d	Recompile and reload imports	lean4-refresh-file-dependencies
C-c C-x or C-c C-l	Execute Lean in stand-alone mode	lean4-std-exe
C-c C-p C-l	Builds package with lake	lean4-lake-build
C-c C-i	Toggle Info-View which shows goals and errors at point	lean4-toggle-info-buffer

lsp-mode

For key bindings from lsp-mode, see its respective documentation and note that not all capabilities are supported by Lean4-Mode.

Flycheck

You may optionally use Lean4-Mode together with Flycheck. In that case, the mode-line will show FlyC:E/N, indicating that there are E number of errors and N number of notes. Following keys will be available by default (via flycheck-mode-map):

Key	Description	Command
C-c ! n	Go to next error	flycheck-next-error
C-c ! p	Go to previous error	flycheck-previous-error

Configuration

lsp-mode

If you want breadcrumbs of namespaces and sections to be shown in the header-line, set the user option lsp-headerline-breadcrumb-enable to t.

Flycheck

Flycheck is an optional but supported dependency of Lean4-Mode. If Flycheck is installed, lsp-mode and thus Lean4-Mode will by default use it. If you want to customize this behavior, e.g. if you’d like to use Emacs’ built-in Flymake package instead of Flycheck while keeping later installed, then customize the lsp-diagnostics-provider user option accordingly.

Common Pitfalls

Lean4-Mode only supports version 4 of Lean. For editing Lean version 3, use Lean3-Mode, which is also known as Lean-Mode due to historical reasons. In principle, it is fine to have both Lean3-Mode and Lean4-Mode installed at the same time. But note that Lean3-Mode uses the prefix lean- for its symbols. E.g. you should not use lean--prefixed commands in a buffer with Lean4-Mode as major mode.