Note that (require 'lean4-mode) is not necessary when the user

December 2, 2024 ยท View on GitHub

#+title: Lean4-Mode - Emacs major mode for Lean language #+language: en #+export_file_name: lean4-mode.texi #+texinfo_dir_category: Emacs misc features #+texinfo_dir_title: Lean4-Mode: (lean4-mode). #+texinfo_dir_desc: Emacs major mode for Lean language

This package extends [[https://www.gnu.org/software/emacs/][GNU Emacs]] by providing a major mode for editing code written in version 4 of the programming language and theorem prover [[https://lean-lang.org][Lean]].

The Lean4-Mode source code is developed at [[https://github.com/leanprover-community/lean4-mode][Github]] and its issues tracked there too. Further discussions and question-answering takes place in the [[https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs][#Emacs channel]] of Lean's Zulip chat.

For legacy version 3 of Lean, use the archived [[https://github.com/leanprover/lean3-mode][Lean3-Mode]] (also known as /Lean-Mode/).

  • Installation

** Brief and Generic Instructions

First, install the dependencies of Lean4-Mode:

Second, install Lean4-Mode itself:

Note that (require 'lean4-mode) is not necessary when the user

relies on autoloading and uses the default settings.

** 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 [[https://elpa.gnu.org][GNU Elpa]] package-archive. You can install the remaining packages either from source or from [[https://melpa.org/#/getting-started][Melpa]] package-archive. For later approach, add the following to your Emacs initialization file (e.g. =~/.emacs.d/init.el=):

#+begin_src elisp (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) #+end_src

Clone the Git repository of Lean4-Mode:

#+begin_src shell git clone https://github.com/leanprover-community/lean4-mode.git ~/path/to/lean4-mode #+end_src

In your Emacs initialization file, add the path to your local Lean4-Mode repository to the load-path list: #+begin_src elisp (add-to-list 'load-path "~/path/to/lean4-mode") #+end_src

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: #+begin_src elisp (require 'lean4-mode) #+end_src

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

#+begin_src elisp (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 )) #+end_src

*** Doom-Emacs

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

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

*** Straight

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

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

  • 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 [[https://emacs-lsp.github.io/lsp-mode/page/keybindings/][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 [[https://github.com/leanprover/lean3-mode][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.