I just started a new project in Lean 4. Since this is a very work-in-progress language with patchy documentation, I wanted to sketch one way to set up a project with working compilation and editor support. This is mostly for my future self, but maybe it’ll help others as well. Note that if you read this article long after June 2021, the instructions are likely outdated.
1 Elan Setup
Install elan. This is a little program that automatically fetches and installs the correct version of Lean for your project. You don’t need to select a default toolchain during installation. Type
elan --version to verify that the installation was successful.
2 Project Setup
Create an empty project directory,
PROJDIR. In it, create the following files:
[package] name = "test" version = "0.1" lean_version = "leanprover/lean4:nightly-2021-05-28"
lean_version, substitute the date of the Lean nightly you want to use. There is also a
stabletoolchain, but at the time of writing it is horribly outdated.
def someNumber : Nat := 42 #check someNumber
import Test.Util def main : IO Unit := do print someNumber
This is the main file of your application/library. If a
mainfunction is defined here, it becomes the entry point of your application. Other Lean projects which depend on this project can import this file with
import Test, and your other files with
import Test.Utiletc. Note that there may only be one
.leanfiles have to go into
Now run the following commands:
This should download and install the Lean 4 nightly specified in
leanpkg.toml. The installation directory is
This builds one
.oleanfile for each of your
leanpkg build bin
This builds the binary
build/bin/Test, which you can run to print
leanpkg build lib
This builds the library
build/lib/libTest.a, which you can link to when building the binary of a dependent Lean project. See
leanpkg help build.
3 Editor Setup
3.1 All Editors
Go to the installation directory of your Lean 4 toolchain. In this example, that’s
~/.elan/toolchains/leanprover--lean4---nightly-2021-05-28/. Then type
elan override set leanprover/lean4:nightly-2021-05-28
This tells elan to use the specified Lean version for Lean files in this directory. You can verify this with
elan show. The Lean files in this directory (specifically in
lib/lean/src) are the standard library for this Lean version, so when we use go-to-definition later, we may end up here.
You’ll have to repeat this process for every toolchain you install. If I was less lazy, I’d implement an auto-detection mechanism for this in elan.
3.2 Visual Studio Code
Install the Lean 4 extension. If you then open the project, everything should work out of the box. I don’t use VSCode, so that’s all I can tell you.
I do use Spacemacs, so I can give more helpful instructions here. If you use a different Emacs flavour, you’ll hopefully be able to figure out equivalent commands.
Add the following to
dotspacemacs-additional-packages in your
(lean4-mode :location (recipe :fetcher github :repo "leanprover/lean4" :files ("lean4-mode/*.el"))) dash dash-functional flycheck lsp-mode f s
The first line instructs Spacemacs to get
lean4-mode from the Lean 4 repository. The other lines are MELPA packages which
lean4-mode depends on.
Now restart Spacemacs to install these packages, then open
PROJDIR/Test/Util.lean. If Spacemacs asks you to specify a project root, give
#check line should be underlined and if you hover over it, you should get an overlay with the type of
lean4-mode is built on the language server protocol, so you can use many of the familiar LSP commands. Errors in your Lean files should show up in the Flycheck buffer (
SPC e l).
You should also be able to go to the definition of
Nat by positioning your cursor over
Nat and typing
<leader> m g d. This should lead you to
~/.elan/toolchains/leanprover--lean4---nightly-2021-05-28/.../Prelude.lean. If LSP asks you for a project root again, choose
~/.elan/toolchains/leanprover--lean4---nightly-2021-05-28/lib/lean/src. (If your
.elan directory is a symlink, LSP may get confused and ask for a project root multiple times.)
Go-to-definition should also work here. If your status bar says that LSP is “starting” forever, you probably haven’t set the correct
elan override for this directory; see the
All Editors section.
If you have the Emacs package for Lean 3,
lean-mode, installed as well, the two modes may fight over which one gets to open
.lean files. I haven’t found a good solution for this yet. The cumbersome solution is to manually specify the major mode (
SPC h M) whenever Emacs picks the wrong one.
I got some errors from
lean4-mode when I did not have a default toolchain selected. If you run into this, type
elan default leanprover/lean4:nightly-2021-05-28
to set a default toolchain.