Metadata-Version: 2.4
Name: lean-runtime
Version: 2.0.3
Summary: Run Lean 4 proofs from Python or standalone files
Author: Alejandro Radisic
License-Expression: Apache-2.0
Project-URL: Homepage, https://github.com/alerad/lean-runtime
Project-URL: Documentation, https://alerad.github.io/lean-runtime/
Project-URL: Repository, https://github.com/alerad/lean-runtime.git
Project-URL: Issues, https://github.com/alerad/lean-runtime/issues
Project-URL: Changelog, https://github.com/alerad/lean-runtime/blob/main/CHANGELOG.md
Keywords: lean4,theorem-prover,formal-verification,toolchain
Classifier: Development Status :: 4 - Beta
Classifier: Operating System :: MacOS
Classifier: Operating System :: POSIX :: Linux
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Typing :: Typed
Requires-Python: >=3.10
Description-Content-Type: text/markdown
License-File: LICENSE
Requires-Dist: tomli>=2; python_version < "3.11"
Provides-Extra: dev
Requires-Dist: pytest>=8; extra == "dev"
Requires-Dist: ruff>=0.6; extra == "dev"
Requires-Dist: mypy>=1.10; extra == "dev"
Requires-Dist: tomli>=2; extra == "dev"
Requires-Dist: jsonschema>=4.23; extra == "dev"
Provides-Extra: docs
Requires-Dist: mkdocs<2,>=1.6; extra == "docs"
Requires-Dist: mkdocs-material>=9.5; extra == "docs"
Dynamic: license-file

# Lean Runtime

Run Lean proofs from Python or a single `.lean` file—without creating a throwaway
Lake project or rebuilding the same dependencies on every machine.

Lean Runtime discovers the exact Lean environment a project needs and reuses a
downloadable copy when one is available. It returns structured Lean results
with a record of the toolchain and dependencies that were actually used.

> **Status:** V1 beta. The local backend runs trusted Lean, Lake, and package code;
> it is an orchestration boundary, not a security sandbox.

## Install

```bash
python -m pip install lean-runtime
```

Lean Runtime manages its own Elan installation on macOS and Linux. Windows
currently requires `LEAN_RUNTIME_ELAN`.

## Run one Lean file

Inside an existing pinned Lake project, just pass the file:

```bash
lean-run MyProject/Main.lean
```

For a portable standalone file, declare exact dependencies in TOML frontmatter:

```lean
-- /// lean-runtime
-- requires = ["mathlib@v4.32.2"]
-- ///

import Mathlib

example : 2 + 2 = 4 := by norm_num
```

```bash
lean-run Main.lean
```

The same context can be supplied from the command line:

```bash
lean-run Main.lean --with mathlib@v4.32.2
```

Create an exact lock for CI without changing the file:

```bash
lean-run Main.lean --with mathlib@v4.32.2 \
  --lock-out environment.lock.json
lean-run Main.lean --lock environment.lock.json
```

## Python

Configure an environment once, then use it repeatedly:

```python
import lean_runtime as lean

env = lean.setup(["mathlib@v4.32.2"])

result = env.check(
    """
    import Mathlib
    example : 2 + 2 = 4 := by norm_num
    """
)
result.raise_for_error()
```

Batch and asyncio APIs reuse that prepared environment:

```python
results = env.check_many(generated_proofs, concurrency=8)
results = await env.check_many_async(generated_proofs, concurrency=20)
```

Local projects use the same setup pattern while retaining mutable-project
semantics:

```python
project = lean.setup(project="./my-project")
result = project.check_file("./my-project/MyProject/Main.lean")
```

One-shot helpers are available when setup reuse is unnecessary:

```python
result = lean.check(source, deps=["mathlib@v4.32.2"])
result = lean.check_file("./my-project/MyProject/Main.lean")
```

When you need evidence rather than extra setup, the operations CLI can verify, explain,
compare, and measure the same exact contexts:

```bash
lean-runtime verify research-stack --offline
lean-runtime compare previous.lock.json environment.lock.json
lean-runtime profile research-stack Main.lean --repeat 5
lean-runtime matrix compatibility.toml Main.lean
```

Use `lean-run Main.lean --explain` to inspect context routing without executing Lean, and
`--timings` to expose preparation versus execution time. Successful ordinary checks remain
one concise line.

Friendly references remain exact: use `mathlib@VERSION`,
`leancert@VERSION`, `owner/repository@REVISION`, or the explicit
`github:owner/repository@REVISION` form. Bare floating package names are never
accepted.

## Share environments

A **project** is your ordinary Lake repository. Its **environment** is the exact
Lean version, dependencies, and build configuration needed to use it. A
**downloadable environment** is a ready-to-use copy that collaborators and CI
can fetch instead of rebuilding Mathlib.

Environment libraries may be public or private. For example:

```bash
lean-runtime --library ghcr.io/owner/lean-environments download environment.lock.json
lean-runtime build-and-publish environment.lock.json \
  --publish-to ghcr.io/owner/lean-environments
```

For an already-built executable, Lean Runtime can also create a verified
**ready-to-run program**. It opens without rebuilding the project, can be saved
as a portable copy, and can be shared through a public or private program
library. See [Ready-to-run programs](https://github.com/alerad/lean-runtime/blob/main/docs/ready-programs.md).

## Technical details

The simple API is backed by exact Git commits and trees, Lake-resolved locks,
platform-aware content-addressed environments, atomic cross-process builds,
downloadable environment reuse, replayable provenance, verification, and trusted
publishers. The libraries use OCI-compatible storage internally, but users do
not need Docker or container concepts. Advanced protocol details remain in the
architecture documentation.

## Documentation

- [Getting started](https://github.com/alerad/lean-runtime/blob/main/docs/getting-started.md)
- [Python API](https://github.com/alerad/lean-runtime/blob/main/docs/python-api.md)
- [`lean-run` and operations CLI](https://github.com/alerad/lean-runtime/blob/main/docs/cli.md)
- [Managed environments](https://github.com/alerad/lean-runtime/blob/main/docs/environments.md)
- [Local Lake projects](https://github.com/alerad/lean-runtime/blob/main/docs/local-projects.md)
- [Portable copies and environment libraries](https://github.com/alerad/lean-runtime/blob/main/docs/portable-copies.md)
- [Ready-to-run programs](https://github.com/alerad/lean-runtime/blob/main/docs/ready-programs.md)
- [Architecture](https://github.com/alerad/lean-runtime/blob/main/docs/architecture.md)
- [Trust and limitations](https://github.com/alerad/lean-runtime/blob/main/docs/trust-and-limitations.md)
- [V1 release case study](https://github.com/alerad/lean-runtime/blob/main/docs/case-study-v1.md)

## License

Apache License 2.0.
