elan-init
brew install elan-init
v4.2.3
Apache-2.0 OR MIT
Lean Theorem Prover installer and version manager
484
30-day installs · #1782
775
90-day · #2446
1.8k
365-day · #2927
548
★ GitHub stars · updated 2mo ago
Runtime dependencies
Build dependencies
Links
- https://github.com/leanprover/elan
- GitHub: leanprover/elan
- Brew formula source: Formula/e/elan-init.rb
Raw metadata
{
"aliases": [
"elan"
],
"alternatives": [],
"build_dependencies": [
"pkgconf",
"rust"
],
"categories": [],
"caveats": null,
"conflicts_with": [
"lean-cli"
],
"dependencies": [
"coreutils",
"gmp"
],
"deprecated": 0,
"deprecation_reason": null,
"desc": "Lean Theorem Prover installer and version manager",
"disable_reason": null,
"disabled": 0,
"enrichment_fetched_at": "2026-06-20T23:37:16+00:00",
"first_seen": "2026-06-20T23:34:18+00:00",
"full_name": "elan-init",
"github_default_branch": "master",
"github_last_commit_at": "2026-06-19T08:14:24Z",
"github_readme_excerpt": "# elan: Lean version manager\n\n*elan* is a small tool for managing your installations of the [Lean theorem prover](https://leanprover.github.io). It places `lean` and `lake` binaries in your `PATH` that automatically select and, if necessary, download the Lean version described in your project\u0027s `lean-toolchain` file.\nYou can also install, select, run, and uninstall Lean versions manually using the commands of the `elan` executable.\n\n```shell\n~/my/package $ cat lean-toolchain\nnightly-2023-06-27\n\n~/my/package $ lake --version\ninfo: downloading component \u0027lean\u0027\nTotal: 181.0 MiB Speed: 17.7 MiB/s\ninfo: installing component \u0027lean\u0027\nLake version 4.1.0-pre (Lean version 4.0.0-nightly-2023-06-27)\n\n~/my/package $ elan show\ninstalled toolchains\n--------------------\n\nnightly (default)\nnightly-2022-06-27\n\nactive toolchain\n----------------\n\nnightly-2023-06-27 (overridden by \u0027/home/me/my/package/lean-toolchain\u0027)\nLean (version 4.0.0-nightly-2023-06-27, commit bb8cc08de85f, Release)\n```\n\n# Installation\n\n## Manual Installation\n\n**Linux/macOS/Cygwin/MSYS2/git bash/...**: run the following command in a terminal:\n\n```bash\ncurl https://elan.lean-lang.org/elan-init.sh -sSf | sh\n```\n\n**Windows**: run the following commands in a terminal (Command Prompt or PowerShell \u2265 version 7.4.1):\n```bash\ncurl -O --location https://elan.lean-lang.org/elan-init.ps1\npowershell -ExecutionPolicy Bypass -f elan-init.ps1\ndel elan-init.ps1\n```\n\nAlternatively, on **any supported platform**: Grab the [latest release](https://github.com/leanprover/elan/releases/latest) for your platform, unpack it, and run the contained installation program.\n\nThe installation will tell you where it will install elan to (`~/.elan` by default), and also ask you about editing your shell config to extend `PATH`. elan can be uninstalled via `elan self uninstall`, which should revert these changes.\n\n## NixOS\n\nThe toolchains downloaded by elan require some patching on NixOS, which is done automatically by the version available in Nixpk",
"github_repo": "leanprover/elan",
"github_stars": 548,
"github_topics": [],
"homepage": "https://github.com/leanprover/elan",
"homepage_og_description": null,
"homepage_og_image": null,
"homepage_title": null,
"installs_30d": 484,
"installs_365d": 1845,
"installs_90d": 775,
"keg_only": 0,
"keg_only_reason": null,
"last_seen": "2026-06-20T23:34:18+00:00",
"license": "Apache-2.0 OR MIT",
"llm_generated_at": null,
"llm_model": null,
"name": "elan-init",
"oldnames": [],
"one_liner": null,
"optional_dependencies": [],
"rank_30d": 1782,
"rank_365d": 2927,
"rank_90d": 2446,
"raw_hash": "bf67358486330ee8",
"recommended_dependencies": [],
"revision": 0,
"ruby_source_path": "Formula/e/elan-init.rb",
"tap": "homebrew/core",
"test_dependencies": [],
"uses_from_macos": [
"bzip2",
"curl"
],
"version_head": "HEAD",
"version_stable": "4.2.3",
"versioned_formulae": [],
"why_use_this": null
}