Metadata-Version: 2.4
Name: lemma-lean
Version: 0.2.0
Classifier: Development Status :: 3 - Alpha
Classifier: Environment :: Console
Classifier: Intended Audience :: Developers
Classifier: License :: OSI Approved :: MIT License
Classifier: License :: OSI Approved :: Apache Software License
Classifier: Operating System :: MacOS
Classifier: Operating System :: Microsoft :: Windows
Classifier: Operating System :: POSIX :: Linux
Classifier: Programming Language :: Rust
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3 :: Only
Classifier: Topic :: Software Development :: Build Tools
Classifier: Topic :: Utilities
License-File: LICENSE
Summary: A modern Lean4 toolchain manager
Keywords: lean,lean4,toolchain,cli
Author-email: PuQing <me@puqing.work>
License: MIT OR Apache-2.0
Requires-Python: >=3.8
Description-Content-Type: text/markdown; charset=UTF-8; variant=GFM
Project-URL: Homepage, https://github.com/LeanOxide/lemma
Project-URL: Issues, https://github.com/LeanOxide/lemma/issues
Project-URL: Repository, https://github.com/LeanOxide/lemma.git

# Lemma - A Modern Lean4 Toolchain Manager

![GitHub Actions Workflow Status](https://img.shields.io/github/actions/workflow/status/LeanOxide/lemma/ci.yml?style=flat-square&logo=github)
![PyPI Version](https://img.shields.io/pypi/v/lemma-lean?style=flat-square&logo=pypi)
![PyPI Downloads](https://img.shields.io/pypi/dm/lemma-lean?style=flat-square&logo=pypi)
[![dependency status](https://deps.rs/repo/github/LeanOxide/lemma/status.svg?style=flat-square)](https://deps.rs/repo/github/LeanOxide/lemma)
![PyPI License](https://img.shields.io/pypi/l/lemma-lean?style=flat-square)
[![codecov](https://codecov.io/github/LeanOxide/lemma/graph/badge.svg)](https://codecov.io/github/LeanOxide/lemma)

[English](README.md) | [简体中文](README_CN.md)

**Lemma** is a rewrite of [elan](https://github.com/leanprover/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:

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

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

```toml
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`:

```bash
pipx install lemma-lean
```

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

```bash
python -m pip install --user lemma-lean
```

On Windows, use the Python launcher if needed:

```powershell
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:

```bash
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

```bash
# 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:

```bash
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

```bash
# 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:

```toml
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:
   ```toml
   lean_version = "v4.25.0"
   ```

### Directory Overrides

Set a toolchain for a specific directory and all subdirectories:

```bash
cd my-project
lemma override set stable
```

Remove the override:

```bash
lemma override unset
```

List all directory overrides:

```bash
lemma override list
```

### Custom Lean Release Sources

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

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

Or use environment variables:

```bash
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:

```bash
# List installed toolchains
lemma toolchain list

# Install the required toolchain
lemma toolchain install stable
```

### Proxy connection issues

If downloads fail behind a proxy:

```bash
# 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`:

```bash
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](LICENSE-MIT) OR [Apache-2.0](LICENSE-APACHE)

