elan-init
« Back to VersTracker
Description:
Lean Theorem Prover installer and version manager
Type: Formula  |  Latest Version: 4.1.2@0  |  Tracked Since: Dec 17, 2025
Links: Homepage  |  @leanprover  |  formulae.brew.sh
Category: Developer tools
Tags: lean theorem-prover version-manager installer mathematics
Install: brew install elan-init
About:
elan-init is a toolchain installer and version manager specifically for the Lean Theorem Prover. It allows users to easily install, manage, and switch between multiple versions of Lean on a single machine. This is essential for developers working on different Lean projects that may require specific compiler versions.
Key Features:
  • Automatic installation of Lean toolchains
  • Easy switching between multiple Lean versions
  • Management of default toolchains per project
  • Self-updating capabilities
Use Cases:
  • Setting up a new Lean development environment
  • Maintaining compatibility with legacy Lean projects
  • Testing Lean code across different compiler versions
Alternatives:
  • rustup – Similar functionality for Rust; elan is the direct equivalent for the Lean ecosystem
License: Apache-2.0 OR MIT
Dependencies: coreutils, gmp
Bottles available for: arm64_tahoe, arm64_sequoia, arm64_sonoma, arm64_ventura, sonoma, ventura, arm64_linux, x86_64_linux
Version History
Detected Version Rev Change Commit
Sep 13, 2025 4:42pm 0 VERSION_BUMP fcee862c
Dec 26, 2024 2:24pm 0 VERSION_BUMP 9e95a9e8
Nov 25, 2024 9:13am 0 VERSION_BUMP f3654be9
Nov 19, 2024 12:37am 0 VERSION_BUMP a13a017f
Sep 12, 2024 5:51pm 0 VERSION_BUMP 9c8e2516