Lean elan

ID

elan

Link

Repository

Upstream stars

⭐ 648

Last commit

2026-08-26

Version requirement

>= 4

Platforms

🐧 Linux · 🍎 macOS · 🪟 Windows

Operations

installed · orphans · install · remove · cleanup

purl types

pkg:elan/

CLI name

elan

Issues and PRs

📦 manager: elan

Source

elan.toml

elan is the version manager for the Lean theorem prover (https://github.com/leanprover/elan), installing the toolchains published at https://github.com/leanprover/lean4.

A package is a toolchain, every verb taking exactly one and the listing printing one per line, which is the reading rustup settled for this whole family. elan is in fact a rustup fork, so much of its shape carries over, but the parsers below do not: see the sentinel note.

Parsing notes, verified against elan 4.2.3 on macOS, driving Lean 4.33.0:

• No installed_version is captured, following pyenv, rustup and bob. A toolchain name is the identity rather than a version field, and the listing resolves stable to a concrete leanprover/lean4:v4.33.0, so the version is already inside the id. The only place a Lean version appears on its own is elan show, which reports the active toolchain alone and so answers for ambient state rather than for the machine.

• The sentinel is rejected differently than in rustup, and the difference matters. Both print no installed toolchains when empty, and rustup drops it by requiring an embedded hyphen in the id. elan’s names need not carry one, stable being a legal toolchain, so that test would silently drop real packages here. Anchoring both ends is what rejects the sentinel instead, its three words failing a single-token match.

• Unlike rustup, elan toolchain list marks nothing: a default toolchain renders exactly like any other, the (default) suffix appearing only in elan show. Nothing has to be stripped from the id.

• elan toolchain gc reports the toolchains no known project references and --delete removes them, which is a read-only orphan query and its collection in one verb pair. Its rows are - <toolchain>; the Known projects: block that follows renders as - default toolchain: <toolchain>, so anchoring the end is what tells the two apart. Both states were reproduced before the pattern was written.

• No outdated, no search and no upgrade. elan update is refused outright as an unrecognized argument, elan publishes no catalog of available toolchains, and elan self update replaces elan itself rather than a package, so it is deliberately not wired to anything.

Caution

Upstream calls the garbage collector experimental, having merged it as such in leanprover/elan#130, so the two operations resting on it are the ones to re-check first if its output moves.

No logo: Simple Icons carries no mark for Lean, so the manager page keeps its default package glyph rather than borrowing an unrelated one.

No escalation: elan installs under $ELAN_HOME, falling back to ~/.elan.

What mpm adds to elan

mpm reaches across every manager at once, not elan alone: mpm installed and mpm outdated cover elan alongside every other manager you run in one table, mpm upgrade --all updates them together, and mpm sbom exports the whole machine as one bill of materials.

Every mpm command also gains --dry-run and --plan previews, cross-scheme version comparison and purl identifiers. See manager augmentations for how each one is built.

Your elan commands, in mpm

You already know elan: each operation maps one-to-one onto mpm, in an interface shared by every manager.

To…	With elan	With mpm
List what’s installed	elan toolchain list	mpm --elan installed
Install a package	elan toolchain install <package_id>	mpm install pkg:elan/<package_id>
Remove a package	elan toolchain uninstall <package_id>	mpm remove pkg:elan/<package_id>
List orphaned dependencies	elan toolchain gc	mpm --elan orphans

Prefix any command above with --dry-run to simulate the underlying manager calls without touching the system: the safe way to watch what mpm would do before trusting it.

Operations

Operation	Supported	Notes
installed	✅
outdated
orphans	✅
search
install	✅
upgrade
upgrade_all
remove	✅
sync
cleanup	✅	The --orphans flag runs the system-wide orphan sweep.
doctor

Configuration

• Ignore elan on the mpm CLI by passing the --no-elan option.

• Ignore it for every run in your configuration:

  [mpm]
  elan = false
  

• Raise the timeout of all elan calls:

  [mpm.overrides.elan]
  timeout = 900
  

• Run mpm config-template elan to print all overridable settings for your configuration file:

  [mpm.overrides.elan]
  cli_names = [
      "elan",
  ]
  cli_search_path = []
  dry_run = false
  ignore_auto_updates = true
  plan = false
  post_args = []
  pre_args = []
  pre_cmds = []
  requirement = ">=4.0.0"
  stop_on_error = false
  unmaintained = false
  version_cli_options = [
      "--version",
  ]
  version_regexes = [
      "^elan (?P<version>\\S+)",
  ]
  

Recipes

A few jobs you would otherwise script around elan, one mpm command each:

• Snapshot and clone a machine: mpm --elan dump elan.toml, then mpm restore elan.toml on the next one.

• Export a compliance SBOM: mpm --elan sbom (CycloneDX by default, --spdx for SPDX).

Privilege escalation

mpm runs this manager as the current user and never prepends sudo by default. Flip the policy for its privileged operations with --sudo or the per-manager sudo override.

None of its operations is privileged.

See privilege escalation for the full policy.

Cooldown

State of Lean elan’s release-age gating, from the cooldown support table:

Status: ❌ None (installs Lean’s own GitHub releases)

A cooldown only pays off where a compromised release can be withdrawn while the clock runs, and can only be emulated where the registry dates its releases. From the retraction table:

• Registry: GitHub release assets

• Retraction: None: withdrawing a build is the upstream author deleting their own release or tag. Nothing sits between them and the user

• Publish date: ✅ server-set published_at on each release (REST API)

With --cooldown set, mpm skips this manager’s install and upgrade operations rather than run them unguarded (fail-closed); --cooldown best-effort opts back in.

Reference traces

A collection of raw native outputs captured from the manager’s own CLI and recorded in the bundled definition. If you know Lean elan well and a transcript below looks wrong, or a newer release changed its output format, report it.

$ elan toolchain list
leanprover/lean4:v4.33.0

$ elan toolchain gc
The following toolchains are not used by any known project; rerun with `--delete` to delete them:
- leanprover/lean4:v4.33.0
Known projects:

Version check

The version is probed by running:

$ elan --version
elan 4.2.3 ( )

and extracted with:

r"^elan (?P<version>\S+)"

Upstream project

Metrics	leanprover/elan
Activity
Popularity
Metadata

Changelog

• 8.0.0 (2026-09-20)

  • Add the elan Lean toolchain manager with installed, install, remove, orphans and cleanup support, a toolchain name being what it calls a package.