Lemma - A Modern Lean4 Toolchain Manager

English | 简体中文

Lemma is a rewrite of elan that addresses critical usability issues, particularly around proxy support and custom toolchain sources.

Why Lemma?

After analyzing the elan codebase, we identified several critical issues that make it difficult to use in enterprise and restricted network environments.

Key Features

Full Proxy Support

• HTTP, HTTPS, and SOCKS5 proxies with authentication
• Standard environment variables: HTTP_PROXY, HTTPS_PROXY, NO_PROXY

Custom Sources and Mirrors

Configure custom Lean release index URLs:

release_url = "https://release.custom.org"

For regional mirrors, especially in China, configure both the release index and the large release-asset prefix:

release_url = "https://mirror.example.com/lean-releases"
release_asset_url_prefix = "https://mirror.example.com"

release_url controls where Lemma fetches index.json. The asset prefix rewrites official archive URLs such as https://releases.lean-lang.org/lean4/v4.30.0/lean-4.30.0-linux.tar.zst to https://mirror.example.com/lean4/v4.30.0/lean-4.30.0-linux.tar.zst, so the large toolchain archive can also come from the mirror instead of redirecting to GitHub release assets.

Installation

The command-line executable is always named lemma, regardless of how you install it.

From PyPI (Recommended)

Install Lemma as a Python package named lemma-lean:

pipx install lemma-lean

If you do not use pipx, install with Python's user site instead:

python -m pip install --user lemma-lean

On Windows, use the Python launcher if needed:

py -m pip install --user lemma-lean

From crates.io

If you have a Rust toolchain installed, you can also install the lemma-rs crate, which provides the same lemma executable:

cargo install lemma-rs

After installation, run a setup command such as lemma toolchain install stable. Lemma will create proxy commands such as lean, lake, and leanc under ~/.lemma/bin. Add that directory to your PATH if you want to call those proxies directly.

From Source

# Build from source
cargo build --release -p lemma-rs

# Install the CLI from this checkout
cargo install --path crates/lemma-rs

Updating Lemma

Use the same package manager that installed Lemma:

pipx upgrade lemma-lean
# or
python -m pip install --user --upgrade lemma-lean
# or, for a crates.io install
cargo install lemma-rs

lemma self update prints these safe package-manager commands instead of replacing the running binary directly.

Usage

Basic Commands

# Install a Lean toolchain
lemma toolchain install stable
lemma toolchain install nightly
lemma toolchain install v4.0.0

# List toolchains
lemma toolchain list

# Set default toolchain
lemma default stable

# Upgrade installed channel toolchains
lemma toolchain upgrade

# Show active toolchain information
lemma show

# Self-management
lemma self update              # Show package-manager upgrade commands
lemma self uninstall           # Remove Lemma-managed toolchains and ~/.lemma data

Use lemma toolchain ... for all toolchain-management operations.

Configuration File

Lemma stores its configuration in ~/.lemma/lemma.toml (or $LEMMA_HOME/lemma.toml).

Example configuration:

version = "1"
default_toolchain = "leanprover/lean4:stable"
path_setup_shown = true
release_url = "https://release.lean-lang.org"
release_asset_url_prefix = "https://mirror.example.com"

[overrides]

Environment Variables

Lemma respects standard proxy environment variables:

• HTTP_PROXY / http_proxy - HTTP proxy URL
• HTTPS_PROXY / https_proxy - HTTPS proxy URL
• ALL_PROXY / all_proxy - Proxy for all protocols
• NO_PROXY / no_proxy - Comma-separated list of domains to bypass proxy
• LEMMA_HOME - Lemma home directory (default: ~/.lemma)
• LEMMA_RELEASE_URL - Override the Lean release index URL
• LEMMA_RELEASE_ASSET_URL_PREFIX - Rewrite Lean release archive URLs to a mirror prefix
• LEMMA_TOOLCHAIN - Override active toolchain for current session

Advanced Usage

Project-specific Toolchains

Lemma automatically detects project-specific toolchains from:

1. lean-toolchain file: Create a lean-toolchain file in your project root:

   stable
   

   or with full specification:

   leanprover/lean4:v4.25.0
   

2. leanpkg.toml: Specify lean_version in your package configuration:

   lean_version = "v4.25.0"
   

Directory Overrides

Set a toolchain for a specific directory and all subdirectories:

cd my-project
lemma override set stable

Remove the override:

lemma override unset

List all directory overrides:

lemma override list

Custom Lean Release Sources

Configure a custom Lean release index in ~/.lemma/lemma.toml:

release_url = "https://mirror.example.com/lean-releases"
release_asset_url_prefix = "https://mirror.example.com"

Or use environment variables:

export LEMMA_RELEASE_URL=https://mirror.example.com/lean-releases
export LEMMA_RELEASE_ASSET_URL_PREFIX=https://mirror.example.com

If your mirror only provides index.json, Lemma can list releases through the mirror but downloads may still follow the official asset URL to GitHub-backed release assets. Set release_asset_url_prefix when the mirror also hosts the toolchain archives under the same /lean4/<version>/<archive> path.

Toolchain Resolution

Lemma resolves which toolchain to use in the following priority order:

1. Explicit override: +toolchain syntax (e.g., lean +nightly test.lean)
2. Environment variable: LEMMA_TOOLCHAIN
3. Directory override: Set via lemma override set
4. Project file: lean-toolchain or leanpkg.toml in current directory or parent directories
5. Default toolchain: Configured via lemma default <toolchain>

Troubleshooting

Toolchain not found

If you see "Toolchain not installed" errors:

# List installed toolchains
lemma toolchain list

# Install the required toolchain
lemma toolchain install stable

Proxy connection issues

If downloads fail behind a proxy:

# Verify proxy settings
echo $HTTPS_PROXY

# Test with curl
curl -v https://release.lean-lang.org

# Set proxy for lemma
export HTTPS_PROXY=http://your-proxy:port

Command not found errors

If lemma is not found, ensure your Python package manager's scripts directory is on PATH (pipx ensurepath can help for pipx installs).

If lean, lake, or leanc are not found, ensure Lemma's proxy directory is on PATH:

export PATH="$HOME/.lemma/bin:$PATH"

Contributing

Contributions are welcome! Key areas that need work:

1. Toolchain Installation - Improve the download and install pipeline
2. Binary Proxying - Improve the toolchain binary wrapper system
3. Testing - Add comprehensive test coverage
4. Documentation - Expand user and developer documentation
5. Platform Support - Test on Windows, macOS, Linux

License

MIT OR Apache-2.0