Metadata-Version: 2.4
Name: lean-runtime
Version: 0.6.0
Summary: Content-addressed execution environments for Lean 4
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 :: 3 - Alpha
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"
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 compiles declarative specifications into content-addressed Lean
execution environments.

```text
environment specification + Lean source + execution policy
                              ↓
kernel-checked result + exact environment and execution provenance
```

It does not replace Elan or Lake. Elan remains authoritative for toolchains and
Lake remains authoritative for dependency resolution and builds. Lean Runtime
adds immutable identities, lifecycle management, reuse, structured Python
results, and replayable provenance above them.

> **Status:** `0.5` alpha. Exact Git environments and trusted local execution
> are implemented. Local execution is an orchestration boundary, not a security
> sandbox.

Full guides, API examples, architecture, and the trust model live in the
[documentation](https://alerad.github.io/lean-runtime/).

## Installation

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

For development:

```bash
python -m pip install -e '.[dev]'
```

Users do not need a separately managed Lean installation. On macOS and Linux,
Lean Runtime bootstraps a private Elan installation and installs requested Lean
versions into its own cache. Windows currently requires `LEAN_RUNTIME_ELAN`.

## Check with a package

The shortest reproducible path discovers a tagged Lake package, pins it to an
exact commit, builds or reuses its environment, and checks the source:

```bash
lean-runtime check Main.lean \
  --with github:alerad/leancert@v4.32.2.4
```

The corresponding Python API uses the identical resolver and store:

```python
from lean_runtime import Runtime

result = Runtime().check(
    "import LeanCert.Tactic\nexample : True := by trivial",
    packages=["github:alerad/leancert@v4.32.2.4"],
)
```

Package discovery reads the referenced root `lean-toolchain` and
`lakefile.toml`, then records the exact commit in the environment lock. Multiple
`--with` options are allowed when their discovered toolchains agree. An
explicit `--toolchain` selects a compatibility build when they differ.

## Python API

```python
from lean_runtime import EnvironmentSpec, GitPackage, Runtime

runtime = Runtime()

spec = EnvironmentSpec(
    toolchain="leanprover/lean4:v4.32.2",
    packages=(
        GitPackage(
            name="mathlib",
            url="https://github.com/leanprover-community/mathlib4.git",
            rev="905b95818eb32af7874a58b427f50c1711a5e96c",
            root_module="Mathlib",
            artifact_command=("lake", "exe", "cache", "get"),
        ),
    ),
)

# Resolution is deliberately separate from materialization.
lock = runtime.resolve(spec)
environment = runtime.ensure(lock, name="mathlib-4.32.2")

result = environment.check(
    """
    import Mathlib

    example : 2 + 2 = 4 := by norm_num
    """
)

assert result.ok
print(result.environment_id)
print(result.execution_id)
print(result.provenance.request_digest)
print(result.provenance.packages)
```

`runtime.open()` performs no resolution and needs no network access:

```python
same_environment = Runtime().open(result.environment_id)
replayed = same_environment.check("import Mathlib\nexample : True := by trivial")
```

The convenience form compiles and reuses the environment automatically:

```python
result = runtime.check(source, environment=spec)
```

## Long-running Lean tools

Generic commands and stateful protocols run in the same disposable,
content-addressed execution model:

```python
import json

from lean_runtime import ExecutionPolicy

environment = runtime.ensure_references(
    ["github:alerad/leancert@v4.32.2.4"],
    name="leancert-4.32.2.4",
)

with environment.spawn_interactive(
    ["lake", "exe", "lean_bridge"],
    policy=ExecutionPolicy(timeout_seconds=3600, memory_mb=4096),
) as session:
    session.stdin.write(json.dumps({"id": 1, "method": "get_info", "params": {}}) + "\n")
    session.stdin.flush()
    response = json.loads(session.stdout.readline())

result = session.close()  # idempotent after context-manager cleanup
assert result.execution_id == session.execution_id
```

`Environment.execute(["lake", "exe", "target"])` provides the corresponding
one-shot path. Both APIs retain the exact environment, policy, command,
transcript, duration, and final exit status.

## Package revision policy

Specifications accept exact Git commits or explicitly marked tags:

```python
GitPackage(
    name="sample",
    url="https://github.com/example/sample.git",
    rev="0123456789abcdef0123456789abcdef01234567",
    root_module="Sample",
)

GitPackage.tag(
    name="mathlib",
    url="https://github.com/leanprover-community/mathlib4.git",
    tag="v4.32.2",
    root_module="Mathlib",
)
```

Tags are convenience inputs: resolution records their exact commit and Git tree
identity in the lock. Floating branches, semantic versions, editable
dependencies, and path packages are intentionally not part of the model.

`root_module` tells the generated environment root what to import so the
package's Lean artifacts are built. `artifact_command` is an optional explicit
package-supported hydration step; it is useful for Mathlib's cache command
without introducing a premature artifact-provider framework.

Artifact commands run from the generated root workspace. Locks, packages, and
artifact commands must be trusted; schema validation is not a security sandbox.

## CLI

An environment specification can be JSON or TOML. See
[examples/mathlib.toml](examples/mathlib.toml).

```bash
lean-runtime check Main.lean --with github:alerad/leancert@v4.32.2.4
lean-runtime resolve environment.toml --output environment.lock.json
lean-runtime ensure environment.lock.json --name research-stack
lean-runtime check research-stack Main.lean --json
lean-runtime inspect research-stack
lean-runtime replay result.execution.json --json
lean-runtime gc                         # dry-run
lean-runtime gc --execute              # removes old, unnamed environments
```

Raw execution remains available for existing projects and core-only snippets:

```bash
lean-runtime raw-check Main.lean --toolchain 4.32.0
lean-runtime raw-check Main.lean --project ./existing-project
lean-runtime project-build ./existing-project MyLibrary
```

## Execution policy

```python
from lean_runtime import ExecutionPolicy

policy = ExecutionPolicy(
    timeout_seconds=30,
    max_output_bytes=1_000_000,
    memory_mb=2048,
    cpu_seconds=20,
)

result = environment.check(source, policy=policy)
print(result.provenance.enforced_policy_fields)
```

The local Unix backend enforces timeout, bounded captured output, address-space
and CPU limits. It cannot enforce network isolation and rejects
`network="disabled"` rather than claiming otherwise. Future container and
remote backends can implement stronger policies without changing environment
semantics.

Checks can be cancelled or batched:

```python
job = environment.start_check(source)
job.cancel()
result = job.result()

results = environment.check_many(sources, concurrency=8)
```

Multi-file and asyncio requests are first-class:

```python
result = environment.check_files(
    {"Support/Defs.lean": defs, "Main.lean": main},
    entrypoint="Main.lean",
)
result = await environment.check_async(source)
```

Long operations can emit structured progress events:

```python
runtime = Runtime(on_event=lambda event: print(event.kind, event.message))
```

## Captures

The first capsule representation is intentionally a canonical JSON manifest,
not a bespoke archive:

```python
capture = environment.capture(source, expected_ok=True)
capture.write("result.execution.json")
```

It contains the complete environment lock, input files, policy, operation, and
optional expected outcome. `runtime.replay_capture(...)` or
`lean-runtime replay` can acquire the exact locked sources and recreate the
environment without invoking dependency resolution. Source/binary archives,
signatures, and attestations are deferred until their trust model is clear.

## Store

The default store is `~/Library/Caches/lean-runtime` on macOS and
`${XDG_CACHE_HOME:-~/.cache}/lean-runtime` on Linux. Set `LEAN_RUNTIME_HOME` to
override it.

```text
lean-runtime/
  elan/          private toolchains
  sources/git/   immutable exact source snapshots
  locks/         portable Lake-backed locks
  environments/  platform-specific published builds
  names/         mutable aliases to immutable identities
  executions/    result/provenance records
  jobs/          disposable writable execution instances
```

See [Architecture](docs/architecture.md) for identities, publication rules,
offline behavior, and trust boundaries.

## Security

Lean files, dependency Lake configurations, custom targets, native extensions,
and artifact commands are trusted code. Content addressing provides identity
and reuse; it is not a sandbox. Do not build adversarial packages with the
local backend.

## License

Apache License 2.0.
