Lemma - A Modern Lean4 Toolchain Manager

GitHub Actions Workflow Status PyPI Version PyPI Downloads dependency status PyPI License codecov

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

Project links

Data verified by PyPI on
Data provided by the project maintainers, verified at the time the release was uploaded to PyPI.

Key dates

PyPI data
Data sourced directly from PyPI's database.
  • Released:
Latest release

1 maintainer

PyPI data
Data sourced directly from PyPI's database.
Avatar for PuQing from gravatar.com PuQing

Credits

PyPI data
Data sourced directly from PyPI's database.

Author: PuQing

GitHub Statistics

Data verified by PyPI on 
The GitHub source repository was provided by the project maintainers and verified by PyPI at the time of upload. Stars, forks, and open issues/PRs are derived from that repository and have not been independently verified.

License

Apache Software License, MIT License (MIT OR Apache-2.0)

Requires

Python >=3.8

Tags

lean lean4 toolchain cli

Classifiers

Report project as malware

Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

lemma_lean-0.2.0.tar.gz (87.6 kB view details)

Uploaded Source

Built Distributions

If you're not sure about the file name format, learn more about wheel file names.

lemma_lean-0.2.0-py3-none-win_amd64.whl (2.7 MB view details)

Uploaded Python 3Windows x86-64

lemma_lean-0.2.0-py3-none-manylinux_2_17_x86_64.manylinux2014_x86_64.whl (3.0 MB view details)

Uploaded Python 3manylinux: glibc 2.17+ x86-64

lemma_lean-0.2.0-py3-none-manylinux_2_17_aarch64.manylinux2014_aarch64.whl (2.8 MB view details)

Uploaded Python 3manylinux: glibc 2.17+ ARM64

lemma_lean-0.2.0-py3-none-macosx_11_0_arm64.whl (2.6 MB view details)

Uploaded Python 3macOS 11.0+ ARM64

lemma_lean-0.2.0-py3-none-macosx_10_12_x86_64.whl (2.8 MB view details)

Uploaded Python 3macOS 10.12+ x86-64

File details

Details for the file lemma_lean-0.2.0.tar.gz.

File metadata

  • Download URL: lemma_lean-0.2.0.tar.gz
  • Upload date:
  • Size: 87.6 kB
  • Tags: Source
  • Uploaded using Trusted Publishing? Yes
  • Uploaded via: twine/7.0.0 CPython/3.13.14

File hashes

Hashes for lemma_lean-0.2.0.tar.gz
Algorithm Hash digest
SHA256 e719e3fdc036b7f9f76805e2d85dab512464571dfcd2eead7c9ad777c746f445
MD5 6804bf8b8337e186099f58823d3a9334
BLAKE2b-256 5e53fec33f96116851e5710dad4e980e821520263ce581b1ab16053c3f24c427

See more details on using hashes here.

Provenance

The following attestation bundles were made for lemma_lean-0.2.0.tar.gz:

Publisher: release.yml on LeanOxide/lemma

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file lemma_lean-0.2.0-py3-none-win_amd64.whl.

File metadata

  • Download URL: lemma_lean-0.2.0-py3-none-win_amd64.whl
  • Upload date:
  • Size: 2.7 MB
  • Tags: Python 3, Windows x86-64
  • Uploaded using Trusted Publishing? Yes
  • Uploaded via: twine/7.0.0 CPython/3.13.14

File hashes

Hashes for lemma_lean-0.2.0-py3-none-win_amd64.whl
Algorithm Hash digest
SHA256 02b5559a572463e18915f104c4bfa3b53d0140f6cfd541bdccb7c168c000a9d0
MD5 2e99107b30a1be43abd90cc9dded3e93
BLAKE2b-256 c2b463cb0e01b0856908ca97906b3cb6e6e52130ccf044fa9ca170a3aab8731f

See more details on using hashes here.

Provenance

The following attestation bundles were made for lemma_lean-0.2.0-py3-none-win_amd64.whl:

Publisher: release.yml on LeanOxide/lemma

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file lemma_lean-0.2.0-py3-none-manylinux_2_17_x86_64.manylinux2014_x86_64.whl.

File metadata

File hashes

Hashes for lemma_lean-0.2.0-py3-none-manylinux_2_17_x86_64.manylinux2014_x86_64.whl
Algorithm Hash digest
SHA256 49a56e8c6860ceb3f9bb8feda918e0bbdd8b24c879665589749fc21a220177da
MD5 cb29a5b9822134bc8443b55a3c9409dd
BLAKE2b-256 7c482b9a139c2c335df1cf515a9821c95b95219068015c45fbf17d3107fbf21b

See more details on using hashes here.

Provenance

The following attestation bundles were made for lemma_lean-0.2.0-py3-none-manylinux_2_17_x86_64.manylinux2014_x86_64.whl:

Publisher: release.yml on LeanOxide/lemma

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file lemma_lean-0.2.0-py3-none-manylinux_2_17_aarch64.manylinux2014_aarch64.whl.

File metadata

File hashes

Hashes for lemma_lean-0.2.0-py3-none-manylinux_2_17_aarch64.manylinux2014_aarch64.whl
Algorithm Hash digest
SHA256 2eb710b824cbc989ae242993b150e02f3499b7536b7443ddac9edb99260b2604
MD5 a63280b5cecf0502ccb72d0d489d5d1a
BLAKE2b-256 a24e6e3108a0b0a225746d82ba2bbe489c9a635e944c304c420be79b99d2d61f

See more details on using hashes here.

Provenance

The following attestation bundles were made for lemma_lean-0.2.0-py3-none-manylinux_2_17_aarch64.manylinux2014_aarch64.whl:

Publisher: release.yml on LeanOxide/lemma

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file lemma_lean-0.2.0-py3-none-macosx_11_0_arm64.whl.

File metadata

File hashes

Hashes for lemma_lean-0.2.0-py3-none-macosx_11_0_arm64.whl
Algorithm Hash digest
SHA256 3704ea1b254744881f789e8d1f2639b9b641d2515c1867da9a48b607e1d03c8d
MD5 17c68f52c194216616b9db96e4c2a6d8
BLAKE2b-256 2a8ea8357e1a2cb88257efe48667eb7ef569fc7cafbc7ed6b8ee3ec695b44386

See more details on using hashes here.

Provenance

The following attestation bundles were made for lemma_lean-0.2.0-py3-none-macosx_11_0_arm64.whl:

Publisher: release.yml on LeanOxide/lemma

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file lemma_lean-0.2.0-py3-none-macosx_10_12_x86_64.whl.

File metadata

File hashes

Hashes for lemma_lean-0.2.0-py3-none-macosx_10_12_x86_64.whl
Algorithm Hash digest
SHA256 62a8ee6f539b395d40f02980d1d56abd3b4f17a607e40c811750a9a9e3ec48ba
MD5 7fabbb102bf74e440e627023b5c7a42a
BLAKE2b-256 e5044377e682fc0c50df1ef865848c869bb1361c61bfb070652efcf5744ca5d1

See more details on using hashes here.

Provenance

The following attestation bundles were made for lemma_lean-0.2.0-py3-none-macosx_10_12_x86_64.whl:

Publisher: release.yml on LeanOxide/lemma

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

Supported by

AWS Cloud computing and Security Sponsor Datadog Monitoring Depot Continuous Integration Fastly CDN Google Download Analytics Pingdom Monitoring Sentry Error logging StatusPage Status page