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:

PROJDIR/leanpkg.toml:
```
[package]
name = "test"
version = "0.1"
lean_version = "leanprover/lean4:nightly-2021-05-28"
```
In lean_version, substitute the date of the Lean nightly you want to use. There is also a stable toolchain, but at the time of writing it is horribly outdated.

PROJDIR/Test/Util.lean:

def someNumber : Nat := 42

#check someNumber

PROJDIR/Test.lean:
```
import Test.Util

def main : IO Unit := do
  print someNumber
```
This is the main file of your application/library. If a main function 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.Util etc. Note that there may only be one .lean file in PROJDIR; other .lean files have to go into Test/.

Now run the following commands:

leanpkg configure

This should download and install the Lean 4 nightly specified in leanpkg.toml. The installation directory is ~/.elan/toolchains/.
leanpkg build

This builds one .olean file for each of your .lean files.
leanpkg build bin

This builds the binary build/bin/Test, which you can run to print 42.
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.

3.3 Spacemacs

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

(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 PROJDIR. The #check line should be underlined and if you hover over it, you should get an overlay with the type of someNumber. 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.