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.