Lean Runtime

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

python -m pip install lean-runtime

The daily workflow

Create a project:

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

Use an existing pinned Lake project from its directory:

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:

lean-runtime adopt ~/research

Check a standalone source file:

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-runtime
-- requires = ["mathlib@v4.33.0"]
-- ///

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

When inference needs an override, there is one spelling:

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:

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:

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

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

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 in docs/. Start with docs/getting-started.md, docs/cli.md, and docs/local-projects.md.