elan picks the Lean toolchain your project asks for

The toolchain file decides, not you

The problem elan solves is that Lean 4 moves fast, with nightly releases changing underneath you, and a project pins the exact version it needs. elan is described as a small tool for managing your installations of the Lean theorem prover, and it places the lean and lake binaries in your PATH so they automatically select, and if necessary download, the Lean version described in your project's lean-toolchain file. The README's opening example shows the whole loop: a project directory contains a lean-toolchain file naming a nightly, running lake --version triggers a download and install of the component, and elan show then lists the installed toolchains and names the active one as overridden by that file's path. The override is the point. The toolchain file is authoritative, and elan is the mechanism that makes a checkout build with the version its author intended.

The same tool also drives manual version management

The automatic selection is only half of it. The README says you can also install, select, run and uninstall Lean versions manually using the commands of the elan executable, and the example output shows the shape of the command surface with an installed toolchains list and an active toolchain section. That is a deliberate inheritance from rustup, which elan is a fork of, and it means a developer who wants to pin a project to something other than what its file says can override the default, and a developer who has several toolchains installed can list them and see which one is live. The default toolchain concept from rustup carries over, so the nightly entry in the example is the fallback used when no project file applies. A team that keeps a long-lived branch pinned to an old nightly and a development branch on a recent one gets both behaviours from one tool, which is the practical argument for elan over installing Lean by hand.

Installation is one shell command, or a downloaded binary

There are three documented ways in, and the first is a single command on Unix-like systems:

curl https://elan.lean-lang.org/elan-init.sh -sSf | sh

@@C1@@The Windows route is a three-command sequence in Command Prompt or in PowerShell 7.4.1 or later, which downloads a PowerShell script, runs it with the execution policy bypassed and then deletes the script.

curl -O --location https://elan.lean-lang.org/elan-init.ps1
powershell -ExecutionPolicy Bypass -f elan-init.ps1
del elan-init.ps1

The third option applies on any supported platform, which is to grab the latest release for your platform from the GitHub releases page, unpack it and run the installation program it contains. The installer tells you where it will install elan, at ~/.elan by default, and asks whether it may edit your shell config to extend PATH. That last part is the decision worth making deliberately, since it is what makes the tool available in new shells. The README also says elan can be uninstalled with elan self uninstall, which should revert those changes.

NixOS gets a patched version, and git is a real prerequisite

Two platform caveats are stated plainly. On NixOS, the README says the toolchains downloaded by elan require some patching, which is done automatically by the version available in Nixpkgs, so the install is a single nix-env invocation and the patching is somebody else's problem. The second is a genuine prerequisite that catches people out: on some systems lake will not work out of the box even if installed through elan, because you need git to download dependencies through lake. That is a small requirement, but it is stated as a prerequisite rather than assumed, and the consequence of missing it is a confusing failure at the first build rather than at the install. It is worth noting that elan itself downloads and installs the Lean toolchain components, so the network dependency is real, and a first lake invocation on a fresh machine will pull a large download.

It is rustup with the names swapped

The implementation section is short and unusually honest about what this project is. elan is basically a fork of rustup, and apart from new features and adaptions to the Lean infrastructure, the changes to the original code are listed in three items. Every mention of rustup was replaced with elan, cargo with lake, and rust and rustc with lean. CARGO_HOME and RUSTUP_HOME were merged into one directory, so there is a single home for the installed toolchains. And the options to configure the host triple were removed, which is right for a language that does not have the same cross-compilation story Rust does. The consequence for a reader is that the documentation for rustup is largely applicable, and that the differences from rustup are in the command surface and in what gets downloaded, not in the architecture. It also means elan inherits rustup's behaviour around channels, defaults and overrides, which is a large part of why it is dependable.

Building elan itself needs Rust, and Windows needs a careful perl

The build section is for contributors rather than users. Building from source requires Rust and Cargo, and the build itself is a cargo build, after which the elan-init installer appears in target/debug. The README notes that this is also the main elan executable, and suggests linking it to elan so you can test it, then running elan --help.

ln -s ./target/debug/elan-init ./elan

On Windows the equivalent is creating a hard link to the built executable. The Windows build has two specific requirements that are easy to miss. It needs a 64-bit developer command prompt, and it needs a Windows build of perl.exe, which the README says you can download from Strawberry Perl, with the instruction that the downloaded perl.exe must be first on your PATH so the build does not pick up the copy that ships with Git under Program Files, because the Git-provided version does not work for the build. The repository root holds the two installer scripts, a build.rs, a flake.nix and flake.lock for Nix builds, a fetch_nixos_patch.sh script, a Cross.toml for cross compilation, a release.toml and both licence files.

Editorial conclusion

elan suits a Lean developer working across several projects pinned to different nightly releases, or a contributor who needs to reproduce a specific commit's toolchain, and it suits a Windows user who accepts a slightly fussier setup. It does not suit a team that wants one global Lean install with no per-project switching, since the whole design is that the toolchain file wins. Before adopting, install it with the shell installer on Unix-like systems and check that git is present, because the README says lake will not work out of the box without it, and note that the last push to the repository was on 2026-10-10 with v4.2.4 from 2026-08-25 under a dual MIT and Apache-2.0 licence.

Frequently asked questions

Official sources

1. Issues
2. leanprover/elan on GitHub
3. License: Apache-2.0
4. README
5. Releases