Context selection¶
Every check runs inside one selected context. Context selection and compiler acceptance are separate decisions.
For ordinary standalone checks, let Lean Runtime discover the context. Explicit context is an override for reproducibility, compatibility testing, or a request that specifically names a release.
Precedence¶
For a Lean file, Lean Runtime considers context sources in this order:
- An explicit command-line or Python API context
- Lean Runtime frontmatter in the file
- The nearest pinned Lake project
- Automatic catalog discovery
If none can produce a context, the operation fails before Lean runs.
Explicit context¶
An explicit context can identify a project, lock file, stored environment, toolchain, or package reference. Explicit input does not need discovery.
Frontmatter¶
-- /// lean-runtime
-- toolchain = "leanprover/lean4:v4.33.0"
-- ///
example : 1 + 1 = 2 := by decide
Frontmatter travels with the source while remaining valid Lean comments.
Pinned project context¶
A file beneath a Lake project uses the nearest project with both a pinned toolchain and manifest. Lean Runtime does not replace those version decisions during a normal project check.
Automatic discovery¶
Discovery begins with declared source imports. The bundled catalog associates exact environments with module inventories. Plausible candidates are ordered under a bounded policy and checked in turn.
Static analysis proposes candidates. It does not prove compatibility. A candidate is accepted only if Lean accepts the source inside that exact environment.
Candidate count, compiler time, wall time, remote acquisition, offline mode, and source-build permission can bound the search. Reaching a bound can produce an inconclusive discovery result rather than a claim that no compatible environment exists.
Inspect the decision¶
status reports evidence and routing. A successful check reports compiler acceptance and execution provenance.