Platforms built & tested by our CI, available as nightly & stable releases via elan (see above)
- x86-64 Linux with glibc 2.27+
- x86-64 macOS 10.15+
- x86-64 Windows 10+
Platforms cross-compiled but not tested by our CI, available as nightly & stable releases
Releases may be silently broken due to the lack of automated testing. Issue reports and fixes are welcome.
- aarch64 Linux with glibc 2.27+
- aarch64 (M1) macOS
Setting Up Lean
There are currently two ways to set up a Lean 4 development environment:
- basic setup (Linux/macOS/Windows): uses
elan+ your preinstalled editor
- Nix setup (Linux/macOS/WSL): uses the Nix package manager for installing all dependencies localized to your project
See also the quickstart instructions for using the basic setup with VS Code as the editor.
Release builds for all supported platforms are available at https://github.com/leanprover/lean4/releases.
Instead of downloading these and setting up the paths manually, however, it is recommended to use the Lean version manager
$ elan self update # in case you haven't updated elan in a while # download & activate latest Lean 4 release (https://github.com/leanprover/lean4/releases) $ elan default leanprover/lean4:stable # alternatively, use the latest nightly build (https://github.com/leanprover/lean4-nightly/releases) $ elan default leanprover/lean4:nightly # alternatively, activate Lean 4 in current directory only $ elan override set leanprover/lean4:stable
Lean 4 comes with a package manager named
lake init foo to initialize a Lean package
foo in the current directory, and
lake build to typecheck and build it as well as all its dependencies. Use
lake help to learn about further commands.
The general directory structure of a package
lakefile.lean # package configuration lean-toolchain # specifies the lean version to use Foo.lean # main file, import via `import Foo` Foo/ A.lean # further files, import via e.g. `import Foo.A` A/... # further nesting build/ # `lake` build output directory
lake build you will see a binary named
./build/bin/foo and when you run it you should see the output:
Lean implements the Language Server Protocol that can be used for interactive development in Emacs, VS Code, and possibly other editors.
Changes must be saved to be visible in other files, which must then be invalidated using an editor command (see links above).
The alternative setup based on Nix provides a perfectly reproducible development environment for your project from the Lean version down to the editor and Lean extension. However, it is still experimental and subject to change; in particular, it is heavily based on an unreleased version of Nix enabling Nix Flakes. The setup has been tested on NixOS, other Linux distributions, and macOS.
After installing (any version of) Nix (https://nixos.org/download.html), you can easily open a shell with the particular pre-release version of Nix needed by and tested with our setup (called the "Lean shell" from here on):
$ nix-shell https://github.com/leanprover/lean4/archive/master.tar.gz -A nix
While this shell is sufficient for executing the steps below, it is recommended to also set the following options in
nix.extraOptions in NixOS):
max-jobs = auto # Allow building multiple derivations in parallel keep-outputs = true # Do not garbage-collect build time-only dependencies (e.g. clang) # Allow fetching build results from the Lean Cachix cache trusted-substituters = https://lean4.cachix.org/ trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= lean4.cachix.org-1:mawtxSxcaiWE24xCXXgh3qnvlTkyU7evRRnGeAhD4Wk=
On a multi-user installation of Nix (the default), you need to restart the Nix daemon afterwards:
sudo pkill nix-daemon
The Cachix integration will magically beam any build steps already executed by the CI right onto your machine when calling Nix commands in the shell opened above. It can be set up analogously as a cache for your own project.
Note: Your system Nix might print warnings about not knowing some of the settings used by the Lean shell Nix, which can be ignored.
From a Lean shell, run
$ nix flake new mypkg -t github:leanprover/lean4
to create a new Lean package in directory
mypkg using the latest commit of Lean 4.
Such packages follow the same directory layout as described in the basic setup above, except for a
lakefile.lean replaced by a
flake.nix file set up so you can run Nix commands on it, for example:
$ nix build # build package and all dependencies $ nix build .#executable # compile `main` definition into executable (after you've added one) $ nix run .#emacs-dev # open a pinned version of Emacs with lean4-mode fully set up $ nix run .#emacs-dev MyPackage.lean # arguments can be passed as well, e.g. the file to open $ nix run .#vscode-dev MyPackage.lean # ditto, using VS Code
Note that if you rename
MyPackage.lean, you also have to adjust the
name attribute in
Also note that if you turn the package into a Git repository, only tracked files will be visible to Nix.
As in the basic setup, changes need to be saved to be visible in other files, which have then to be invalidated via an editor command.
If you don't want to or cannot start the pinned editor from Nix, e.g. because you're running Lean inside WSL/a container/on a different machine, you can manually point your editor at the
lean wrapper script the commands above use internally:
$ nix build .#lean-dev -o result-lean-dev
./result-lean-dev/bin/lean script essentially runs
nix run .#lean in the current project's root directory when you open a Lean file or use the "refresh dependencies" command such that the correct Lean version for that project is executed.
This includes selecting the correct stage of Lean (which it will compile on the fly, though without progress output) if you are working on Lean itself.
Package dependencies can be added as further input flakes and passed to the
deps list of
buildLeanPackage. Example: https://github.com/Kha/testpkg2/blob/master/flake.nix#L5
For hacking, it can be useful to temporarily override an input with a local checkout/different version of a dependency:
$ nix build --override-input somedep path/to/somedep
On a build error, Nix will show the last 10 lines of the output by default. You can pass
nix build to show all lines, or pass the shown
*.drv path to
nix log to show the full log after the fact.
Keeping all outputs ever built on a machine alive can accumulate to quite impressive amounts of disk space, so you might want to trigger the Nix GC when
/nix/store/ has grown too large:
This will remove everything not reachable from "GC roots" such as the
./result symlink created by
Note that the package information in
flake.nix is currently completely independent from
lakefile.lean used in the basic setup.
Unifying the two formats is TBD.