Metadata-Version: 2.4
Name: lean-runtime
Version: 4.0.1
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"
Requires-Dist: zstandard<1,>=0.23
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

Lean Runtime makes Lean projects and standalone proofs work without asking you
to manage toolchains, dependency checkouts, exact environments, or caches.

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

## The daily workflow

Create a project:

```bash
lean-runtime new MyProof
cd MyProof
lean-runtime check
lean-runtime build
```

Use an existing pinned Lake project from its directory:

```bash
lean-runtime check
lean-runtime adopt
```

`adopt` verifies the existing exact dependency graph, previews reuse and disk
recovery, asks for confirmation, and swaps dependency links atomically. It does
not change `lean-toolchain` or `lake-manifest.json`. Passing a directory that
contains several projects discovers them automatically:

```bash
lean-runtime adopt ~/research
```

Check a standalone source file:

```bash
lean-runtime check Main.lean
```

The same command uses the nearest pinned Lake project when one exists and
otherwise performs bounded exact-environment discovery. A file can carry its
context in strict comment frontmatter:

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

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

When inference needs an override, there is one spelling:

```bash
lean-runtime check Main.lean --using mathlib@v4.33.0
lean-runtime check Main.lean --using environment.lock.json
lean-runtime check Main.lean --using research-stack
lean-runtime check Main.lean --using lean:v4.33.0
lean-runtime check Main.lean --using ~/proofs/MyProject
```

Typed `package:`, `lock:`, `env:`, `toolchain:`, and `project:` prefixes resolve
rare ambiguities. Persistent store, registry, and trust policy belongs in
environment configuration rather than everyday command lines.

## Commands

The normal surface is deliberately small:

```text
new NAME       create a project
adopt [PATH]   share dependencies from existing project(s)
check [PATH…]  check a project, directory, source file, or stdin
watch FILE     re-check on save
build [TARGET] build the current project
update         preview and apply a safe project update
publish        configure verified project publication
status [PATH]  explain the selected project or environment
verify SUBJECT verify an exact artifact
doctor         diagnose and offer safe repairs
clean          preview and reclaim unused storage
```

Project commands use the current directory when no path is supplied. Guided
mutations show their plan and ask before changing anything; automation passes
`--yes`, and inspection-only calls pass `--dry-run`.

Persistent registry, availability, store, and publisher-trust policy belongs
in `~/.config/lean-runtime/config.toml`; the nearest project's
`lean-runtime.toml` can override it. Daily commands therefore normally need no
configuration flags.

Exact and operator workflows live under noun namespaces:

```text
env       list · info · lock · acquire · diff · export · import
project   info · scan · share · unshare · lock · export
program   create · run · info · acquire · export · import · publish
toolchain list · info · install · optimize
storage   usage · verify
catalog   catalog maintenance
```

There are no v3 command aliases. `run`, `init`, `prepare`, `open`, `download`,
`environments`, `inspect`, `compare`, `copy`, `finalize`, `lean-run`, and
`lean-runtime-catalog` were removed in 4.0.

## Existing Elan installations

Lean Runtime automatically reuses an exact compatible toolchain already
installed by the user's Elan. This access is read-only: it never changes the
user's default, installs into the user's Elan home, or removes user toolchains.
Missing toolchains and downloadable slim checking runtimes remain isolated in
Lean Runtime's private store. `lean-runtime status` and `doctor` expose the
choice when it matters.

## Exact environments

```bash
lean-runtime env lock environment.toml --output environment.lock.json
lean-runtime env acquire environment.lock.json --name research-stack
lean-runtime env info research-stack
lean-runtime env diff previous.lock.json environment.lock.json
lean-runtime env export research-stack --output research-stack.lean-environment
lean-runtime env import research-stack.lean-environment --name imported-stack
```

Locks are canonical and content-addressed. Full environments preserve source;
downloaded sparse capsules project only verified import closures and keep the
same environment identity as their projection grows.

## Python

```python
import lean_runtime as lean

env = lean.setup(deps=["mathlib@v4.33.0"])
result = env.check("import Mathlib\nexample : 2 + 2 = 4 := by norm_num\n")
result.raise_for_error()
```

The Python API retains the explicit `Runtime`, `EnvironmentSpec`,
`EnvironmentLock`, project, capture, program, cancellation, and verification
interfaces for infrastructure code.

## Guarantees and limits

- Exact Git commits, trees, locks, toolchains, platform identities, and artifact
  digests are verified before an environment becomes ready.
- Acquisitions and project sharing are staged, probed, and published atomically.
- User project metadata and user Elan state are not silently rewritten.
- The local execution backend enforces supported resource limits but is not a
  network sandbox; unsupported isolation requests fail explicitly.
- Logical Lean rejections exit 1; invalid/infrastructure invocations exit 2;
  publication failures retain their documented classified exit statuses.

Documentation lives at
[alerad.github.io/lean-runtime](https://alerad.github.io/lean-runtime/).
