Lean elan

ID

elan

Home page

https://github.com/leanprover/elan

Upstream stars

⭐ 598

Last commit

2026-07-16

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

meta_package_manager/managers/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	✓	--orphans runs the system-wide orphan sweep
doctor

Selecting and configuring elan

Deselect elan for a single run with --no-elan, or persist the choice in your configuration:

[mpm]
elan = false

Keep it enabled but tune how mpm drives it with a per-manager override:

[mpm.managers.elan]
timeout = 900

mpm config-template elan prints every overridable attribute as a ready-to-paste block.

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 needs root.

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.

Version probe

The version is probed by running:

$ elan --version
elan 4.2.3 ( )

and extracted with:

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

Reference traces

Raw native outputs captured in the bundled definition: the reference mpm’s parsers were written against. 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:

Feed any of these through mpm and the raw output becomes one uniform table, the same shape for every manager: filter it, project columns, or export it (mpm --elan installed --output json, or csv, toml, yaml), each package carrying a purl and a version comparable across managers.

Upstream project

Metrics	leanprover/elan
Activity
Popularity
Metadata

Changelog

• 8.0.0.dev0 (unreleased)

  • Add elan as a bundled definition, with installed, install, remove, orphans and cleanup support. It manages Lean toolchains, so a toolchain name is what it calls a package, and no version is reported beside it, the listing resolving a channel to a concrete name that already carries one. elan toolchain gc reports the toolchains no project references and --delete collects them, which is a read-only orphan query and its cleanup in one verb pair.