elan is a small tool for managing your installations of the Lean
theorem prover. It places lean and lake binaries in your PATH that
automatically select and, if necessary, download the Lean version
described in your project's lean-toolchain file. You can also install,
select, run, and uninstall Lean versions manually using the commands
of the elan executable.
elan is basically a fork of rustup. Apart from new features and
adaptions to the Lean infrastructure, these are the basic changes to
the original code:
Replaced every mention of rustup with elan, cargo with lake, and
rust(c) with lean Merged CARGO_HOME and RUSTUP_HOME Removed options to
configure host triple
Note: elan is one of the ways to manage Lean toolchains. The SB author
cannot guarantee that it is the best one. Learning on the experience
of other GNU/Linux distributions, it might be reasonable to have other
packages from the lean-* package family in the future.