elan

elan manages installations of the Lean theorem prover for Linux, macOS, and Windows. Its `lean` and `lake` commands can read a project’s `lean-toolchain` file, select the specified Lean version, and download it when needed. The `elan` command also lets users install, select, run, or uninstall Lean versions manually. It supports project version pinning, lockfiles, automatic switching, shell integration, and CI/CD usage. Installation instructions include shell methods for Linux and macOS, a PowerShell method for Windows, and release downloads for supported platforms. On NixOS, the README recommends using the Nixpkgs version because toolchains downloaded by elan require patching there. Lake needs git to download dependencies. The project describes elan as a rustup fork adapted for Lean infrastructure. It is free and lists Apache-2.0 and MIT licenses; the latest release listed is v4.2.4. The README says the self-uninstall command removes elan and reverses shell configuration changes made during installation.

elan handles Lean version selection both from project configuration and through manual commands. NixOS users should follow the README’s Nixpkgs recommendation, and Lake dependency downloads require git.

elan suits Lean users who want project-specific toolchain selection or manual version management. It may also suit teams using pinned toolchains in CI/CD.