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"

Installation

Quick Install (Recommended)

Install Lemma as a Python package. The package name and command are both lemma.

pipx install lemma

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

python -m pip install --user lemma

On Windows, use the Python launcher if needed:

py -m pip install --user lemma

After installation, run a setup command such as lemma lean 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

# 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
# or
python -m pip install --user --upgrade lemma

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

Usage

Basic Commands

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

# List toolchains
lemma lean list

# Set default toolchain
lemma default stable

# Upgrade installed channel toolchains
lemma lean 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

lemma toolchain ... remains available as a compatibility alias for lemma lean ..., but new documentation uses lemma lean ....

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"

[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_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"

Or use environment variable:

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

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 lean list

# Install the required toolchain
lemma lean 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