lean-rs

Rust bindings for hosting Lean 4 capabilities. Lean owns Lean semantics — elaboration, kernel checking, proof objects, universes, MetaM, dependent-type meaning. lean-rs owns hosting: linking, runtime initialization, ABI conversion, module loading, error and panic boundaries, scheduling, diagnostics, batching, and packaging. Rust does not reconstruct Lean semantic facts.

This site collects the architecture charter, design notes, recipes, safety audits, and operational runbooks that ship in the lean-rs repository. The repository README is the entry point for new users — it walks through the crate layout, the minimal same-process example, and the worked examples. Read it first if you have not used lean-rs before.

Where to start

If you read only two pages on this site, read them in this order:

1. Charter — the design boundary between Lean and lean-rs, what is hidden, what is preserved, and which alternatives were rejected.
2. Safety model — the unsafe boundary, refcount ownership, and the workspace concurrency stance.

Everything else is reference for a specific subsystem. The numeric prefix on each architecture document reflects the order it was written, not the order it should be read; use the sidebar groupings instead.

How the site is organized

• Foundations — charter, safety model, versioning, raw FFI rationale.
• Same-process FFI (lean-rs) — the L1 safe front door: concurrency, panic containment, callbacks, loader.
• Host stack (lean-rs-host) — the L2 theorem-prover-host surface and its capability contract.
• Worker (lean-rs-worker) — the process-boundary supervisor and its scale and observability story.
• Recipes — task-oriented walkthroughs for shipping a Lean-backed crate or wiring a worker capability.
• Safety audits — long-session memory bounds and the workspace unsafe inventory.
• Operations — testing strategy, performance baselines, diagnostics, release process, toolchain bumps.

Versions and platforms

lean-rs targets stable Rust (MSRV 1.91) on macOS and Linux. The supported Lean toolchain window is enumerated in Version matrix; the procedure for extending it is Bump toolchain.

Architecture Charter

The design boundary between Lean and lean-rs, the smallest public interface that supports it, and the alternatives that were considered and rejected. Any new API or behavior must clear three questions: does it hide what should be hidden, preserve what should be preserved, discard what should be discarded?

The charter pins intent, not Rust items or symbol names; those live in the per-crate API review baselines under docs/api-review/.

Purpose

Lean owns elaboration, kernel checking, proof objects, universes, MetaM, and dependent-type meaning. lean-rs owns linking, runtime initialization, ABI conversion, module loading, error and panic boundaries, scheduling, diagnostics, batching, and packaging. The two halves do not negotiate. Anything that asks Rust to recompute a Lean semantic fact is out of scope; anything that asks Lean to know about Rust hosting (thread pools, panic conversion, FFI batching, module loaders) is out of scope.

Adopted Shape

Five published crates plus one workspace-internal helper:

• lean-rs-sys (published). Raw extern "C" view of lean.h, split by semantic category; pure-Rust mirrors of lean.h’s static inline refcount helpers via AtomicI32::from_ptr; the REQUIRED_SYMBOLS allowlist; build-time LEAN_HEADER_DIGEST; link directives. Public types are opaque (lean_object is [u8; 0] + PhantomData<(*mut u8, PhantomPinned)>); layout structs are pub(crate). The one crate-wide #[allow(unsafe_code)] opt-out; every unsafe { ... } block carries a // SAFETY: comment naming the invariant.
• lean-toolchain (published). Toolchain discovery, typed ToolchainFingerprint, fixture digest, layered link diagnostics, build-script helpers. Re-exports LEAN_VERSION, LEAN_HEADER_DIGEST, and REQUIRED_SYMBOLS from lean-rs-sys so the allowlist lives in one place.
• lean-rs (published, L1). The safe FFI primitive: bring the runtime up, open a Lake-built dylib, initialise a module, call typed @[export] functions, and register Rust callbacks through a generic shim package. Five public modules (error, module, handle, runtime, abi) plus one #[doc(hidden)] pub mod __host_internals giving the sibling lean-rs-host the small set of LeanError-constructor wrappers it needs without exposing them to external callers. It has no theorem-prover host shim contract; every downstream that just needs to call Lean from Rust starts here.
• lean-rs-host (published, L2). The opinionated theorem-prover-host stack built on lean-rs: LeanHost, LeanCapabilities, LeanSession, elaboration / evidence / meta surfaces, SessionPool. Owns and bundles the 28 + 6 lean_rs_host_* @[export] Lean shim contract it loads alongside consumer capability dylibs. Batch and session-pool operations are methods on LeanSession rather than a separate batch module. Downstreams that want this opinion add it on top of lean-rs; downstreams that don’t aren’t paying for it.
• lean-rs-worker (published process-boundary layer). The worker crate supervises a child process around the host stack. It owns process lifecycle, private framing, request timeouts, fatal-exit classification, memory cycling, live row streaming, diagnostics, terminal summaries, capability metadata, and typed command facades. It is not a remote LeanSession mirror and not a lean-dup API. Downstreams bring their own command names and serde row schemas.

lean-rs-test-support is workspace-internal (publish = false).

Composition Rule

Compose at the highest layer that fits the workload:

• use lean-rs for custom same-process ABI calls, module loading, and advanced callbacks;
• use lean-rs-host for trusted in-process theorem-prover work such as imports, elaboration, kernel checks, declaration queries, progress, cancellation, and pooling;
• use lean-rs-worker when the application needs a process boundary for fatal Lean exits, request watchdogs, worker cycling, live row streams, diagnostics, or typed downstream commands.

Lower layers are still real APIs. They are escape hatches and implementation substrates, not steps every downstream caller should hand-compose.

Lifetime spine

The universal currency inside lean-rs is a token-bound object handle: runtime::Obj<'lean> carries a phantom lifetime tied to a &'lean LeanRuntime borrow. Public types built on top—the L1 semantic handles (LeanExpr<'lean>, LeanName<'lean>, …) and the L2 surfaces in lean-rs-host (LeanHost<'lean>, LeanCapabilities<'lean, 'h>, LeanSession<'lean, 'c>)—propagate the lifetime so the type system enforces init-before-use and no value escapes the runtime. The pattern is borrowed from PyO3’s Bound<'py, T>; LeanRuntime plays the role Python<'py> plays, except creation is process-once rather than GIL-scoped. 'lean is invisible at typical call sites (inferred from the runtime borrow) and disappears from the *_rs::* re-exports when bound to 'static.

The L1/L2 crate split gives each layer its own semver and refactor surface: lean-rs’s internal modules can reshape without affecting lean-rs-host callers, and vice versa, as long as both crate roots stay stable.

Topic deep-dives:

• 05-raw-sys-design.md — lean-rs-sys per-decision rationale.
• 03-host-stack.md — lean-rs-host curated surface.
• 14-interop-release-contract.md — reusable interop release contract.
• 16-production-boundary.md, 17-worker-session-adapter.md — worker-process boundary and the host-session subset crossing it.
• 18-worker-data-streaming.md — downstream row streams over the worker boundary.
• 20-worker-pool.md — local worker-pool boundary.
• 22-worker-row-batching.md, 23-worker-data-plane-format.md — row batching and data-plane format decisions.
• 24-lean-side-worker-streaming.md — Lean-side worker envelope helpers.
• 28-production-scale-release.md — production-scale worker contract.

Hidden knowledge

No public Rust API requires a caller to know any of this. If an L1 item appears in lean-rs’s public surface, or an L2 item in lean-rs-host’s, the wrong layer has taken ownership.

Hidden by lean-rs (L1):

• Runtime init order: lean_initialize_runtime_module, lean_initialize, per-thread lean_initialize_thread / lean_finalize_thread, process-args setup, LEAN_INIT_MUTEX.
• lean_object layout: tag bits, packed scalar encoding, ctor field placement, scalar vs heap distinction (lean_is_scalar).
• Reference counting: lean_inc / lean_dec, owned vs borrowed args (lean_obj_arg vs b_lean_obj_arg), owned results (lean_obj_res), in-place reuse rules.
• Module initializer names and ordering: per-module initialize_<Module> symbols, dependency order, idempotent flag.
• Object conversion: boxed scalars (lean_box / lean_unbox), strings, bytearrays, arrays, ctor structures, closures.
• Exception and panic boundary: Lean exceptions to typed Rust errors; Rust panics caught before unwinding across a C frame.
• The seam between Lean semantic authority and Rust hosting: Rust never owns a semantic fact about a Lean term.

Hidden by lean-rs-host (L2):

• Session lifecycle: LeanHost → LeanCapabilities → LeanSession construction order, imports cache, capability refresh, the 28 + 6 lean_rs_host_* Lean shim contract.
• Capability dispatch: SessionSymbols cached address tables, Args / R propagation through call_capability, tracing-span shape and metrics.
• Batching: per-source result aggregation, N + 1 vs 2N FFI-cost analysis behind bulk methods, strict / skip-missing semantics.
• Pool capacity: FIFO-take / LIFO-push reuse, capability-agnostic storage (entries are bare Obj<'lean> environments rewrapped at acquire), over-capacity drop accounting.

Decisions that must not leak

Implementation details. Changing them is allowed; surfacing them in the public API is a contract change.

• lean_object layout (tag bits, header, ctor field order).
• Borrowed vs owned RC tokens (lean_obj_arg, b_lean_obj_arg, lean_obj_res).
• Module initializer symbol names (initialize_<Module>), ordering, per-module idempotence flag.
• Lake search policy: how lean-toolchain finds Lake, search order, cache, fallback discovery for embedders without a Lake workspace.
• MetaM execution details: elaborator state, meta-level monad stack, trace and option propagation.
• Raw proof-term interpretation: Expr, universe levels, declaration bodies, environment internals.

Preserved capability

Rust applications using lean-rs can call Lean code, ask the elaborator and kernel semantic questions through bounded host capabilities, and receive typed results. They can load compiled Lean modules, invoke exported functions, batch calls, and reuse sessions. None of this requires reaching into lean-rs-sys or knowing any item in the hidden-knowledge table. Applications that legitimately need raw FFI—for example, to call a Lean capability not yet wrapped in lean-rs—can opt in by depending on lean-rs-sys directly, accepting full unsafe discipline. This is friendlier than a workspace fork.

Discarded behaviour

Not in scope; will not be added.

• Raw lean_* calls through lean-rs. Raw imports live in pub(crate) modules and are never re-exported through lean-rs’s safe surface. Applications needing raw FFI depend on lean-rs-sys directly (opting in to full unsafe discipline and opaque public types). The recommended path is to contribute the missing capability to lean-rs’s safe layer.
• Rust-side reconstruction of Lean semantics. No parallel representation of Expr, universes, environments, or proof terms.
• Unmeasured FFI micro-optimizations. Any performance claim is backed by a named workload, command, before number, and after number—the discipline in PERFORMANCE-BASELINE.

Rejected alternatives

Each was considered before the adopted shape. Recorded so later prompts can recognize a regression toward one of them.

• A safe wrapper over all of lean.h. Surface is large and shallow. Every ABI decision (lean_obj_arg direction, RC obligation, initializer ordering, ctor field layout) ends up in the public type system, so the caller still has to know everything lean.h knows. The “safety” is nominal.
• Mirror Lean internals in Rust. Creating Rust types for Expr, Level, Name, environments, and elaborator state creates a second source of truth. Drift is guaranteed the moment Lean’s internals evolve, and drift here means quietly wrong proofs. The charter’s first rule—Lean owns Lean semantics—exists to make this impossible.
• Thin façade re-exporting raw FFI directly. Pushes the entire initialization, refcount, and error contract back onto callers. No error or panic boundary; degenerates into raw-FFI-with-extra-steps.
• Six published crates, one per layer (lean4-sys → lean4-runtime → lean4-abi → lean4-module → lean4-host + test-support). Fake public-API story: no real downstream picks up lean4-abi or lean4-runtime in isolation; they take lean4-host. Cuts against the dominant Rust binding shape (git2+libgit2-sys, openssl+openssl-sys, z3+z3-sys, rusqlite+libsqlite3-sys, the pyo3 family), which is consistently two or three crates: a raw *-sys plus one safe front door, plus a build helper in larger stacks. The internal organization the layer cake encodes is real and worth preserving; pub(crate) modules inside lean-rs police those boundaries at zero semver cost.
• External lean-sys adoption. Considered taking digama0/lean-sys as the raw FFI source. Rejected: the published 0.0.9 was pinned to a Lean below our target, and the surfaces we needed (LEAN_VERSION const, cargo:rerun-if-changed=lean.h, signature-checked allowlist, typed diagnostics) would have required ongoing upstream PRs the published crate did not provide.
• Conflate L1 FFI primitive and L2 host stack in one crate. Putting both layers behind one default entry point (LeanHost) made it impossible for an external L1-only consumer to depend on lean-rs = "0.1" without first satisfying the lean_rs_host_* shim contract. Generic callback helpers belong below the host stack; theorem-prover host shims do not.

The adopted shape is deeper than each rejected alternative: fewer caller-facing details, less temporal coupling, a small unsafe surface, and a one-line in-process layering invariant (lean-rs-sys → lean-toolchain → lean-rs → lean-rs-host) with lean-rs-worker wrapping the host stack when callers need a process boundary. It matches the dominant Rust binding shape, so contributors arrive with correct expectations, and it contains no Rust-side dependent-type imitation.

Safety Model

lean-rs exposes a fully safe Rust surface over an unsafe C ABI by confining raw FFI to one crate, denying Send/Sync on every Lean handle, and binding handle lifetimes to a process-once runtime anchor. Every change that adds an unsafe block, wrapper type, FFI call, or concurrency claim must be consistent with the rules below. An API that cannot be made consistent does not ship.

Unsafe boundary

Raw lean_* symbols enter the workspace only through lean-rs-sys (published). Its public types are opaque: lean_object is [u8; 0] + PhantomData<(*mut u8, PhantomPinned)>, and downstream code reaches object state only through pub unsafe fn helpers. Lean’s header layout (LeanObjectRepr) is pub(crate).

Inside lean-rs, every import of a lean_rs_sys item lives in a pub(crate) module of runtime and is never re-exported. Every public function of lean-rs and lean-toolchain is safe Rust. A reader of lean_rs::* cannot acquire a raw Lean pointer through the public API.

Applications that genuinely need raw FFI opt in by depending on lean-rs-sys directly, accepting full unsafe discipline (per-block // SAFETY:, per-fn # Safety doc) and opaque public types—friendlier than forking the workspace, and the same trade every peer *-sys crate makes.

Reference counting

Lean’s per-thread runtime model means refcount adjustments cannot escape the safe layer. pub(crate) runtime::obj::Obj<'lean> owns one refcount; pub(crate) runtime::obj::ObjRef<'lean, 'a> is a borrowed view tied to its source’s lifetime and the runtime borrow. Obj<'lean> releases its reference on Drop; Clone performs lean_inc via the Rust mirror in lean-rs-sys; ObjRef performs no RC adjustments on its own.

The public surface never accepts or returns raw lean_obj_arg, b_lean_obj_arg, or lean_obj_res. A caller of lean-rs does not need to know what lean_inc and lean_dec are. If a future API would force the caller to choose a refcount discipline, that is a charter violation, not an option.

Proof objects

Proof-related results cross into Rust as opaque handles or Lean-authored summaries. Rust does not reconstruct proof terms, inspect their structure, or re-derive a kernel judgement; the kernel is in Lean.

A handle’s only safe public operations are the ones Lean explicitly exposes through a capability—“ask Lean to print this proof’s type” is fine if Lean offers it; “walk the proof’s expression tree in Rust” is not.

Concurrency

The Lean runtime is per-thread (lean_initialize_thread / lean_finalize_thread), so every Lean-derived handle is !Send + !Sync by default. Treating a Lean object as freely portable is a soundness hazard. Opting any handle type into Send or Sync is a per-type contract change that must be justified against the per-thread model.

See 04-concurrency.md for the full thread-attach discipline and the async-embedding pattern.

Workspace lint policy

unsafe-code = "deny" at the workspace level (set in Cargo.toml [workspace.lints.rust]).

Per-file opt-outs require, in order:

1. #[allow(unsafe_code)] at the smallest scope that compiles—a module, not a crate. PR description names the reason. A blanket allow at the crate root is rejected.
2. A // SAFETY: comment on every unsafe { ... } block naming the invariant the caller or surrounding context relies on. “Calls into lean-rs-sys” is not a safety comment; “the runtime is initialized on this thread and obj is the unique owner per Obj<'lean>’s Drop” is.
3. A test that would fail under a plausible violation when practical—Miri on the Rust side of the boundary (Miri cannot validate the Lean C runtime itself), a sanitizer build, a refcount stress test, or a focused unit test on the unsafe seam.
4. Reviewer sign-off from someone other than the author. Self-merging a new unsafe block is not allowed.

Panic discipline

Rust panics must not unwind across a C or Lean frame. The error module of lean-rs is the typed conversion point for Rust-owned boundaries: it catches Rust panics before they cross into Lean callbacks, converts Lean IO exceptions to typed Rust errors, and converts ABI-shape violations to typed errors. It is not a Lean-runtime panic recovery layer. A Lean internal panic, generated unreachable, std::exit, or abort during a LeanSession call may terminate the process; see 06-panic-containment.md. No unwrap(), expect(), or panic! in non-test code unless a comment names a proof obligation that makes the call infallible.

Lean-to-Rust callbacks go through LeanCallbackHandle, not raw user-provided function pointers. The registry catches unwinding Rust panics before the C boundary and reports them as callback status plus a bounded LeanError; see 10-callback-registry.md.

Versioning and Compatibility

The supported Lean toolchain window, the in-tree raw-FFI policy, the header-digest policy, crate semver, and supported platforms. The single place to look when deciding whether a given Lean toolchain or host OS is supported. Each entry is a compatibility commitment; bumping any of them requires a versioned proposal, not a build fix.

Supported Lean toolchain window

lean-rs supports a contiguous window of Lean 4 stable releases plus the current upstream release candidate, enumerated in the SUPPORTED_TOOLCHAINS table. The table is the single source of truth; this document mirrors it for narrative context. As of 2026-05-23:

Lean does not always bump lean.h between point releases; rows that share a header share a digest. Extending the window is the bump procedure.

Lower bound: 4.26.0. A 2026-05-18 multi-toolchain sweep (scripts/test-all-toolchains.sh) covered 4.23.0 through 4.29.1. The six releases from 4.26.0 onwards pass clean (242 tests each, 0 failures); releases ≤ 4.25.x SIGSEGV inside lean_dec_ref_cold from L2 host-stack tests (lean-rs-host session/meta). The 4.30.0-rc2 row was added on 2026-05-23 after the standard layout-probe + symbol-probe gate; it is promoted to a stable row when upstream tags 4.30.0.

Policy.

• The window is contiguous and CI-tested in full. Every named release runs the workspace suite on ubuntu-latest and macos-latest; see .github/workflows/ci.yml.
• A consumer may build against any release in the window. The build script accepts any lean.h digest in the table; LeanRuntime::init re-validates against the same table as a backstop.
• Layout assumptions in lean-rs-sys/src/repr.rs are verified byte-identical across the entire window.
• A change in Lean’s C ABI—lean_object layout, ownership convention on lean_obj_arg / b_lean_obj_arg, the initializer protocol—at any point in the window is a contract change. Stop; do not paper over the ABI change with brittle wrappers.

Lake naming conventions. Two coexist in the window. The dylib loader and the Lake-project discovery probe both so Rust code is convention-agnostic.

Raw FFI source

Raw extern "C" declarations for the curated subset of lean.h, the pure-Rust mirrors of lean.h’s static inline refcount helpers, and the REQUIRED_SYMBOLS allowlist live in the published workspace crate lean-rs-sys (crates/lean-rs-sys/). Publication matches every peer *-sys crate and gives advanced users a stable raw-FFI escape hatch without forking the workspace.

There is no external lean-sys dependency. The split between lean-rs-sys and lean-toolchain:

• lean-rs-sys owns what the active Lean header says: extern declarations split by category, the pure-Rust refcount mirrors, the REQUIRED_SYMBOLS allowlist, the SUPPORTED_TOOLCHAINS window table, LEAN_VERSION, LEAN_RESOLVED_VERSION, LEAN_HEADER_PATH, LEAN_HEADER_DIGEST, and the cargo:rustc-link-* / rerun-if-changed=<lean.h> directives. Public types are opaque; layout structs are pub(crate). Its metadata-only feature is reserved for build-helper crates that need those constants without linking their own build-script binaries to libleanshared.
• lean-toolchain owns everything composed on top: the typed ToolchainFingerprint (which exposes is_supported()), the Lake fixture digest, layered link diagnostics, reusable build-script helpers, and required_symbols() returning lean_rs_sys::REQUIRED_SYMBOLS so the allowlist lives in one place.

See 05-raw-sys-design.md for the per-decision rationale behind lean-rs-sys’s shape.

Header digest

lean-rs-sys’s build script computes a SHA-256 over the discovered lean.h and looks it up in SUPPORTED_TOOLCHAINS. A miss fails the build with a bounded diagnostic naming the discovered digest and the full window; a hit emits cargo:rustc-cfg=lean_v_X_Y_Z (dots → underscores) so per-version divergences can be #[cfg]-gated, and bakes the resolved version into LEAN_RESOLVED_VERSION for runtime inspection.

The digest’s two jobs: (1) refuse to compile the Rust refcount mirrors against a lean.h whose layout has not been audited; (2) refuse to silently link a consumer’s binary against a different libleanshared than the one whose ABI the published lean-rs-sys was authored for. It is not a security boundary.

Crate semver

The workspace crates start at 0.1.0 and follow Cargo’s 0.x semver: any minor bump may break the public API; consumers should pin a single minor.

lean-rs-sys. The public surface is intrinsically unsafe—the curated extern "C" view of lean.h. The semver promise is about symbol names and signatures and the SUPPORTED_TOOLCHAINS window, not about safe behaviour. Lean’s header layout is not part of this surface—LeanObjectRepr is pub(crate) and may be updated to track Lean version bumps without breaking downstream code that uses the pub unsafe fn helpers.

lean-toolchain, lean-rs, lean-rs-host, lean-rs-worker. Standard 0.x semver over the curated re-exports at each crate root. Items inside lean-rs’s pub(crate) modules (runtime, abi) and the internal helper modules under module/ and host/ are not part of the public API; they can be renamed, moved, or collapsed without a minor bump as long as the curated re-exports keep their shape. lean-rs-host also depends on its bundled host shim package’s @[export] contract. lean-rs-worker’s semver surface is its supervisor, capability-builder, typed-command, row, diagnostic, timeout, and restart-policy API; private protocol frame shapes are not public API.

Lean shim packages. Same toolchain window. lean-rs bundles lean-rs-interop-shims for generic callback ABI helpers. lean-rs-host bundles lean-rs-host-shims plus the generic helper it needs for host progress.

Stabilization to 1.0 requires the RELEASE-READINESS contract and is not implicit.

Supported platforms

Supported and CI-tested:

• ubuntu-latest (x86_64 GNU/Linux).
• macos-latest (Apple Silicon).

Rust toolchain: stable, pinned by rust-toolchain.toml at the repo root.

Windows is an explicit non-goal at this stage. Adding it is itself a compatibility decision: a CI matrix entry, a documented build flag covering MSVC linking and the lean-rs-sys feature selection, and an update to this file. Other platforms (BSDs, embedded, WASM) are not supported.

Bumping the Lean version: process

The canonical procedure lives in docs/bump-toolchain.md. In summary:

1. elan toolchain install leanprover/lean4:vX.Y.Z.
2. Capture the new lean.h SHA-256 (the bump-toolchain doc has a one-liner).
3. Add a row to SUPPORTED_TOOLCHAINS (or extend an existing header-identical row).
4. Add the version to the matrix in .github/workflows/ci.yml.
5. Run scripts/test-all-toolchains.sh locally; commit; open PR.

If any ABI assumption breaks at the new release—lean_object layout shifts, a REQUIRED_SYMBOLS entry disappears, the Lake naming convention changes again—stop. File a Stop and discuss before patching around the diff with brittle wrappers.

lean-rs-sys Design Rationale

The per-decision rationale behind the lean-rs-sys crate’s shape. The charter and safety-model docs depend on it; the version-compatibility doc references it for the semver story. Revisiting any decision below is a contract change, not a build fix.

lean-rs-sys is the workspace’s raw FFI crate—the curated extern "C" view of lean.h plus the pure-Rust mirrors of lean.h’s static inline refcount helpers, the symbol allowlist, the header digest, and the link directives. Published as the foundation of the lean-rs-sys → lean-toolchain → lean-rs layering.

This document covers why. The what lives in the source tree.

What this design deliberately does not commit to

Pinned upfront so the rationale below reads as boundary-defending, not boundary-extending.

• Bindgen. Hand-written allowlist stays. Hand-written is auditable, has no clang dep, and is easy to gate on Lean version.
• Multi-Lean-version support beyond the contiguous supported range. See 02-versioning-and-compatibility.md.
• Windows. Per CI-LINT-BASELINE, Linux + macOS only.
• A proc-macro layer. REQUIRED_SYMBOLS is hand-maintained; tests/symbols_match.rs codegen is deferred until the allowlist reaches ~80 entries.

1. Why publish = true

Every comparable peer publishes its *-sys crate: pyo3-ffi, libgit2-sys, libsqlite3-sys, openssl-sys, mlua-sys, libz-sys, lua-sys, wasmtime-c-api. Reason: when a user hits a capability the safe layer does not yet wrap, depending on the *-sys crate directly (with full unsafe discipline) is dramatically friendlier than forking the workspace.

The “no raw escape hatch through lean-rs” policy that motivated publish = false is enforced inside lean-rs by the pub(crate) discipline around raw imports—independent of lean-rs-sys’s publication status. The minimum-unsafe public surface (see §2) means even opt-in users cannot accidentally corrupt the runtime by writing through *mut lean_object.

2. Why opaque public types + crate-private LeanObjectRepr

The naive choice would mirror pyo3-ffi’s pub struct PyObject { pub ob_refcnt, pub ob_type }: layout in public, fields direct. For lean-rs-sys published the right answer is different.

Public surface (src/types.rs):

#![allow(unused)]
fn main() {
use core::marker::{PhantomData, PhantomPinned};

#[repr(C)]
pub struct lean_object {
    _data: [u8; 0],
    _marker: PhantomData<(*mut u8, PhantomPinned)>,
}

pub type lean_obj_arg   = *mut lean_object;
pub type b_lean_obj_arg = *mut lean_object;
pub type u_lean_obj_arg = *mut lean_object;
pub type lean_obj_res   = *mut lean_object;
pub type b_lean_obj_res = *mut lean_object;
}

Standard Rust pattern for an FFI-opaque type pre-extern type (RFC 1861, unstable). The PhantomData<(*mut u8, PhantomPinned)> makes the type !Send + !Sync + !Unpin and prevents accidental copies; the precise idiom bindgen --blocklist-type emits.

Crate-private repr (src/repr.rs):

#![allow(unused)]
fn main() {
#[repr(C)]
pub(crate) struct LeanObjectRepr {
    pub(crate) m_rc:    i32,   // atomic ops via AtomicI32::from_ptr at call sites
    pub(crate) m_cs_sz: u16,
    pub(crate) m_other: u8,
    pub(crate) m_tag:   u8,
}
}

Plus subclass header reprs (LeanCtorObjectRepr, LeanArrayObjectRepr, LeanStringObjectRepr, LeanClosureObjectRepr, …). Each inline mirror (lean_inc, lean_dec, lean_ptr_tag, …) casts *mut lean_object → *mut LeanObjectRepr inside unsafe { ... } blocks with // SAFETY: comments naming the invariant.

Why this is the minimum-unsafe choice for a published crate

1. Downstream code that holds *mut lean_object literally cannot write (*ptr).m_rc = 0—the public type has zero fields visible. The only path to RC and tag inspection is through pub unsafe fn helpers, explicit and correct by construction.
2. Every cast from *mut lean_object to *mut LeanObjectRepr is a single unsafe operation prefacing a // SAFETY: block. The cast does not multiply unsafe scope.
3. Lean’s header layout becomes a crate-private invariant. Downstream semver decouples from lean.h: if Lean reorders header fields in 4.30, the crate updates LeanObjectRepr and re-publishes with a bumped Lean-version range; downstream code using lean_inc/lean_dec is unaffected.
4. Contrast with pyo3-ffi is intentional. CPython documents direct field access (Py_TYPE(op) does (*op).ob_type). Lean’s lean.h accesses fields only via inline helpers; no public Lean API names m_rc or m_tag. The opaque design is honest about Lean’s actual contract.

3. Why pure-Rust refcount mirrors (not a C shim)

The inline helpers in lean.h (lean_inc, lean_dec, lean_inc_ref_n, lean_dec_ref, friends—lean.h:536–563 of Lean 4.29.1) are static inline, not exported symbols. The crate must either mirror them in Rust or vendor a C shim built via cc.

Why a Rust mirror

• Inlines at the call site. A Rust mirror inlines into lean-rs’s Drop/Clone directly. A C shim defeats inlining across the FFI boundary unless cross-LTO is enabled (fragile, environment-dependent).
• Fewer build dependencies. No cc build-dep, no .c files in the tree, no per-platform compiler shenanigans.

Why atomic-relaxed everywhere

core::sync::atomic::AtomicI32 with Ordering::Relaxed on all loads, stores, and the MT-path fetch_sub, matching the memory_order_relaxed argument the static inline C source passes to atomic_fetch_sub_explicit. The cold path is the externally-exported lean_dec_ref_cold, which owns the actual deallocation and its own ordering decisions.

AtomicI32::from_ptr (stable since Rust 1.75) is the load-bearing primitive: the mirrors materialize a &AtomicI32 from *mut lean_object so the actual load/store/fetch_sub happens on a safe reference. Overflow guards on the single-threaded fast path use i32::strict_add / i32::strict_sub (stable since 1.91) so a refcount invariant breach surfaces as a panic in both debug and release; that drives the workspace rust-version = "1.91".

How drift is caught

The build script reads the discovered lean.h, computes SHA-256, and looks it up in SUPPORTED_TOOLCHAINS—the table of (versions, header_digest, missing_symbols) entries that names the v0.1.0 compatibility window. A miss fails the build with bounded diagnostics naming the discovered digest and the full window. The mirrors are byte-identical across every entry (verified empirically; the table commentary records the layout-stability proof). The mirrors plus the digest check are the entire trust boundary for the refcount fast path.

4. Why split-by-category module layout (~12 files)

For ~80–100 symbols, a single src/lib.rs (libgit2-sys / libz-sys style) becomes a 700-LOC scrolling exercise. A split-by-category layout (openssl-sys / pyo3-ffi style) is the right answer at this scale:

crates/lean-rs-sys/src/
  lib.rs       crate doc, lint allow, re-exports, REQUIRED_SYMBOLS
  consts.rs    LEAN_VERSION, header path, header digest, tag constants
  types.rs     opaque lean_object + ABI typedefs
  refcount.rs  Rust mirrors of lean_inc / lean_dec / friends
  object.rs    ctor / closure alloc, box, unbox, ptr_tag, is_scalar, casts
  scalar.rs    uint*/int*/usize/isize <-> Nat/Int conversions
  string.rs    lean_mk_string, lean_string_cstr, lean_string_size
  array.rs     lean_array_*, lean_sarray_*
  nat_int.rs   bignum dispatchers
  closure.rs   lean_alloc_closure, lean_apply_1..16
  io.rs        lean_io_result_*
  init.rs      lean_initialize, lean_initialize_runtime_module, threads
  external.rs  lean_alloc_external, lean_register_external_class
  repr.rs      pub(crate) struct LeanObjectRepr + subclass repr structs

Twelve files at 50–150 LOC each. Easier to navigate on docs.rs, easier to audit per category. Within each module the convention is “extern decls at top (link-checked), Rust mirrors below”; the per-file doc names the lean.h line range the module covers.

5. Why C-verbatim naming

Every peer *-sys preserves C names verbatim—PyObject, git_repository, lua_State, SSL_CTX. Reasons:

• Searchability. Users grep for lean_inc and find both lean.h and the binding in one shot.
• No bikeshedding. 1-to-1 mapping has no judgment calls.
• Higher-layer renaming is the right place for it. lean-rs’s safe layer wraps these under Rust-style names (LeanRuntime, LeanExpr, …); lean-rs-sys keeps raw names so the boundary is visible.

The crate root enables #![allow(non_camel_case_types)] and #![allow(non_snake_case)] as a consequence.

6. Why a REQUIRED_SYMBOLS allowlist plus a linkage test

The extern "C" blocks across src/*.rs are the authoritative declarations; pub const REQUIRED_SYMBOLS: &[&str] enumerates them as data for tooling:

• tests/linkage.rs takes the address of each entry; if any symbol is missing in libleanshared, the binary fails to link and the test fails.
• lean-toolchain’s required_symbols() returns lean_rs_sys::REQUIRED_SYMBOLS directly—the allowlist lives once.
• Future tooling (version-compatibility checks, documentation, the charter) can iterate the list without parsing source.

Hand-maintaining ~75 entries is acceptable; churn is low. A future tests/symbols_match.rs could grep the extern "C" blocks and assert equivalence if drift becomes a real problem.

7. Why a single-file build.rs and sha2 as the only build-dep

The script’s job is small:

1. Discover Lean (env vars → lean --print-prefix → fixture Lake env, in order, with bounded diagnostics on each miss).
2. Read <prefix>/include/lean/lean.h and compute SHA-256.
3. Look up the digest in SUPPORTED_TOOLCHAINS. On a hit, record the matched resolved version; on a miss, fail the build with the discovered digest and the supported window.
4. Emit cargo:rustc-env=LEAN_{VERSION,RESOLVED_VERSION,HEADER_PATH,HEADER_DIGEST}=… plus cargo:rustc-cfg=lean_v_X_Y_Z for the matched entry.
5. Emit cargo:rustc-link-* directives based on features (static vs dynamic, mimalloc). The default is dynamic (see §10).
6. Emit cargo:rerun-if-{env-changed,changed}=….

At ~150 LOC, a single build.rs is right. Splitting into a build/ directory (openssl-sys style) is overkill. sha2 is the sole runtime dependency; no bindgen, no cc, no pkg-config.

8. Minimum-unsafe discipline

1. #![allow(unsafe_code)] at the crate root only; no per-file silent allows.
2. Every pub unsafe fn carries a # Safety doc section naming pre-conditions (typically a Lean ABI invariant or a layout assumption pinned by LEAN_HEADER_DIGEST).
3. Every unsafe { ... } block carries a // SAFETY: comment naming the invariant.
4. No public pub fields on any FFI type. Layout access is exclusively through pub unsafe fn helpers that cast *mut lean_object → *mut LeanObjectRepr internally.
5. NonNull<lean_object> at API edges where Lean’s ABI guarantees non-null; raw *mut lean_object only where the C ABI permits null.
6. AtomicI32::from_ptr (Rust 1.75+) inside the refcount mirrors so the actual load/store/fetch_sub happens on a safe &AtomicI32.
7. No transmute; all pointer reshaping is .cast::<T>() or &raw mut with // SAFETY: justification.
8. Refcount and allocation-size arithmetic uses i32::strict_add / usize::strict_add / strict_mul (Rust 1.91+)—overflow panics in debug and release, surfacing invariant breaches instead of silently producing a wrong size or wrapped refcount.

9. As-built deviations

The sections above describe the approved design. Implementation surfaced these deviations:

• Default features are ["mimalloc", "dynamic"], not ["mimalloc", "static"]. The prompt’s static link set (Lean, Init, leanrt, leancpp, Lake) does not actually link a Lean stdlib symbol-using program without at least libStd.a and a specific archive order. The default switched to dynamic so the test binary links against libleanshared out of the box. The static feature is preserved for embedders who explicitly want it.
• The mimalloc feature is a no-op marker. Lean 4.29.1’s mimalloc is statically linked into libleanrt.a / libleanshared; no separate libmimalloc exists to link against. The feature stays as a marker downstream tooling can read and a hook for future toolchains that ship mimalloc separately.
• LeanObjectRepr::m_rc is i32, not AtomicI32. AtomicI32::from_ptr takes *mut i32; storing as plain i32 makes the cast ergonomic and keeps the layout byte-exact. Atomic semantics happen at the call site, not in the struct.
• Init symbols live in init.rs but not in lean.h. lean_initialize, lean_initialize_runtime_module, lean_initialize_thread, lean_finalize_thread, lean_setup_args are exported by libleanshared but not declared in lean.h. They appear in init.rs as extern "C" declarations with the standard runtime signatures. The LEAN_HEADER_DIGEST check does not gate them (it guards layout, not runtime entry points); REQUIRED_SYMBOLS plus tests/linkage.rs covers them instead.
• REQUIRED_SYMBOLS has ~75 entries (vs the ~50–80 estimate). Items the prompt prefigured as externs are actually static inline in 4.29.1 (lean_alloc_ctor_memory, lean_alloc_closure, lean_alloc_array). Those are mirrored in Rust and dropped from the allowlist; lean_alloc_object / lean_free_object (the real externs) are listed instead.
• Layout assertions for pub(crate) LeanObjectRepr and friends live in #[cfg(test)] mod tests inside src/repr.rs, not tests/layout.rs. Integration tests cannot see pub(crate) items; the unit-test module keeps internals internal without leaking a #[doc(hidden)] pub mod __test accessor.
• The digest-mismatch fixture test is documented, not automated. Verification step 6 in the prompt called for a build-time test that flips a lean.h byte and asserts failure. Automating it would require either an in-tree fixture sysroot or a noisy subprocess test; the procedure is documented for manual exercise in the crate’s README.md.
• MSRV is 1.91, originally planned at 1.85 for AtomicI32::from_ptr (1.75). Bumped to use strict_add / strict_sub / strict_mul (1.91) so refcount or size overflow panics in debug and release instead of silent wrap.
• Lint discipline. Doc lints (doc_markdown, missing_safety_doc, undocumented_unsafe_blocks, too_long_first_doc_paragraph, missing_inline_in_public_items, missing_panics_doc) are never silenced; every violation is fixed. Narrow module-level allows persist for clippy::inline_always (FFI mirror modules where always-inline is the design), clippy::struct_field_names (repr.rs—m_* mirrors C), and clippy::cast_possible_* / cast_sign_loss (scalar.rs—C ABI mandates the narrowing shape).

Cross-references

• Charter: 00-charter.md—Adopted shape.
• Safety model: 01-safety-model.md—Unsafe boundary.
• Version compatibility: 02-versioning-and-compatibility.md—Header digest, Bumping the Lean version.
• L1 safe surface: the lean-rs crate (typed FFI primitive). Crate docs at https://docs.rs/lean-rs.
• L2 opinionated stack: 03-host-stack.md—the lean-rs-host crate, what gets built on top of the L1 safe surface.

Concurrency and the Lean Task Runtime

The concurrency contract for lean-rs. Lean is per-thread; LeanRuntime is !Send; every handle inherits that structurally; thread attach is a public RAII type owned by lean_rs::runtime. The rest of the design follows.

Thread affinity

LeanRuntime contains a PhantomData<*mut ()>, so it is !Send + !Sync. Every safe handle on the public surface either holds &'lean LeanRuntime directly or transitively (through Obj<'lean>, which carries PhantomData<&'lean LeanRuntime>), and inherits the same restriction. The auto-trait inference is structural—there are no unsafe impl Send or unsafe impl Sync anywhere in the crate.

Handles covered:

• LeanRuntime, LeanThreadGuard<'lean>
• LeanHost<'lean>, LeanCapabilities<'lean, 'h>, LeanSession<'lean, 'c>
• LeanName<'lean>, LeanLevel<'lean>, LeanExpr<'lean>, LeanDeclaration<'lean>, LeanEvidence<'lean>
• SessionPool<'lean>, PooledSession<'lean, 'p, 'c>

Each is pinned at compile time by crates/lean-rs/tests/compile_fail/runtime_is_not_send_or_sync.rs. An accidental impl Send from a refactor is caught by the .stderr snapshot before the change can merge.

Why the 'lean parameter, on top of OnceLock

In practice the runtime resolves to &'static LeanRuntime: OnceLock makes it a process-once singleton, and no current caller binds 'lean to a non-static lifetime. The parameter forecloses one bug class OnceLock alone cannot catch—a handle outliving a scoped runtime view (e.g., a future per-task LeanRuntime). The cost is signature noise.

What can cross threads

Data types—types that carry information about a Lean result but no Lean refcount—are Send + Sync by auto-trait derivation and may travel freely:

• LeanCancellationToken (contains only Arc<AtomicBool>; it carries no Lean handle and is checked cooperatively by the worker thread).
• LeanError, LeanResult<T> (per LeanError’s Clone + Send + Sync derivation, with T: Send + Sync as the usual constraint).
• EvidenceStatus, LeanKernelOutcome<'lean> (the 'lean argument is a marker; the type carries no Lean refcount).
• ProofSummary (a bounded byte buffer).
• LeanDiagnostic, LeanPosition, LeanSeverity.
• SessionStats, PoolStats.

Typical workflow: a worker runs Lean work to completion inside its LeanThreadGuard scope, projects the result to one of these plain Rust types, and sends the projection back to a coordinator thread over a channel. Lean handles never leave the worker.

Cancellation is the asymmetric exception to “results travel back”: the coordinator sends a LeanCancellationToken clone into the worker before the operation starts, then may call cancel() from another thread. The session itself still stays on the worker. See 07-cooperative-cancellation.md.

Thread attach and detach

LeanThreadGuard<'lean> is the public RAII type owning one attach/detach pair. LeanThreadGuard::attach(runtime) attaches the calling OS thread (forwarded to lean_initialize_thread); the guard’s Drop detaches (lean_finalize_thread). Three rules:

1. Every OS thread that Lean did not start, and that calls into Lean, must hold a LeanThreadGuard for the duration of its Lean work.
2. The thread that called LeanRuntime::init does not need a guard; it is implicitly attached for the rest of its lifetime. (Lean’s own initialization runs on that thread; treating it as a “main” thread is the convention.)
3. A guard must be dropped on the same thread that attached it. The !Send claim on LeanThreadGuard makes that structural—the compiler refuses to let one cross a thread boundary.

Nested attaches are legal: a worker that re-enters attach (e.g., inside a callback) gets a second guard; the per-thread attach depth balances on the matching Drop.

Every host-call funnel (crate::module::LeanExported::call, which all typed Lean dispatches route through) inserts a debug-only debug_assert_attached. A worker that forgets its guard panics with a clear Rust message in debug; release builds compile the assertion away.

Task manager

The Lean task manager is required for any capability that runs Language.Lean.processCommands (notably LeanSession::kernel_check), which asserts g_task_manager on entry. LeanRuntime::init therefore starts the task manager as part of its process-once init sequence, after lean_initialize_runtime_module and lean_initialize.

Worker count defaults to Lean’s compiled-in heuristic (typically one per core). Override by setting LEAN_RS_NUM_THREADS to a positive integer before the first LeanRuntime::init call; the first call captures the value and later changes have no effect, because the task manager is process-lived and init is idempotent. Invalid values fall back to Lean’s default with a tracing::warn! against the lean_rs target.

Set LEAN_RS_NUM_THREADS when several Lean-using processes run side by side (CI test matrices, batch workers, multi-tenant services) so the sum of their pools does not oversubscribe cores. The workspace ships LEAN_RS_NUM_THREADS = "1" as a cargo [env] default; tests run under cargo nextest run with a 4-process cap, for at most 4 Lean workers across the suite. See docs/testing.md for the test-runner side.

The crate does not currently expose a programmatic with_workers(n) constructor; the env var is the single supported override. Adding a programmatic API later is a strict refinement.

The task manager is process-lived. lean-rs does not call lean_finalize_task_manager; Lean tears it down at process exit, like the runtime itself.

The Lean Task value type (Lean-level Task α) is intentionally not part of the public Rust surface. lean_task_* exists in lean.h but is not exposed through lean-rs-sys. Rust-side concurrency uses Rust primitives; Lean tasks are an internal implementation detail of capabilities that need them.

SessionPool under concurrency

SessionPool<'lean> is a per-thread free-list for LeanSession instances bucketed by their imports key. Interior mutability is RefCell<PoolInner<'lean>> + Cell<PoolStats>; combined with the inherited !Send + !Sync of LeanRuntime, the pool is firmly single-threaded.

Intended deployment: one pool per worker, all anchored to the shared &'static LeanRuntime returned by LeanRuntime::init. Workers acquire and release independently; the pool itself never crosses a thread boundary. Cross-thread session sharing is unsupported and prevented at compile time. If a workload needs more capacity than one pool can sustain, the answer is more workers (each with its own pool), not a shared pool.

Embedding in async runtimes (Tokio / smol / async-std)

Sync-first, with a dedicated bounded thread pool. Each worker holds a LeanThreadGuard for its lifetime and owns its own LeanHost / LeanCapabilities / SessionPool. Async code submits jobs to that pool via the runtime’s blocking-task primitive and receives back a Send-able Rust projection.

#![allow(unused)]
fn main() {
// One-time setup, off the async pool.
let runtime = lean_rs::LeanRuntime::init()?;
let lean_pool = tokio::runtime::Builder::new_multi_thread()
    .worker_threads(num_lean_workers)
    .on_thread_start(move || {
        WORKER_GUARD.with(|cell| {
            cell.borrow_mut()
                .replace(lean_rs::LeanThreadGuard::attach(runtime));
        });
    })
    .on_thread_stop(|| {
        WORKER_GUARD.with(|cell| { cell.borrow_mut().take(); });
    })
    .build()?;

// In async code:
let summary: lean_rs::ProofSummary = lean_pool
    .spawn_blocking(move || run_one_lean_job(/* ... */))
    .await??;
}

Two rules carry over from the sync API:

1. No Lean-derived value crosses an await. LeanSession, LeanExpr, etc. are !Send; the compiler will refuse. The programmer must arrange the work so a complete unit happens inside one spawn_blocking closure.
2. The return value must be Send + Sync Rust data. A LeanKernelOutcome or ProofSummary is the natural unit; raw handles are not.

No async helpers ship as part of lean-rs. The sketch shows what to wire up, not a published API.

Why not async-first

Making lean-rs itself async fn-shaped would push every Lean call through an executor poll, multiply the surface, and provide no benefit over the pattern above. Lean is synchronous inside a thread; the natural place to absorb that into an async service is at the thread boundary, not inside the binding crate. Embedders needing fine-grained async cancellation around a Lean call wrap the blocking task themselves—the building block is spawn_blocking, not yet-another Future.

Panic Containment

Lean internal panics are contained by a process boundary, not by a LeanSession state transition. If a kernel assertion, generated unreachable, runtime overflow panic, or panic! compiled with LEAN_ABORT_ON_PANIC=1 fires during a session call, the host process may terminate. Consumers that need to survive that failure class must run Lean work in a child worker process and treat worker exit as the recovery signal.

No LeanError::SessionPoisoned, LeanDiagnosticCode::SessionPoisoned, LeanRuntime::recycle, or in-process LeanSandbox API exists, and the sections below give the soundness argument for why.

Caller Contract

The public LeanSession methods keep the existing typed contracts for ordinary Lean failures:

The same rule applies to LeanSession::call_capability: if the called Lean export returns through its normal C ABI, lean-rs decodes it. If the export terminates the process or unwinds as a foreign exception through the non-unwinding C ABI, LeanSession does not recover.

Why The Boundary Is The Process

LeanSession dispatches through unsafe extern "C" function pointers resolved from Lake-built shared libraries. Rust’s std::panic::catch_unwind catches unwinding Rust panics in the same Rust runtime; it does not catch aborting panics, and it does not provide a sound recovery contract for foreign exceptions crossing a non-unwinding C ABI. The Rust Reference also classifies unwinding into Rust through the wrong FFI ABI as undefined behavior.

Lean’s runtime panic paths are not a single Rust-style unwind mechanism. Across the supported window two paths in the upstream sources cover the cases:

• runtime/object.cpp: lean_internal_panic prints and exits; lean_panic_impl aborts when LEAN_ABORT_ON_PANIC is set. As of Lean 4.30 (upstream PR #12539), lean_panic_impl additionally calls print_backtrace, which delegates demangling to the Lean-side @[export] lean_demangle_bt_line_cstr from Lean.Compiler.NameDemangling. See Decoupling from Lean’s panic-time runtime callbacks below.
• runtime/debug.h: lean_unreachable() throws Lean’s C++ unreachable_reached exception.

Those mechanisms bypass the error channel that LeanIo<T> decodes. A session-poisoning API would catch only a subset of the failures it claimed to contain, masking the rest behind a falsely-typed recovery.

Soundness Argument

After an internal Lean panic, lean-rs cannot prove enough to continue in the same process.

Reference counts. Obj<'lean> assumes each Rust-owned handle has one valid Lean reference and that Drop may later call lean_dec. If a panic or foreign unwind interrupts Lean while it is transferring or consuming owned C-ABI arguments, Rust cannot know which Lean references were incremented, decremented, or installed into another object.

Lean global state. Module initializer flags, interned names, imported environment tables, options, task-manager state, and runtime allocator state are process-global or runtime-global. A panic in the middle of a mutation leaves no public Lean recovery primitive that proves those globals are consistent.

The 'lean lifetime. LeanRuntime::init() creates the process-once anchor for every Obj<'lean> and semantic handle. There is no safe operation that invalidates all existing 'lean values, tears down Lean, and creates a fresh incompatible 'lean inside the same process.

The sealed meta::* registry. The Rust registry only proves that a request is routed to one of the pre-registered MetaM exports. It does not prove that the Lean elaborator state behind that export is valid after an internal panic.

SessionPool entries. A pool entry is an owned Lean.Environment handle. SessionPool::drain() can release cached environment references under normal execution, but it cannot validate that an environment returned from a partially panicked Lean call is semantically or refcount-wise intact.

The safe contract is therefore negative and explicit: process termination is the containment boundary for Lean internal panics. Use a child process when the application must continue.

Rejected Alternatives

Session poisoning with catch_unwind. Rejected. It would require wrapping every public LeanSession method, marking the session poisoned on a caught panic, and returning LeanError::SessionPoisoned thereafter. That does not cover abort, std::exit, LEAN_ABORT_ON_PANIC, or the C++ exception path from lean_unreachable(), and it cannot prove refcount or Lean-global integrity after a foreign unwind crosses the C ABI.

LeanSandbox child-process API. Valid architecture, not shipped. A child process is the right containment mechanism, but the IPC protocol needed to make it a LeanSession-shaped contract is a separate host product. Downstreams with service-level containment needs should run their own worker process around lean-rs today.

In-process runtime recycling. Rejected. Lean runtime state is process-bound, and lean-rs cannot prove all old 'lean values are gone before recreating the runtime. See Long-Session Memory for the lifetime argument.

Verification Fixture

crates/lean-rs-host/tests/panic_containment.rs re-runs its own test binary as a child process with LEAN_ABORT_ON_PANIC=1 and LEAN_BACKTRACE=0, then calls the fixture export lean_rs_fixture_panic_unit. The parent asserts that the child exits unsuccessfully. This keeps the normal test runner alive while pinning the documented process-level behavior.

The sanitizer workflow also runs this fixture under Linux AddressSanitizer.

Decoupling from Lean’s panic-time runtime callbacks

Lean 4.30 (PR #12539) rewrote the C runtime’s panic-time backtrace handler to call into a Lean-implemented demangler (@[export] lean_demangle_bt_line_cstr from Lean.Compiler.NameDemangling). The PR’s stated invariant is that this is safe because print_backtrace is only called from lean_panic_impl (soft panics), where the Lean runtime is expected to be in a normal execution state.

That invariant holds for the Lean compiler and lake projects, which always load the full compiler stdlib. It does not hold for embedders. A lean-rs-worker child process intentionally embeds a minimal Lean: it loads libleanshared.so plus a small capability dylib chain, and cannot guarantee that the modules a future Lean panic handler decides to call back into are initialized when user code panics. The observed symptom on Linux is that lean_panic_impl calls print_backtrace → lean_demangle_bt_line_cstr and hangs before reaching abort_on_panic(); the parent’s request times out instead of observing a fatal exit.

lean-rs-worker and the host-stack verification fixture therefore pin a structural boundary: no Lean code may run from the C panic handler in a worker child. The boundary is enforced with LEAN_BACKTRACE=0, which lean_panic_impl checks before calling print_backtrace:

if (g_panic_messages) {
    panic_eprintln(msg, size, force_stderr);                    // always
    char * bt_env = getenv("LEAN_BACKTRACE");
    if (!bt_env || strcmp(bt_env, "0") != 0) {
        panic_eprintln("backtrace:", force_stderr);
        print_backtrace(force_stderr);                          // <- entire C->Lean re-entry block
    }
}
abort_on_panic();

With LEAN_BACKTRACE=0 set, the panic message still prints to the child’s stderr and the abort still fires; only the backtrace generation (and any C→Lean callback inside it) is skipped.

LEAN_BACKTRACE=0 is chosen, not LEAN_BACKTRACE_RAW=1, for two reasons:

• Wider availability. LEAN_BACKTRACE is present in 4.26+; LEAN_BACKTRACE_RAW was introduced in 4.29.1 with the PR that wired in the Lean demangler. The supported toolchain window spans the older variable.
• Narrower dependency on upstream internals. LEAN_BACKTRACE_RAW=1 runs print_backtrace and only skips the demangler call. If a future upstream change adds another C→Lean callback elsewhere inside print_backtrace, LEAN_BACKTRACE_RAW would not protect against it. LEAN_BACKTRACE=0 skips the entire block, so the boundary survives upstream reshuffles to what print_backtrace does internally.

The LeanWorkerConfig docstring states the policy at the public surface. The supervisor’s Command::env defaults apply before any explicit LeanWorkerConfig::env(...) entries, so a caller who has independently arranged for the demangler module to be initialized can opt back into a demangled backtrace with .env("LEAN_BACKTRACE", "1").

In-process embedders that use LeanHost directly (not via worker) are not affected by this default — they own their own process environment, and the host shim’s import Lean transitively initializes Lean.Compiler.NameDemangling, so the panic-time demangler callback resolves cleanly. The worker child is the case that needs the explicit boundary.

Decoupling from the kernel’s core-dump pipe handler

LEAN_ABORT_ON_PANIC=1 turns a Lean internal panic into abort() → SIGABRT. The parent supervisor recognises that fatal exit by reading EOF on the child’s stdout and translating it to LeanWorkerError::ChildPanicOrAbort { exit }. That round trip is fast — unless the kernel suspends the dying child to feed its core image to a pipe-based core_pattern handler.

On GitHub Actions ubuntu-latest, the runner inherits Ubuntu’s default core_pattern, which pipes the core image to apport (or systemd-coredump on newer images). For a worker child that has loaded libleanshared.so plus a capability dylib chain, the kernel holds the dying process’s file descriptors open while it streams the image to the handler. Measured delays on the runner are 30–110 seconds; the supervisor’s 30-second per-request timeout fires first and the parent reports Timeout { operation, duration } instead of the typed fatal exit.

The contained workloads have no use for a core file: typed errors (ChildPanicOrAbort, Worker { code, message }) and the captured child stderr already cover the supported diagnostic surface. The fix is to suppress core dumps in every worker child: child::disable_core_dumps calls setrlimit(RLIMIT_CORE, {0, 0}) at the top of the child entry point so any subsequent SIGABRT terminates the process immediately, closing the IPC pipes and letting the parent observe EOF on normal IPC timescales. The same call is a Windows no-op (Windows does not use POSIX rlimits or core_pattern).

This boundary lives in the child binary rather than in LeanWorker::spawn because the policy belongs to “any process shipped as a lean-rs-worker child,” including downstream binaries written using run_worker_child_stdio. Spawning the child from a different supervisor (the private __test_support::WorkerProcess, a downstream service) still inherits the boundary because it is baked into run_stdio. No public API change is required.

Regression cover: crates/lean-rs-worker/tests/protocol.rs::fatal_exit_after_partial_rows_is_reported_as_worker_failure asserts that panic-to-fatal-exit detection completes within 10 seconds. Without the rlimit fix, the same test takes 30–110 seconds on Linux runners with apport.

References

• Rust std::panic::catch_unwind: https://doc.rust-lang.org/std/panic/fn.catch_unwind.html
• Rust Reference, panic and FFI unwinding: https://doc.rust-lang.org/stable/reference/panic.html
• Lean Reference, FFI ABI and initialization: https://lean-lang.org/doc/reference/latest/Run-Time-Code/Foreign-Function-Interface/
• Lean Reference, reference counting: https://lean-lang.org/doc/reference/latest/Run-Time-Code/Reference-Counting/

Cooperative Cancellation

lean-rs-host cancellation is cooperative. A caller creates a LeanCancellationToken, shares a clone with the thread that may request cancellation, and passes Some(&token) to a LeanSession operation. The operation checks the token before it enters Lean and, for token-aware bulk paths, between per-item dispatches. If the token has been cancelled, the operation returns LeanError::Cancelled with diagnostic code lean_rs.cancelled.

#![allow(unused)]
fn main() {
use std::thread;
use lean_rs_host::LeanCancellationToken;

let token = LeanCancellationToken::new();
let canceller = token.clone();

thread::spawn(move || {
    canceller.cancel();
});

// On the Lean worker thread:
// session.query_declarations_bulk(&names, Some(&token))?;
}

Already-collected bulk results are discarded. There is no partial-output return shape.

Cancellation is a control signal checked at host-owned boundaries. Progress events are observability signals delivered through the reusable interop callback substrate. Where a method uses a Rust per-item loop, progress reports and cancellation checks share the same item boundary.

What Is Checked

Every host operation that can enter Lean accepts Option<&LeanCancellationToken> as its final argument:

• LeanCapabilities::session
• SessionPool::acquire
• LeanSession::{query_declaration,list_declarations,list_declarations_filtered,declaration_source_range,declaration_type,declaration_kind,declaration_name}
• LeanSession::{elaborate,kernel_check,check_evidence,summarize_evidence}
• LeanSession::{run_meta,query_declarations_bulk,declaration_type_bulk,declaration_kind_bulk,declaration_name_bulk,elaborate_bulk,call_capability}

Some long-running methods also accept Option<&dyn LeanProgressSink> after the cancellation token. That progress sink is not a cancellation token. It may call token.cancel() on a shared token, but the session still observes cancellation only at the next host-controlled check point.

None preserves the existing non-cancellable path. In particular, query_declarations_bulk(..., None), declaration_*_bulk(..., None), and elaborate_bulk(..., None) keep their single Lean-side bulk dispatch.

Some(token) enables cancellation checks. For singular methods, the token is checked before each FFI dispatch point the Rust side controls. For bulk methods, the Rust side switches to a per-item loop and checks the token between items. That path is intentionally less batched: cancellation points require returning to Rust.

What Is Not Checked

The token does not interrupt work already running inside Lean. It cannot stop:

• one stuck isDefEq call that never returns to the host;
• a C-side kernel reduction that does not burn heartbeats;
• an @[export] symbol that runs its own long loop without checking heartbeats or returning to Rust;
• Lean runtime panics, aborts, std::exit, or foreign unwinds.

Use LeanElabOptions / LeanMetaOptions heartbeats for interpreter work that does burn heartbeats. Use a caller-level timeout or a worker-process boundary for work that may not return to a cooperative check point.

Threading Model

LeanCancellationToken is Clone + Send + Sync because it contains only an Arc<AtomicBool>. That does not make LeanSession cross-thread. Sessions, Lean handles, capabilities, pools, and runtimes remain !Send + !Sync and stay on the Lean worker thread.

The intended pattern is asymmetrical:

1. The worker thread owns the LeanSession and passes Some(&token) to the operation.
2. Another thread owns a clone of the token and calls cancel().
3. The worker observes cancellation at the next host-controlled check point and returns LeanError::Cancelled.

The token is one-way. Create a fresh token for the next operation.

Rejected Shapes

*_with_cancellation methods were rejected as a shallow duplicate API. They double the public surface while providing the same operation with one extra argument.

A session-wide cancellation wrapper was rejected because cancellation is an operation-level decision. A token may apply to one user request, not to the session’s whole imported environment.

Pre-emptive cancellation was rejected because the host cannot safely unwind or interrupt arbitrary Lean runtime work. Panic containment imposes the same boundary: when the host cannot prove Lean state and refcounts remain valid, the recovery boundary is a worker process. See 06-panic-containment.md.

Reusable Interop

lean-rs should make Lean/Rust interop feel closer to PyO3 or maturin in the places where Lean’s runtime model allows it: typed Rust calls into Lean exports, build helpers that hide Lake path rules, reusable callback handles, and worked downstream examples. It must not claim Python-style reflection. Lean does not provide a stable C API for looking up and invoking arbitrary Lean declarations by name; cross-language entry points are explicit @[export] ABI boundaries.

The architecture therefore keeps shims, but makes them fewer, deeper, and reusable. The goal is not “shimless” interop. The goal is a stable interop boundary that hides callback handles, trampoline safety, object conversion, and Lake wiring from downstream crates.

Chosen Boundary

The interop stack has five layers:

• lean-rs-sys owns raw Lean C runtime symbols and opaque raw types.
• lean-rs owns typed object ownership, exported-function calls, and callback handles.
• Generic Lean interop shims own reusable ABI helpers for callbacks and, when real callers need them, strings, names, and object plumbing.
• lean-rs-host owns theorem-prover host policy: sessions, declaration introspection, elaboration, kernel checking, and progress events.
• lean-toolchain owns Lake and build-script ergonomics.

This split keeps volatile decisions low in the stack. A callback handle’s lifetime, a trampoline’s panic boundary, or Lake’s dylib naming rules should be implemented once and reused. Higher layers should talk in their own terms: LeanSession, declaration filters, cancellation tokens, and progress events.

Rejected Designs

No shims. This design would require a Lean equivalent of Python’s reflective C API: runtime declaration lookup, dynamic invocation by name, and stable object introspection from C. A source survey of the Lean runtime found the opposite shape: Lean exposes explicit exported symbols and an internal runtime API, and theorem-prover operations such as elaboration, MetaM, and server-style workflows live in Lean code. Rust should not reconstruct those semantics through raw object layouts.

Host-specific shims only. The host-specific only design would keep all callback-bearing work in lean-rs-host. The current host shims are appropriate for host policy, but callbacks, progress, and downstream capability examples would each need the same lower-level machinery: opaque Rust handles, ABI trampolines, panic containment rules, reentrancy limits, and string/name conversion helpers. Repeating those details in every host feature would make each shim shallow and would expose ABI decisions to consumers.

Generic interop shims plus host policy. This is the chosen design. The generic shim layer supplies reusable mechanisms. lean-rs-host then builds theorem-prover policy on top without owning the callback substrate itself.

Progress Reporting

Progress is host policy, not a low-level callback primitive. LeanProgressSink reports LeanSession phases such as import, bulk-introspection progress, or kernel-check progress. It is implemented over the generic callback substrate.

That ordering prevents a host-only callback path from becoming the de facto interop API. The same substrate must serve downstream Lean extensions that do not use lean-rs-host.

Contract

New interop surfaces must pass the deep-module test:

• Public APIs expose Rust concepts that callers need, not raw callback pointers or Lake path policy.
• Generic mechanisms stay below host policy.
• Panic, abort, and reentrancy limits are documented at the callback boundary.
• Performance claims name the workload and measurement command.

The generic shim package is documented in 11-generic-interop-shims.md. The build-script helper path and cache contract are documented in 12-interop-build-and-link.md. The downstream recipe is documented in ../recipes/downstream-interop.md. Structured host progress is documented in 13-structured-progress.md. Shim packaging is crate-owned: lean-rs ships the L1 generic interop shims, and lean-rs-host ships the host shims it loads. The release contract and source-of-truth map are in 14-interop-release-contract.md.

Callback ABI Spike

The minimum Lean-to-Rust callback ABI that the public registry sits on top of. The registry itself is documented in 10-callback-registry.md.

ABI Shape

The test-only host shim export is:

lean_rs_interop_test_callback_loop : USize -> USize -> UInt64 -> IO UInt8

The first USize is an opaque Rust-owned handle. The second is a Rust function pointer. Lean does not call the function pointer directly. It calls lean_rs_interop_tick_callback_call, a tiny C helper linked into the shim dylib. The helper casts the second USize to:

uint8_t (*)(uintptr_t handle, uint64_t current, uint64_t total)

and invokes it with the opaque handle and integer payload.

This proves the reusable mechanism without requiring a process-global exported Rust symbol. The Rust test owns the handle and the trampoline function pointer; the shim only knows the stable C ABI shape.

The C helper source and Lean callback call primitive live in the generic lean-rs-interop-shims package bundled under crates/lean-rs/shims/. The host shim export remains as a compatibility test symbol and loops over the same C helper in the host crate’s bundled shim copy.

Thread And Reentrancy Contract

The callback runs synchronously on the Lean-bound thread. It must not re-enter a LeanSession or call another Lean export through the same runtime stack. Later public callback handles must preserve that rule at the API boundary.

The handle is opaque to Lean. In the spike it is a pointer to a test-local Rust probe whose lifetime covers the whole Lean call. The public registry replaces that test-local pointer with an RAII registration handle.

Panic Boundary

Rust panics must not unwind into Lean or across a non-unwinding C ABI. The test trampoline catches Rust panics before returning to the C helper and reports failure as a UInt8 status. Lean internal panics remain process-scoped; see 06-panic-containment.md.

The relevant rules are the Rust Reference’s FFI unwinding table and std::panic::catch_unwind: catch_unwind catches Rust unwinding panics, not aborts, and non-unwinding C ABI boundaries are not a recovery surface for foreign unwinds. Lean’s FFI model still uses explicit @[extern] and @[export] ABI boundaries.

Files

• Generic Lean helper: crates/lean-rs/shims/lean-rs-interop-shims/LeanRsInterop/Callback.lean
• C helper: crates/lean-rs/shims/lean-rs-interop-shims/c/interop_callback.c
• Host test export: crates/lean-rs-host/shims/lean-rs-host-shims/LeanRsHostShims/Interop.lean
• Rust fixture: crates/lean-rs/tests/callback_trampoline.rs
• Sanitizer job: .github/workflows/sanitizer.yml

Out of scope at this layer

The ABI proves event order and panic-boundary behavior. Two things are left to the public registry and to higher layers:

• object payload conversion beyond (current, total) integers;
• host progress events.

Callback Registry

lean-rs exposes a narrow Rust callback registry for Lean-to-Rust calls. This is an L1 primitive, not a LeanSession feature and not the worker-facing data streaming API. A callback handle is the low-level same-process mechanism used when an exported Lean function must push data into Rust before it returns. Worker-style callers should normally use lean-rs-worker typed commands and row sinks; the worker child may use callbacks internally, but parent callers do not receive or pass callback handles.

Public Shape

Rust code registers a closure for one sealed payload type:

#![allow(unused)]
fn main() {
let callback = lean_rs::LeanCallbackHandle::<lean_rs::LeanProgressTick>::register(|tick| {
    eprintln!("{}/{}", tick.current, tick.total);
    lean_rs::LeanCallbackFlow::Continue
})?;
let (handle, trampoline) = callback.abi_parts();
}

A Lean export that follows the callback ABI accepts the two values as USize:

opaque_handle : USize
trampoline    : USize

Lean treats both values as opaque and passes them to a payload-specific helper such as LeanRsInterop.Callback.Tick or LeanRsInterop.Callback.String. The helper invokes the Rust trampoline through its matching C symbol. Callers cannot supply their own trampoline function pointer through the public API.

Payloads

LeanCallbackHandle<P> is generic over P: LeanCallbackPayload, but LeanCallbackPayload is sealed. Downstream crates can use supported payloads; they cannot add new ABI shapes or decode raw Lean objects themselves.

The supported payloads are:

#![allow(unused)]
fn main() {
pub struct LeanProgressTick {
    pub current: u64,
    pub total: u64,
}

pub struct LeanStringEvent {
    pub value: String,
}
}

LeanProgressTick is the two-counter payload. It carries no host policy by itself; lean-rs-host interprets it as progress when reporting long-running session work.

LeanStringEvent copies a borrowed Lean String into an owned Rust String before user code runs. No Lean object lifetime escapes the trampoline. Trusted same-process line-oriented protocols can use it directly; see ../recipes/string-callback-streaming.md for a JSONL-like example.

Flow And Lifetime

Callbacks return LeanCallbackFlow. Continue lets the Lean-side callback loop continue; Stop asks Lean to stop cleanly and return LeanCallbackStatus::Stopped.

LeanCallbackHandle<P> is an RAII registration. Dropping it unregisters the id. Lean may call the handle only while the Rust value is alive. If a stale id is called after drop, the trampoline returns LeanCallbackStatus::StaleHandle instead of dereferencing freed Rust memory.

The handle is Send + Sync. The registered closure must be Fn(P) -> LeanCallbackFlow + Send + Sync + 'static because Lean may invoke it on the Lean-bound worker thread, and registry lookup clones an internal Arc before running the callback.

Panic And Reentrancy

Rust panics must not cross Lean or C frames. The registry trampoline catches unwinding Rust panics, records a LeanError with HostStage::CallbackPanic, and returns LeanCallbackStatus::Panic to Lean. Aborting Rust panics and Lean internal panics remain process-scoped.

Callbacks run synchronously on the Lean-bound thread. A callback invoked during a Lean call must not call back into the same LeanSession or re-enter the same Lean call stack. The registry is a one-way callback mechanism; it does not make the host session reentrant.

Diagnostics

The trampoline returns LeanCallbackStatus as a UInt8 status:

For Panic, callers can inspect LeanCallbackHandle::last_error() while the handle is still alive. The recorded error has diagnostic code lean_rs.internal and stage CallbackPanic.

Files

• Registry: crates/lean-rs/src/callback.rs
• Generic Lean helpers: crates/lean-rs/shims/lean-rs-interop-shims/LeanRsInterop/Callback/Tick.lean and crates/lean-rs/shims/lean-rs-interop-shims/LeanRsInterop/Callback/String.lean
• Tests: crates/lean-rs/tests/callback_registry.rs

Generic Interop Shims

lean-rs-interop-shims is the reusable Lean package below lean-rs-host-shims. It contains ABI helper code that belongs to Lean/Rust interop itself, not to the theorem-prover host session model.

Package Boundary

The packaged L1 copy lives under crates/lean-rs/shims/lean-rs-interop-shims/. lean-rs-host carries its own bundled copy under crates/lean-rs-host/shims/lean-rs-interop-shims/ so the host crate can build and load its shims without reaching into another crate’s source directory at runtime. Its public Lean namespace is LeanRsInterop.

Current modules:

• LeanRsInterop.Callback.Tick: tick callback helper for LeanCallbackHandle<LeanProgressTick>.
• LeanRsInterop.Callback.String: string callback helper for LeanCallbackHandle<LeanStringEvent>.
• LeanRsInterop.Callback: roll-up module that imports both payload-specific helper namespaces.

Name, byte, and object helpers belong in this package when a prompt adds a real caller. They are not present yet, because unused helpers would widen the shim surface without hiding any current complexity.

Callback Helper

The callback helpers own the reusable ABI mechanism:

LeanRsInterop.Callback.Tick.call : USize -> USize -> UInt64 -> UInt64 -> BaseIO UInt8
LeanRsInterop.Callback.Tick.loop : USize -> USize -> UInt64 -> IO UInt8
LeanRsInterop.Callback.String.call : USize -> USize -> @& String -> BaseIO UInt8
LeanRsInterop.Callback.String.loop : USize -> USize -> Array String -> IO UInt8

The first USize is an opaque Rust callback handle. The second is the Rust trampoline value returned by LeanCallbackHandle::abi_trampoline(). The tick helper calls lean_rs_interop_tick_callback_call, which delivers a (current, total) payload. The string helper calls lean_rs_interop_string_callback_call, which delivers a borrowed Lean String payload. Both helpers return the UInt8 status produced by the Rust trampoline. The raw trampoline signature is crate-owned; Lean code should only pass the opaque values through the payload-specific helpers. The loop functions are small conveniences used by downstream-style fixtures.

Lean code treats the handle and trampoline as opaque tokens. Lifetime, reentrancy, and Rust panic containment are Rust-side registry contracts; see 10-callback-registry.md.

Relationship To Host Shims

lean-rs-host-shims still owns the 28 + 6 lean_rs_host_* theorem-prover policy symbols. Host-specific environment queries, elaboration, kernel checking, and MetaM services stay out of LeanRsInterop.

The host compatibility export is loaded from the host dylib directly, so it keeps a local Lean loop and compiles the bundled generic package’s C helper source into the host shared facet.

The host package keeps its test export:

lean_rs_interop_test_callback_loop : USize -> USize -> UInt64 -> IO UInt8

That export loops over the same lean_rs_interop_tick_callback_call C helper used by LeanRsInterop.Callback.Tick.call. This preserves the Rust test symbol while moving the callback C helper source into the generic package.

Downstream Fixture

fixtures/interop-shims/ is a small Lake package that depends on lean-rs-interop-shims without importing lean-rs-host-shims. Its LeanRsInteropConsumer.Callback module exports a plain addition function, a tick callback loop, and a string callback loop through the generic helpers. The fixture verifies that downstream capability packages can use typed exports and generic callbacks without taking a host session dependency.

Build commands:

cd crates/lean-rs/shims/lean-rs-interop-shims && lake build
cd fixtures/interop-shims && lake build

Rust consumers should not compute the resulting dylib paths by hand. Use lean_toolchain::build_lake_target for both the generic shim target and the consumer target; see 12-interop-build-and-link.md and crates/lean-rs/examples/interop_callback.rs. The consumer-facing recipe is docs/recipes/downstream-interop.md.

Non-Goals

The package is not a broad Lean standard library for Rust interop. It should grow only when a real lean-rs caller needs a helper that would otherwise duplicate ABI, ownership, or conversion rules across packages.

Interop Build And Link

lean-toolchain owns the build-script path for downstream crates that compile Lake shared-library targets. Callers name the Lake project root and target; they do not construct .lake/build/lib paths or reimplement Lake’s package-name mangling.

Build Script Contract

Use CargoLeanCapability for downstream crates that ship Lean source:

fn main() -> Result<(), Box<dyn std::error::Error>> {
    lean_toolchain::CargoLeanCapability::new("lean", "MyCapability")
        .package("my_app")
        .module("MyCapability")
        .build()?;
    Ok(())
}

The helper emits the Lean link-search, link-lib, runtime rpath, Cargo rerun directives, a deterministic manifest compile-time environment variable, and a compatibility dylib-path variable:

cargo:rustc-env=LEAN_RS_CAPABILITY_MY_CAPABILITY_MANIFEST=<manifest path>
cargo:rustc-env=LEAN_RS_CAPABILITY_MY_CAPABILITY_DYLIB=<built dylib path>

It runs lake build MyCapability:shared, resolves Lake’s supported dylib naming conventions, writes a self-describing artifact manifest, and returns BuiltLeanCapability for build scripts that want to inspect the result. The manifest is the canonical runtime handoff for shipped crates; the direct dylib path remains a lower-level compatibility path.

Lower-level helpers remain available for custom build flows:

• emit_lean_link_directives_checked emits only Lean link directives and returns typed LinkDiagnostics on discovery failure.
• emit_lean_link_directives preserves the warning-on-failure behavior.
• build_lake_target builds one Lake shared-library target and emits Cargo rerun directives.
• build_lake_target_quiet uses the same cache and path resolver without emitting Cargo directives; lean-rs-host uses it when it materializes bundled shims at runtime.

build_lake_target emits cargo:rerun-if-changed lines for the Lake files and Lean source files it scans. It captures Lake stdout and stderr, so stdout stays limited to Cargo directives and caller-chosen cargo: lines.

discover_lake_modules is the runtime discovery companion for higher-level planners. It resolves the Lake root, discovers lean_lib module roots, enumerates source modules deterministically, and returns source-set fingerprints without building a shared library. lean-rs-worker uses that general discovery output for import-set planning; downstream crates should not reimplement Lake source-root or module-path conventions.

Human cache diagnostics go to stderr:

lean-toolchain: cache hit for Lake target `LeanRsInterop` in ...; using ...
lean-toolchain: cache miss for Lake target `LeanRsInterop` in ...; running `lake build LeanRsInterop:shared`

Cache Key

The cache key is local to the Lake project:

• SHA-256 of lake-manifest.json;
• target name and Lake package name;
• count of scanned source files;
• maximum mtime of lakefile.lean, lakefile.toml, lean-toolchain, and every *.lean file below the project root, excluding .lake/.

A hit is accepted only when the cache key matches and the expected dylib exists. Cache write, manifest, traversal, and output-resolution failures are LinkDiagnostics::LakeOutputUnresolved.

Diagnostics

The helper path reports typed failures:

• MissingLean, MissingHeader, MissingLib, UnsupportedToolchain, and VersionMismatch from Lean toolchain discovery.
• LakeUnavailable when the lake executable cannot be started.
• LakeTargetMissing when the target is not declared as a lean_lib.
• LakeBuildFailed when lake build <target>:shared exits unsuccessfully.
• LakeOutputUnresolved when the manifest, cache, source scan, or expected dylib path cannot be resolved.

Each diagnostic renders as one line, so callers may print it through cargo:warning= or return it from build.rs.

Generic Interop Example

crates/lean-rs/examples/interop_callback.rs builds two Lake targets through the helper:

• crates/lean-rs/shims/lean-rs-interop-shims target LeanRsInterop;
• fixtures/interop-shims target LeanRsInteropConsumer.

The example opens the generic shim dylib globally, opens the downstream-style consumer dylib, calls an ordinary Lean export from Rust, and invokes a Lean callback loop through LeanCallbackHandle. It uses no lean-rs-host session API.

Run it twice to see the cache miss and cache hit paths:

cargo run -p lean-rs --example interop_callback
cargo run -p lean-rs --example interop_callback

The canonical shipped-crate recipe is docs/recipes/ship-crate-with-lean.md. The advanced same-process callback recipe is docs/recipes/downstream-interop.md.

Scope

The helper builds Lake lean_lib shared facets for the host platform. It does not cross-compile, build executables, or publish Lake packages. The generic and host shim sources are bundled with their owning Rust crates; this helper is the path those crates and downstream examples use to materialize the dylibs.

Structured Progress

lean-rs-host progress is a host-level observation channel for long-running LeanSession calls. It is built on the L1 callback registry from lean-rs and the generic lean-rs-interop-shims callback helper. The host crate owns the policy: phase names, totals, cancellation checkpoints, and which session methods report events.

Public Contract

Long-running host methods accept a final progress: Option<&dyn LeanProgressSink> after their existing cancellation parameter. None is the fast path: no callback handle is allocated, no progress shim is called, and bulk methods keep their single-dispatch shape. Some(sink) registers a temporary callback handle for the one call and drops it before the method returns.

The temporary handle is LeanCallbackHandle<LeanProgressTick>. The bridge converts that L1 tick payload into a host LeanProgressEvent; it does not expose LeanStringEvent or any downstream streaming policy through the host progress surface.

LeanProgressEvent contains:

• phase: &'static str: a stable method-local phase label;
• current: u64: a phase-local counter;
• total: Option<u64>: a known phase-local bound when cheap;
• elapsed: Duration: time since that phase began.

Events are delivered synchronously on the Lean-bound worker thread. A sink must not call back into the same LeanSession or re-enter the same Lean call stack. Expensive UI, logging, or IPC work should be queued by the sink and handled on a different thread.

Rust panics from progress sinks are contained by the callback boundary. The session method returns LeanError::Host with stage CallbackPanic and code lean_rs.internal. Lean internal panics remain process-scoped; see 06-panic-containment.md.

Reporting Points

Progress is phase-granular, not a promise that every Lean suboperation reports. The current host surface reports progress for:

• LeanCapabilities::session and SessionPool::acquire on fresh imports;
• LeanSession::query_declarations_bulk;
• LeanSession::{declaration_type_bulk,declaration_kind_bulk,declaration_name_bulk};
• LeanSession::elaborate_bulk;
• LeanSession::list_declarations_filtered;
• LeanSession::kernel_check.

Bulk methods with progress = Some and cancellation = None use Lean-side progress shims so they still perform one bulk dispatch. Bulk methods with both progress and cancellation use Rust per-item loops where a per-item singular path exists, so cancellation can be observed between items and partial output can be discarded. list_declarations_filtered, fresh import, and kernel_check do not have a Rust per-item equivalent; cancellation is checked before dispatch and then again only after Lean returns.

Empty bulk input returns an empty vector, records no FFI dispatch, and emits no progress event.

Relationship To Tracing And Cancellation

tracing spans describe call boundaries and are useful for logs, profiles, and post-hoc diagnostics. Progress events are a caller-supplied in-process callback for live user feedback such as phase=query_declarations_bulk current=4200 total=5000. Neither replaces the other.

Cancellation is a control signal. Progress is an observation signal. Where a method uses a Rust per-item loop, the cancellation check and progress report happen at the same item boundary. A progress sink may call token.cancel() on a shared LeanCancellationToken; the method observes that token at the next host-controlled cancellation check.

ABI Boundary

The host shims expose additive progress variants returning IO (Except UInt8 α). The UInt8 is the L1 LeanCallbackStatus byte. Rust decodes Except.ok as the method result, maps Panic through the callback handle’s stored error, and maps StaleHandle, WrongPayload, and Stopped to internal host invariant failures. Host progress is one-way: unlike a generic L1 callback loop, a progress sink does not define stop semantics. Existing no-progress shim symbols and signatures are unchanged.

LeanCapabilities builds the crate-bundled generic interop and host shim Lake targets on demand, then opens the generic interop shim dylib globally before opening the host shim dylib. This anchors the generated LeanRsInterop.Callback.Tick initializer that host progress shims import.

Interop Release Contract

The reusable interop stack is stable enough for 0.1.x consumers when they stay inside the documented boundaries: explicit Lean exports, typed Rust calls, crate-owned callback handles, bundled shim packages, and lean-toolchain build helpers. The model is close to PyO3/maturin in the parts Lean exposes: a Rust crate can build a Lean shared-library target, load it, call typed exports, and pass an opaque Rust callback handle back into Lean. It is not Python-style reflection.

Source Of Truth

Consumer-facing contracts live in these documents:

• ../recipes/downstream-interop.md: L1 interop without lean-rs-host.
• ../recipes/string-callback-streaming.md: L1 same-process Lean-to-Rust string callbacks without lean-rs-host.
• ../recipes/worker-capability-runner.md: the worker-facing command path for live rows, diagnostics, terminal summaries, timeouts, and cycling.
• 03-host-stack.md: L2 LeanHost / LeanCapabilities / LeanSession surface and host method signatures.
• 10-callback-registry.md: callback handle lifetime, panic, and reentrancy rules.
• 11-generic-interop-shims.md: generic Lean shim ownership.
• 12-interop-build-and-link.md: build_lake_target cache, diagnostics, and Cargo output rules.
• 13-structured-progress.md: LeanProgressSink semantics.
• ../lean-rs-host-capability-contract.md: fixed host shim symbol contract.

Implementation notes, spike rationale, and rejected designs remain in 08-reusable-interop.md and 09-callback-abi-spike.md. They explain why the current boundary exists, but the documents above are the release contract consumers should follow.

What The Stack Provides

lean-rs provides the L1 primitive: a LeanRuntime, loaded LeanLibrary / LeanModule handles, typed LeanExported calls, semantic object handles, structured errors, and LeanCallbackHandle<P> for synchronous same-process Lean-to-Rust callbacks. Callback handles carry only opaque ABI values and a crate-owned trampoline; downstream code does not pass arbitrary function pointers to Lean. Payloads are a sealed family owned by lean-rs; current payloads are LeanProgressTick and LeanStringEvent. This is the mechanism layer. Worker-class interfaces should expose lean-rs-worker typed commands and row sinks instead of callback handles.

lean-toolchain provides the build-script path: link directives for the active Lean toolchain and build_lake_target for Lake shared-library targets. It owns Lake dylib naming, cache metadata, Cargo rerun directives, and typed link/build diagnostics.

lean-rs-host provides theorem-prover policy above L1: sessions, imports, declaration introspection, source ranges, filtered listing, elaboration, kernel checking, bounded MetaM, pooling, cooperative cancellation, and structured progress. It ships the host and generic shim sources it needs, builds them on demand, and opens them beside the consumer capability dylib.

lean-rs-worker provides the process-boundary product interface for worker-style tools: builder-managed capability startup, typed commands, live rows, diagnostic sinks, terminal summaries, request timeouts, and worker cycling. It may use L1 callbacks inside the child, but the parent-facing API is worker IPC, not cross-process callbacks.

What It Does Not Provide

The stack does not discover or invoke arbitrary Lean definitions by reflection. Every cross-language entry point is an explicit @[export] with a supported ABI shape.

The stack does not make Lean internal panics recoverable in-process. Rust callback panics are caught at the callback trampoline boundary; Lean panic!, abort, std::exit, and foreign unwinds remain process-scoped.

The stack does not provide cross-process callback handles. Handles are valid only in the process that registered them and only while the Rust LeanCallbackHandle is alive.

The stack does not require new callback payloads for worker JSON row streaming. Worker rows already travel over the worker protocol as JSON or validated raw JSON; callback payload expansion is only for same-process L1 interop needs.

The stack is not shimless. The release boundary is fewer, deeper, crate-owned shims: generic interop shims for callbacks and host shims for theorem-prover policy.

Release Gates

Before a release that changes interop or host progress, run:

cargo run -p lean-rs --example interop_callback
cargo run -p lean-rs --example string_streaming
cargo run -p lean-rs-host --example progress
cargo run -p lean-rs-worker --example worker_capability_runner
cargo test -p lean-rs --test callback_trampoline -- --nocapture
cargo test -p lean-rs --test callback_registry -- --nocapture
cargo test -p lean-rs-host --test progress -- --nocapture
cargo test -p lean-rs-worker --test streaming_runner -- --nocapture
cargo test -p lean-rs-worker --test typed_command -- --nocapture
cargo bench -p lean-rs-host --bench session -- \
  host::session::declaration_kind_bulk_vs_loop/bulk_5000 --baseline <saved-baseline>
cargo bench -p lean-rs-worker --bench row_payload -- --baseline <saved-baseline>
cargo bench -p lean-rs-worker --bench worker_capability -- --sample-size 10

The sanitizer workflow must continue to run the callback trampoline, callback registry, panic containment, host progress, and worker fatal-exit fixtures on Linux ASan. Public API baselines under ../api-review/ are regenerated in the same commit as any intentional public surface change.

Callback Payloads

The original two-counter callback payload is a progress tick. It was enough to prove the callback handle, trampoline, stale-handle, panic, and reentrancy contracts, but it is not a general Lean-to-Rust callback payload model.

The next callback boundary keeps the same deep-module rule as the existing L1 registry: lean-rs owns callback handle lifetime, trampoline safety, payload decoding, panic containment, stale handles, and wrong-payload handling. Callers should not learn raw Lean object lifetimes, refcount rules, or callback ABI details to receive a payload.

Designs Considered

Single enum payload. One callback handle could accept an enum such as Tick | String | Bytes. This keeps one public handle type, but it makes the handle less precise. Every callback site would carry variants it does not accept, and a Lean-side wrong payload would become normal runtime branching instead of a boundary error. Progress reporting would also remain visible in the low-level payload vocabulary.

Fully user-defined payloads. Downstream crates could implement a public LeanCallbackPayload trait. That would look flexible, but it would push the wrong complexity upward. A sound implementation would have to know how Lean objects cross the ABI, when strings are retained or copied, how wrong payloads are detected, and which panic path is allowed through the trampoline. Those are registry concerns, not consumer concerns.

Sealed typed payload family. This is the chosen design. lean-rs owns the supported payload shapes, and a callback handle registers one shape at a time:

#![allow(unused)]
fn main() {
LeanCallbackHandle<P: LeanCallbackPayload>
}

LeanCallbackPayload is sealed. Downstream crates can use supported payloads, but they cannot add ABI shapes by implementing the trait themselves. This keeps the public API general enough for current use cases without turning callback payload decoding into a user extension point.

Initial Payloads

The first two payloads are:

#![allow(unused)]
fn main() {
pub struct LeanProgressTick {
    pub current: u64,
    pub total: u64,
}

pub struct LeanStringEvent {
    pub value: String,
}
}

LeanProgressTick carries the existing counter payload. lean-rs-host continues to own progress policy: phase names, elapsed time, cancellation checkpoints, and which LeanSession methods emit events. The host layer may map a LeanProgressTick into LeanProgressEvent, but progress is not the L1 callback abstraction. It is an observability/control signal, not a data row.

LeanStringEvent is the next useful L1 payload. It supports downstream same-process line-oriented protocols: Lean can emit one encoded line at a time, Rust receives owned strings, and neither side has to tunnel through subprocess stdout. Worker-style tools should not expose this handle to parent callers; lean-rs-worker turns child-local callbacks into typed worker rows when a process boundary is needed. The runnable L1 proof is ../recipes/string-callback-streaming.md.

Byte arrays and arbitrary Lean-object callbacks are deferred. They should land only when a measured same-process L1 consumer needs them, because each payload adds ABI, ownership, and diagnostics surface area. Worker JSON/raw-JSON rows do not require new callback payloads.

Error Boundary

The typed registry must distinguish these cases:

• the callback ran and wants Lean to continue;
• the callback ran and asks Lean to stop;
• Lean called a stale handle;
• Rust contained a callback panic;
• Lean called a handle with the wrong payload shape.

The public status vocabulary should express those outcomes without exposing raw pointers or Lean object references. Wrong-payload handling belongs in lean-rs because the registry knows the payload type associated with each handle.

Relationship To Existing Docs

10-callback-registry.md documents the implemented typed registry. The counter event is LeanProgressTick, and string callbacks use LeanCallbackHandle<LeanStringEvent>.

13-structured-progress.md remains host policy. Its progress sink is implemented over LeanProgressTick, not a general callback event.

14-interop-release-contract.md remains useful for the interop stack as a whole: explicit exports, build helpers, callback handles, bundled shims, and examples. The callback payload part of that release contract is the narrow piece being revised.

Loader And Artifact Boundary

The v0.1.1 release validated the worker foundation, but it also exposed a separate source of fragility: shipping Lean shared libraries is still too easy to do correctly only by accident. A caller should not have to know which dylib must be opened first, which one needs global symbols, how long a transitive dependency handle must remain alive, which environment variables the platform loader consults, or why docs.rs builds without Lean installed.

Those details are real, and they are volatile. They belong behind the lean-rs crate boundaries, not in every downstream build script, test helper, or worker launcher.

Chosen Boundary

The shipping stack has three responsibilities:

CargoLeanCapability artifact description
    -> LeanCapability bundle loader
    -> LeanWorkerCapabilityBuilder / LeanWorkerPool

• lean-toolchain owns the build artifact description. It builds the Lake shared-library target, resolves Lake’s dylib naming, emits Cargo rerun and link directives, and records enough artifact metadata for runtime code to reopen the same capability without rediscovering Lake output conventions. Release gates also simulate docs.rs from normalized crate tarballs with Lean, Lake, and Elan hidden from PATH, so package drift fails before crates.io receives immutable uploads.
• lean-rs owns runtime loader lifetime and symbol visibility. It opens the capability and any dependent Lean dylibs in the required order, keeps those handles alive for the full capability lifetime, preflights the manifest and artifacts into stable diagnostics, initializes the requested module, and hides platform loader differences.
• lean-rs-worker owns the process boundary. It locates and starts the app-owned worker child, builds the child environment, opens the capability in the child, reports bootstrap diagnostics, and keeps protocol pipes private.

Callers still know their own Lake package and root module, exported command names, typed request and row schemas, and whether the workload should run in process or behind worker isolation. Those are application decisions. Loader order, RTLD_GLOBAL, LD_LIBRARY_PATH, DYLD_*, Lake .lake/build/lib layout, docs.rs no-Lean behavior, and worker protocol pipes are not.

Rejected Designs

Caller-managed loader order. Rejected. It would make every user understand which Lean dylibs are dependencies, which ones must be opened globally, and how long each handle must stay alive. That repeats the same fragile dynamic-loader contract at every call site and test fixture.

Scattered helper fixes. Rejected. Test-only handle leaks, local LD_LIBRARY_PATH workarounds, special docs.rs branches in individual build scripts, and one-off worker child path probes can fix one failure at a time, but they keep the volatile knowledge duplicated. The next platform or package layout change would create another incident.

Deep loader/artifact boundary. Chosen. The build helper records the artifact; the runtime loader opens the complete bundle and anchors it; the worker builder transports that bundle into an isolated child process. Each layer has a different abstraction and hides a distinct kind of complexity.

Brittleness Classes

Lean Process-Global State

Lean runtime initialization, imported modules, interned names, persistent objects, allocator state, and module initializers are process-scoped. Dropping a Rust wrapper does not necessarily undo those effects. lean-rs-host exposes trusted in-process work; lean-rs-worker remains the production boundary for panic containment and memory reset.

Dynamic-Loader Symbol Visibility

Lean-generated shared libraries can reference symbols emitted by imported Lean libraries. On ELF platforms, later libraries may need earlier libraries to have been opened with globally visible symbols. On macOS the loader can appear more forgiving, which makes Linux-only failures easy to miss. Normal callers should not choose global visibility manually.

Transitive Dylib Lifetime

Opening a dependency globally is not enough if the Rust handle is dropped while another Lean dylib still relies on its symbols. The loader boundary must anchor dependent handles for as long as the capability can execute code that depends on them. Test-only leaks are a symptom that lifetime belongs in the loader abstraction.

docs.rs Builds Without Lean

docs.rs builds crate documentation in an environment where Lean, Lake, and Elan may be absent. Published crates must make documentation builds independent of a local Lean installation. A docs.rs guard is not a substitute for checking package contents and build behavior before publishing.

crates.io Package Drift

Published tarballs are immutable. A missing template, shim, README, benchmark, lean-toolchain, lakefile.lean, or generated doc baseline cannot be repaired in-place after release. The package boundary must include explicit contents checks so local builds, docs.rs builds, and downstream builds see the files the docs describe.

Worker Child Bootstrap Environment

Worker applications ship an app-owned worker child. The parent must find that binary, pass capability artifact paths, preserve only the environment needed by Lean and the worker protocol, and report startup failures with actionable diagnostics. Callers should not debug child pipes, inherited environment drift, or dependency-binary lookup rules.

Crate Responsibilities

lean-toolchain

lean-toolchain hides:

• Lean and Lake discovery;
• lake build <target>:shared;
• Lake shared-library naming across supported toolchains;
• Cargo rerun directives and link directives;
• package include expectations for Lean sources and Lake metadata;
• artifact metadata such as package, module, dylib path, search roots, toolchain fingerprint, and dependency dylibs known at build time.

The lower-level build_lake_target and raw link-directive helpers remain for advanced build systems. They are not the canonical shipped-crate path.

lean-rs

lean-rs hides:

• LeanLibrary handle lifetime;
• dependency open order;
• global symbol visibility;
• manifest preflight and repair hints;
• module initializer symbol names and sequencing;
• platform loader differences;
• nullary Lean global-vs-function export classification.

LeanCapability is the normal same-process runtime surface for shipped capabilities. LeanCapabilityPreflight is the doctor-style surface for checking a manifest-backed capability before opening it. LeanLibrary::open and LeanLibrary::open_globally remain public for advanced L1 interop and focused tests, but they are escape hatches: using them means the caller has chosen to manage loader details explicitly.

lean-rs-worker

lean-rs-worker hides:

• app-owned worker child lookup;
• child environment construction;
• capability startup inside the child;
• bootstrap and capability diagnostics;
• request timeouts, restart policy, and process isolation;
• worker protocol frames, pipes, and child lifecycle details.

The worker builder and pool should consume the same artifact description as the same-process loader. Worker parent-facing examples must not ask callers to open Lean dylibs, set loader paths, or pass callback handles across the process boundary.

Normal And Advanced Paths

Use the highest-level surface that matches the job:

• Use CargoLeanCapability in build.rs for crates that ship Lean source.
• Use LeanCapability to call a built capability in process.
• Use LeanWorkerCapabilityBuilder or LeanWorkerPool when the application needs process isolation, request timeouts, live rows, memory cycling, or crash containment. Their normal packaged-app input is the same manifest-backed capability descriptor that LeanCapability consumes.
• Use LeanLibrary::open, LeanLibrary::open_globally, raw link directives, and low-level worker APIs only for advanced interop, diagnostics, and tests.

Regression Gates

crates/lean-rs-worker/tests/loader_regressions.rs protects the public packaged-app path. It builds the shipped-crate template, then runs the same-process binary and worker example with LD_LIBRARY_PATH, LD_PRELOAD, DYLD_LIBRARY_PATH, DYLD_FALLBACK_LIBRARY_PATH, and DYLD_INSERT_LIBRARIES removed. The test proves the canonical path relies on build artifacts, rpath, and the bundle loader rather than a developer shell’s loader environment. The same file also checks the template package list and proves a public LeanCapability bundle keeps a transitive Lean dependency alive after the opener helper returns.

Worker bootstrap is checked through LeanWorkerCapabilityBuilder::check(). The report validates app-owned child resolution, executable status, manifest-backed capability preflight, protocol handshake, import session startup, and optional metadata expectations before a real command runs. The worker regression still keeps PATH because current host-session import startup uses Lean tooling; the bootstrap check now reports that deployment boundary explicitly instead of asking callers to manage child pipes or dynamic-loader variables.

This is not a narrow fix for one Linux or docs.rs failure. The failures point at a common design problem: volatile loader, package, and bootstrap decisions were visible in too many places. The hardening arc moves those decisions behind the crates that can own and test them, then makes the package simulation, loader regressions, worker bootstrap checks, and public-API baselines release gates.

Info-tree projection

LeanSession::process_with_info_tree projects a processed Lean source string into the ProcessedFile value type: four arrays of structurally distinct nodes (commands, terms, tactics, name references) plus the diagnostics the elaborator emitted. One Lean export, one Rust value, three downstream queries (goal_at_position, type_at_position, references_of_name) unblocked. Per POSD ch 6.1, the interface stays general-purpose (source, options, cancellation → ProcessedFile); the projection’s functionality serves the cursor-query trio but its interface doesn’t encode any of them.

What the projection carries

Every node carries an explicit (start_line, start_column, end_line, end_column) source range — 1-based at every layer, matching Lean’s Position convention. Bodies are owned strings and primitive integers only, so a ProcessedFile is Send + Sync + 'static and crosses worker-thread channels cleanly.

The diagnostics field reuses the host stack’s LeanElabFailure shape, so callers branch through the same diagnostics() / truncated() accessors as LeanSession::kernel_check.

What the projection does not carry

Raw Lean.Expr values, metavariable contexts, and Elab.InfoTree nodes themselves all stay behind the FFI boundary on purpose. They carry references the Rust side cannot revive outside the elaboration session that produced them — projecting to strings + ranges is what keeps the cross-thread guarantee. Callers that need notation-aware text for a specific expression use the optional lean_rs_host::meta::pp_expr service against the captured expression on the Lean side, not the projection.

The shim is also explicitly not incremental in v1. Every call re-runs Lean.Elab.IO.processCommands against the supplied source — the same path Lean’s LSP server uses for each didChange. Incremental reuse is a v0.3 optimisation when there is profile data to justify it. Per-command progress reporting is similarly deferred: every prompt-06 cursor query operates on one buffer per call, so adding a _progress sibling shim would double the symbol contract for a hypothetical use case.

Optional capability

lean_rs_host_process_with_info_tree is declared optional in the capability contract. A fork of the shim package that omits the symbol still loads cleanly; process_with_info_tree returns ProcessFileOutcome::Unsupported at dispatch time without invoking the FFI. The pattern matches the five MetaM services that already use this degradation path (LeanMetaResponse::Unsupported).

Position helpers

ProcessedFile exposes three inherent helpers so cursor consumers do not reinvent the range walk:

• term_at(line, column) -> Option<&TermInfoNode> — innermost containing term node.
• tactic_at(line, column) -> Option<&TacticInfoNode> — innermost containing tactic node.
• references_of(name) -> Vec<&NameRefNode> — every identifier occurrence whose fully-qualified name matches exactly.

“Innermost” is defined by source-range area: lines are weighted heavily so cross-line ranges always dominate single-line ranges. Ties on the same line break by column span. These helpers are pure Rust — no Lean call.

Host Stack Surface (lean-rs-host)

The curated public API of the L2 host stack—the published lean-rs-host crate. The classification table below is the semver surface: which items cross the crate root, which stay at module paths, which stay pub(crate). Refactors that reshape internal modules are free as long as the curated re-exports stay stable.

See 05-raw-sys-design.md for lean-rs-sys’s sibling rationale.

Layering

lean-rs-sys → lean-toolchain → lean-rs → lean-rs-host. The L1 FFI primitive lean-rs ships the typed @[export]-calling machinery and the structured error boundary; this L2 crate adds the opinionated capability/session/pool stack, and depends on the 28 + 6 lean_rs_host_* @[export] Lean shims bundled with lean-rs-host and loaded alongside consumer capability dylibs.

Downstream applications that just need to call a @[export] Lean function with typed arguments—the norm for Rust bindings to GC-hosted languages—depend on lean-rs directly and skip this crate.

Reusable interop machinery belongs below this crate; see 08-reusable-interop.md. The lean_rs_host_* shim contract remains the theorem-prover host policy layer, not the generic callback or build substrate.

Curated crate-root surface

#![allow(unused)]
fn main() {
// crates/lean-rs-host/src/lib.rs (illustrative)
pub use crate::host::{
    LeanHost, LeanCapabilities, LeanSession, LeanCancellationToken,
    LeanDeclarationFilter, LeanSourceRange,
    SessionPool, PooledSession, SessionStats, PoolStats,
};
pub use crate::host::elaboration::{
    LeanElabOptions, LeanElabFailure, LeanDiagnostic, LeanSeverity, LeanPosition,
    LEAN_HEARTBEAT_LIMIT_DEFAULT, LEAN_HEARTBEAT_LIMIT_MAX,
    LEAN_DIAGNOSTIC_BYTE_LIMIT_DEFAULT, LEAN_DIAGNOSTIC_BYTE_LIMIT_MAX,
};
pub use crate::host::evidence::{
    LeanEvidence, EvidenceStatus, LeanKernelOutcome, ProofSummary,
    LEAN_PROOF_SUMMARY_BYTE_LIMIT,
};
}

The handle types (LeanName, LeanLevel, LeanExpr, LeanDeclaration) and the error model live on lean_rs::*; callers needing both surfaces write use lean_rs::{LeanRuntime, LeanName} and use lean_rs_host::{LeanHost, LeanSession} side by side. The L1 crate root re-exports them; no module-path import needed.

Specialised sub-module surfaces

The crate root names mandatory session capabilities and entry points only. Sub-module paths host specialised or optional capabilities so the layer difference is visible at the import site (Ousterhout ch. 7—different layer, different abstraction).

• lean_rs_host::meta—the bounded MetaM capability. Five of the thirty-four SessionSymbols (meta_infer_type, meta_whnf, meta_heartbeat_burn, meta_is_def_eq, meta_pp_expr) are optional, and run_meta is the only call site that touches the meta types. Surfacing LeanMetaOptions, LeanMetaResponse, LeanMetaService, LeanMetaTransparency, MetaCallStatus, and the five factories at the crate root would pollute the namespace of every caller for the benefit of the subset that opts into MetaM. Meta callers write use lean_rs_host::meta::{...}; everyone else is undisturbed.
• lean_rs_host::process—the optional info-tree projection capability. One additional SessionSymbols slot (process_with_info_tree) and a value-typed ProcessedFile projection; only LeanSession::process_with_info_tree touches the module, so the four node types and the outcome enum live under process rather than at the crate root.

Mandatory entry points

Pooling and observability

Limits

Internal types

Methods on the curated types (happy-path shape)

Each requires doc comments and # Errors / # Panics sections.

• LeanHost::from_lake_project(runtime: &'lean LeanRuntime, path: impl AsRef<Path>) -> LeanResult<Self>
• LeanHost::load_capabilities(&self, package: &str, lib_name: &str) -> LeanResult<LeanCapabilities<'lean, '_>>—two-arg because Lake’s compiled dylib basename is lib{escaped_package}_{lib_name}.{dylib,so} with _ → __ escaping on the package; both pieces are required to resolve the on-disk artifact.
• LeanCapabilities::session(&self, imports: &[&str], cancellation: Option<&LeanCancellationToken>, progress: Option<&dyn LeanProgressSink>) -> LeanResult<LeanSession<'lean, '_>>
• LeanSession::query_declaration(&mut self, name: &str, cancellation: Option<&LeanCancellationToken>) -> LeanResult<LeanDeclaration<'lean>>
• LeanSession::elaborate(&mut self, source: &str, expected_type: Option<&LeanExpr<'lean>>, options: &LeanElabOptions, cancellation: Option<&LeanCancellationToken>) -> LeanResult<Result<LeanExpr<'lean>, LeanElabFailure>>
• LeanSession::kernel_check(&mut self, source: &str, options: &LeanElabOptions, cancellation: Option<&LeanCancellationToken>, progress: Option<&dyn LeanProgressSink>) -> LeanResult<LeanKernelOutcome<'lean>>
• LeanSession::check_evidence(&mut self, handle: &LeanEvidence<'lean>, cancellation: Option<&LeanCancellationToken>) -> LeanResult<EvidenceStatus>
• LeanSession::summarize_evidence(&mut self, handle: &LeanEvidence<'lean>, cancellation: Option<&LeanCancellationToken>) -> LeanResult<ProofSummary>
• LeanSession::run_meta<Req, Resp>(&mut self, service: &LeanMetaService<Req, Resp>, request: Req, options: &LeanMetaOptions, cancellation: Option<&LeanCancellationToken>) -> LeanResult<LeanMetaResponse<Resp>> where Req: LeanAbi<'lean> and Resp: TryFromLean<'lean>.
• LeanSession::query_declarations_bulk(&mut self, names: &[&str], cancellation: Option<&LeanCancellationToken>, progress: Option<&dyn LeanProgressSink>) -> LeanResult<Vec<LeanDeclaration<'lean>>>—strict semantics; first missing name errors the batch with Host(Conversion) naming it. With no token and no progress, the method keeps the N + 1 FFI-call shape (one bulk dispatch + N name_from_string) vs 2N for the singular fold. With a token, it loops through the singular path so it can check between names and discard partial output on cancellation. With progress and no token, it uses one Lean-side progress dispatch.
• LeanSession::declaration_source_range(&mut self, name: &str, cancellation: Option<&LeanCancellationToken>) -> LeanResult<Option<LeanSourceRange>>—returns Lean’s 1-based declaration range when recorded. The shim resolves module source paths from Lake source roots when possible and falls back to Lean’s module label when the source file cannot be found.
• LeanSession::list_declarations_filtered(&mut self, filter: &LeanDeclarationFilter, cancellation: Option<&LeanCancellationToken>, progress: Option<&dyn LeanProgressSink>) -> LeanResult<Vec<LeanName<'lean>>>—one Lean-side environment fold that excludes private, generated, and internal names according to the filter before Rust allocates returned handles.
• LeanSession::declaration_type_bulk(&mut self, names: &[&str], cancellation: Option<&LeanCancellationToken>, progress: Option<&dyn LeanProgressSink>) -> LeanResult<Vec<Option<LeanExpr<'lean>>>>—with no token, one bulk dispatch over Array String; with Some(token), loops through declaration_type so cancellation can be checked between names. Missing declarations are None in place.
• LeanSession::declaration_kind_bulk(&mut self, names: &[&str], cancellation: Option<&LeanCancellationToken>, progress: Option<&dyn LeanProgressSink>) -> LeanResult<Vec<String>>—with no token, one bulk dispatch over Array String; with Some(token), loops through declaration_kind. Missing declarations are "missing" in place.
• LeanSession::declaration_name_bulk(&mut self, names: &[&str], cancellation: Option<&LeanCancellationToken>, progress: Option<&dyn LeanProgressSink>) -> LeanResult<Vec<String>>—with no token, one bulk dispatch over Array String; with Some(token), loops through declaration_name. Missing declarations render as their input name.
• LeanSession::elaborate_bulk(&mut self, sources: &[&str], options: &LeanElabOptions, cancellation: Option<&LeanCancellationToken>, progress: Option<&dyn LeanProgressSink>) -> LeanResult<Vec<Result<LeanExpr<'lean>, LeanElabFailure>>>—per-source Result mirrors elaborate exactly. No expected_type parameter; a concrete second caller would justify the per-source &[Option<&LeanExpr>] surface. With no token, this is one Lean-side bulk dispatch; with Some(token), this loops per source to create cancellation check points.
• LeanSession::call_capability<Args, R>(&mut self, name: &str, args: Args, cancellation: Option<&LeanCancellationToken>) -> LeanResult<R::Output> where Args: LeanArgs<'lean> and R: DecodeCallResult<'lean>. Function-only escape hatch for capability-dylib exports beyond the twenty-seven session-fixed symbols; reuses the same Args / R bounds as lean_rs::LeanModule::exported, including the LeanIo<T> IO marker. Adds session-level tracing (lean_rs.host.session.call_capability span with symbol + arity fields) and a SessionStats counter bump—those L2 concerns are why it lives here rather than as a pass-through on LeanModule. Callers that don’t want the instrumentation use module.exported::<Args, R>(name)?.call(args) directly on the L1 handle.
• LeanSession::stats(&self) -> SessionStats—snapshot of per-session dispatch metrics.
• SessionPool::with_capacity(runtime: &'lean LeanRuntime, capacity: usize) -> Self
• SessionPool::acquire<'p, 'c>(&'p self, caps: &'c LeanCapabilities<'lean, 'c>, imports: &[&str], cancellation: Option<&LeanCancellationToken>, progress: Option<&dyn LeanProgressSink>) -> LeanResult<PooledSession<'lean, 'p, 'c>>—capability-agnostic storage; entries are bare Obj<'lean> environments rewrapped under the supplied capability borrow at acquire time. FIFO on take, LIFO on push.
• SessionPool::drain(&self) -> usize—drops every cached free-list environment and returns the number removed. Checked-out PooledSessions remain valid and may return to the pool later. This releases Rust-owned environment refs only; it does not reset Lean’s process-global import/runtime state.
• SessionPool::stats(&self) -> PoolStats, len(), is_empty(), capacity()—observability. PoolStats tracks imports, reuse, release-at-capacity drops, explicit drain calls, and entries removed by drains.

None leak raw lean_* types, raw refcount obligations, or initializer-symbol order.

Lifetime cascade

#![allow(unused)]
fn main() {
LeanRuntime                 ::init() -> LeanResult<&'static LeanRuntime>
LeanHost<'lean>             ::from_lake_project(&'lean LeanRuntime, path) -> ...
LeanCapabilities<'lean, 'h> ::load_capabilities(&'h LeanHost<'lean>, package, lib_name)
LeanSession<'lean, 'c>      ::session(&'c LeanCapabilities<'lean, '_>, imports, cancellation, progress)
LeanExpr<'lean>             // (and the other L1 handles)
}

'lean is invisible at typical call sites (inferred from the runtime borrow). Compile-time enforcement: no handle outlives the runtime borrow; no L2 type escapes to another thread (all types are !Send + !Sync by default—see the trybuild assertion at crates/lean-rs-host/tests/compile_fail/runtime_is_not_send_or_sync.rs).

Error model

LeanError lives on lean-rs (L1). It is the only public error type that crosses either crate’s boundary. Two variants: LeanException(LeanException) for Lean-thrown IO errors that callers may surface to end users, and Host(HostFailure) for any host-stack failure (init, link, load, conversion, contained callback panic, internal invariant). Payload structs have private fields and pub(crate) constructors that run the bounding helper, so the LEAN_ERROR_MESSAGE_LIMIT (4 KiB) cap on message() is a structural invariant—external callers receive LeanError values but cannot mint one with an unbounded message. lean-rs-host constructs Host(...) variants via the lean_rs::__host_internals seam.

Except<E, T> is a value type, not an error. When an exported function returns IO (Except E T):

1. Outer IO failure → LeanError::LeanException (host failure).
2. Inner Except decodes via TryFromLean into Rust Result<T, E> (application semantics).

The caller sees LeanResult<Result<T, E>> and decides how to flatten. Rule: runtime / host failures are LeanError; application semantics are values.

Consumed L1 surface

lean-rs-host reaches into lean_rs::* as a normal downstream consumer. None of these belong to this crate’s semver surface—they are listed so the L1 → L2 dependency is visible.

• LeanRuntime—process-once init; lifetime anchor for every L2 type.
• LeanThreadGuard—RAII attach for worker threads not started inside Lean.
• LeanLibrary—RAII handle over the capability dylib LeanCapabilities opens.
• LeanModule—initialized module handle the session reaches typed exports through.
• LeanExported—cached typed function handle the session calls via call_capability.
• LeanArgs, LeanIo, DecodeCallResult, LeanAbi—bounds and markers for typed dispatch generics.
• LeanName, LeanLevel, LeanExpr, LeanDeclaration—opaque handles re-used as L2 method return shapes.
• lean_rs::error::*—LeanError, LeanResult, LeanException, LeanCancelled, HostFailure, HostStage, LeanExceptionKind, LeanDiagnosticCode, LEAN_ERROR_MESSAGE_LIMIT, DiagnosticCapture, CapturedEvent, DIAGNOSTIC_CAPTURE_DEFAULT_CAPACITY. The shared error model.

Two #[doc(hidden)] pub seams substitute for Cargo’s missing “friend crate” visibility:

• lean_rs::__host_internals::{host_module_init,host_cancelled}—the narrow constructor wrappers this crate calls from host/lake.rs and host/cancellation.rs. They preserve the bounding invariant (external callers receive LeanError values but cannot mint one with an unbounded message) without forcing this crate to re-implement error construction. Re-add wrappers the same way (single-call #[doc(hidden)] pub fn + re-export) if a future call site needs one.
• lean_rs::error::bound_message—UTF-8-boundary truncation helper used at six sites in host/{elaboration,meta}/options.rs and host/elaboration/diagnostic.rs to bound Lean-authored strings before they flow into Host(...) payloads. Lives on the L1 surface (not at __host_internals) because it is a string utility, not a constructor wrapper.

The supertrait lean_rs::abi::traits::sealed::SealedAbi is similarly pub so this crate can implement LeanAbi for its own host-defined types (LeanEvidence, etc.); external crates are blocked by the orphan rule plus the #[doc(hidden)] marker on the parent module.

Rejected approaches

• Re-export every pub item from every internal module at the crate root. Path-shortening dressed up as curation; gives mandatory and specialised items equal status. Violates Ousterhout ch. 17 (consistency requires dissimilar things to be done differently).
• One LeanHost god-type with every operation as a method. The canonical “complect” case (Ousterhout ch. 4 + Hickey): runtime, modules, sessions, semantic handles, and error policy braided into one mechanism. Kills the 'lean cascade—LeanExpr<'lean> cannot outlive its session, but a god type would have to be 'static to host every method—and forces caller code to thread one large &mut through every layer.
• Hide lean-rs-host’s internal modules behind a top-level façade. Over-encapsulates for hypothetical safety wins. Advanced users already have a clean escape hatch via lean-rs-sys, but that drops them to raw FFI. Keeping lean-rs::module visible at module paths preserves the middle tier: typed handles, no raw lean_* symbols.
• Keep LeanHost / LeanCapabilities / LeanSession in lean-rs itself. Conflated two layers behind one default entry point and made it impossible for an external L1-only consumer to depend on lean-rs = "0.1" without satisfying the 28 + 6 lean_rs_host_* shim contract.

Naming convention

• Crate-root re-exports use the Lean prefix. Disambiguates use lean_rs_host::* in mixed-language projects.
• Module-path types drop the prefix when the module path disambiguates. lean_rs_host::host::session::SessionStats, lean_rs_host::host::pool::PoolStats. If a power-user item is later elevated to the crate root, re-export with the Lean prefix where that improves disambiguation (e.g., pub use ... as LeanSessionStats).
• Internal pub(crate) types use short names. They never appear in docs.

Verification

The classification is satisfied when:

1. rg -n "^pub use" crates/lean-rs-host/src/lib.rs matches the curated set above.
2. crates/lean-rs-host/tests/curated_surface.rs uses only use lean_rs::{...} and use lean_rs_host::{...} crate-root items (no module-path access).
3. crates/lean-rs-host/tests/compile_fail/runtime_is_not_send_or_sync.rs confirms every L2 type is neither Send nor Sync.
4. RUSTDOCFLAGS="-D warnings" cargo doc --no-deps --workspace is clean and every curated item has a doc comment.
5. docs/api-review/lean-rs-host-public.txt matches the curated surface 1:1.

lean-rs-host Capability Contract

The 28 mandatory + 6 optional @[export] lean_rs_host_* symbols lean-rs-host’s LeanCapabilities::load_capabilities resolves at runtime. The lean-rs-host crate ships the implementation under crates/lean-rs-host/shims/lean-rs-host-shims/ and a bundled generic interop dependency under crates/lean-rs-host/shims/lean-rs-interop-shims/. External consumers do not add a lean_rs_host_shims require line to their own lakefile.lean; the Rust loader builds and opens the crate-owned shim dylibs. Expected host-shim dylib name: liblean__rs__host__shims_LeanRsHostShims.{dylib,so}.

This document covers the wire-level contract: each Lean signature, the typed Rust shape LeanSession::* exposes on top, and the Rust call-site mapping. The architectural rationale (generic interop dylib, host shim dylib, RTLD_GLOBAL, the consumer lakefile.lean shape) lives in architecture/03-host-stack.md.

Resolution

LeanCapabilities::new performs:

1. LakeProject::interop_dylib() builds the bundled generic interop shim target if needed, opens the generic interop dylib globally, and initializes LeanRsInterop.
2. LakeProject::shim_dylib() builds the bundled host shim target if needed.
3. LeanLibrary::open_globally(runtime, shim_dylib_path) opens the host shim dylib with RTLD_LAZY | RTLD_GLOBAL on Unix.
4. shim_library.initialize_module("lean_rs_host_shims", "LeanRsHostShims") runs the shim’s root initializer, which transitively initializes Lean.* and the already-loaded generic callback module.
5. user_library.initialize_module(<package>, <lib_name>) runs the consumer’s root initializer. The consumer does not require or initialize host shims.
6. SessionSymbols::resolve(&shim_library) populates every lean_rs_host_* address from the shim dylib. The consumer dylib’s LeanSession::call_capability route stays open for user-authored @[export] symbols.

LeanSession::import passes three .olean roots to the import shim: the consumer project, lean_rs_interop_shims, and lean_rs_host_shims.

A missing mandatory symbol fails capability load with LeanError::Host(stage = Link). A missing optional meta-service symbol stores None in SessionSymbols; LeanSession::run_meta returns LeanMetaResponse::Unsupported for that service at dispatch time.

Mandatory contract (28 symbols)

Lean structure types (ElabOpts, ElabResult, Evidence, EvidenceStatus, KernelOutcome, ProofSummary, MetaOpts, MetaResponse, DeclarationFilter, SourceRange) live in crates/lean-rs-host/shims/lean-rs-host-shims/LeanRsHostShims/Elaboration.lean and Meta.lean. Rust counterparts and the TryFromLean / IntoLean impls crossing the ABI live in crates/lean-rs-host/src/host/{elaboration,evidence,meta}/. DeclarationFilter is a private wire record whose three flags are Nat-backed 0/1 values so it uses the same object-slot structure ABI as the rest of the host-defined records; Rust callers see ordinary bool fields.

Environment and declaration queries (15)

Elaboration, kernel check, evidence (5)

Optional contract (6 symbols)

If absent at load time, SessionSymbols::resolve_optional_function_symbol stores None for that slot; the dispatching call site degrades gracefully — LeanSession::run_meta synthesises LeanMetaResponse::Unsupported for the meta services, and LeanSession::process_with_info_tree returns ProcessFileOutcome::Unsupported for the info-tree projection.

Forking the shim package

The shim package is small (~700 LOC across four files). A fork that customises behaviour (e.g., different heartbeat policy, extra logging on the kernel-check path) must keep:

• Same Lake package name (lean_rs_host_shims) and lean_lib name (LeanRsHostShims) so LeanCapabilities can initialize the module and interpret symbol names consistently.
• Same 28 mandatory @[export] symbol names with compatible signatures (the Rust side casts function pointers to fixed shapes).
• The 6 optional symbols are truly optional; omitting any collapses the corresponding session method to its Unsupported arm (run_meta for the five meta services, process_with_info_tree for the info-tree projection).

A fork that changes the Lean structure layouts also needs corresponding Rust changes—this is why the shim package isn’t framed as “compatibility shims” but as the implementation of the wire contract.

Forks should keep reusable callback/string/name/object ABI helpers in the generic lean-rs-interop-shims package when those helpers are not host-policy-specific.

Production Boundary

lean-rs-host is the fast in-process theorem-prover API. It is the right surface for trusted workloads where the caller accepts Lean’s process-scoped failure and memory contracts. It is not the containment boundary for production systems that must survive Lean internal panics, aborts, foreign unwinds, or long-running import sweeps that retain process-global memory.

The production boundary is a worker process. lean-rs-worker owns child processes, framed IPC, restart policy, fatal-exit diagnostics, request timeouts, live row streaming, typed command facades, and memory cycling. lean-rs-host remains the in-process API that the worker uses inside the child.

Chosen Boundary

The crate split is:

• lean-rs owns typed Lean object handles, exported calls, and sealed callback payloads.
• lean-rs-host owns in-process sessions, imports, elaboration, kernel checks, declaration introspection, MetaM, pooling, cancellation, and progress.
• lean-rs-worker owns process supervision, worker protocol framing, restart policy, lifecycle, request watchdogs, row streaming, typed commands, memory cycling, and fatal-exit reporting.

This boundary keeps each layer at a different abstraction. lean-rs-host answers theorem-prover questions in one process. lean-rs-worker answers an operational question: how to run that host stack when the caller needs process isolation or a hard memory reset.

Why Process Isolation Is Required

Lean internal failures do not all return through an error channel. A kernel assertion, generated unreachable, LEAN_ABORT_ON_PANIC path, std::exit, abort, or foreign unwind may terminate the process or cross a C ABI boundary that Rust cannot recover from soundly. LeanSession therefore cannot promise a poisoned-but-droppable session after those failures. The safe containment unit is the child process: the parent observes worker exit and decides whether to restart.

The worker boundary does not change the in-process panic contract. Inside the child, the same rules from 06-panic-containment.md apply. The difference is that the parent process survives and receives a typed worker-failure report instead of losing the application process.

Why Memory Cycling Is Required

Long-running processes can retain Lean runtime memory even after Rust-owned session and pool values are dropped. Reused imported environments are stable, but workloads that sweep fresh import sets can leave process-global residue in module initialization state, imported environment data, compacted regions, interned names, allocator state, and other Lean runtime structures.

SessionPool::drain() releases cached Rust-owned environment references. It is useful at idle boundaries, but it is not an RSS reset. Only exiting the worker process resets Lean’s process-global state. lean-rs-worker therefore provides process-cycling triggers for explicit cycles, request count, import-like request count, idle restart, measured RSS ceiling, and in-flight worker-session cancellation. The measurement baseline remains ../safety/long-session-memory.md.

Host Operations Across The Boundary

The worker session adapter is a narrow, process-safe subset of LeanSession. It returns copied diagnostics, kernel statuses, and rendered declaration strings; it does not send runtime-bound LeanExpr, LeanEvidence, LeanDeclaration, or LeanName handles to the parent. See 17-worker-session-adapter.md.

Rejected Boundaries

Embedding worker support in lean-rs-host. Rejected. Process supervision, framed IPC, restart bookkeeping, crash diagnostics, and memory cycling are not theorem-prover session operations. Putting them on LeanSession or LeanCapabilities would make the in-process host layer shallow: every caller would see operational machinery even when they only need fast trusted calls.

Downstream-only orchestration. Rejected. Leaving process supervision to each consumer would make every production embedder rediscover the same rules for panic containment, child cleanup, request framing, crash classification, restart cadence, and memory cycling. Those rules are part of the binding stack’s operational contract and should be encoded once.

Callback Payloads Stay Below The Worker

Callback payloads remain an L1 lean-rs concern. LeanCallbackPayload is sealed, and supported payloads are added only after the ABI, ownership, wrong-payload, stale-handle, reentrancy, and panic-boundary rules are proven. The worker should use those payloads; it should not create an arbitrary cross-process callback type system.

Byte streaming and Lean-object events are future callback payload work, not worker-protocol shortcuts. The worker may carry serialized effects over IPC, but the same deep-module rule applies: payload decoding and Lean object soundness belong below the process supervisor.

Consumer Guidance

Compose at the highest layer that matches the operational requirement. Direct lean-rs callbacks are for trusted same-process ABI work. lean-rs-host is for trusted in-process theorem-prover sessions. lean-rs-worker is for worker-style tools where process lifecycle, IPC, fatal exits, request timeouts, row streaming, and memory reset should be owned by the library rather than every downstream caller.

Use lean-rs-host directly when the process can trust the Lean workload, when latency is the primary concern, and when process-level memory retention is acceptable.

Use the lean-rs-worker boundary when the application must continue after Lean exits, must classify fatal child exits, or must reset memory after large import sweeps. The worker is not a replacement for lean-rs-host; it is a process boundary around it. See ../recipes/worker-process-boundary.md for the runnable worker-streaming example.

Worker Session Adapter

lean-rs-worker exposes a narrow host-session adapter over the process boundary. It is not a remote LeanSession. The in-process session remains the richer API for trusted callers; the worker adapter serves production callers that need crash isolation, memory cycling, and typed IPC.

Public Shape

Callers open a session with LeanWorker::open_session and a LeanWorkerSessionConfig naming the Lake project, package, library, and import list. The returned LeanWorkerSession borrows the supervisor and exposes the supported cross-process subset:

• elaborate returns LeanWorkerElabResult;
• kernel_check returns LeanWorkerKernelResult;
• declaration_kinds returns Vec<String>;
• declaration_names returns Vec<String>.

These outputs are deliberately serializable. The worker does not send LeanExpr, LeanEvidence, LeanDeclaration, or LeanName handles to the parent because those handles are tied to the child Lean runtime. Diagnostics are copied into LeanWorkerDiagnostic values with severity, message, file label, and optional source positions.

Hidden Boundary

The private protocol carries frames for opening a host session and for the supported operations. That protocol is versioned and tested, but it is not the caller-facing API. Callers do not manage Command, pipe reads, frame encoding, child stderr parsing, or restart bookkeeping.

Inside the child, the adapter calls lean-rs-host. This keeps theorem-prover policy in lean-rs-host and process policy in lean-rs-worker.

Progress And Cancellation

Worker progress is a parent-side IPC event, not a cross-process callback handle. LeanWorkerProgressSink receives LeanWorkerProgressEvent values with a string phase, current count, optional total, and elapsed duration measured in the parent.

LeanWorkerCancellationToken is also parent-side. The supervisor checks it before sending a request and after progress frames while a request is in flight. If cancellation is observed during a request, the supervisor cycles the child process, returns LeanWorkerError::Cancelled, and invalidates the open LeanWorkerSession. Open a new session before issuing more host requests.

This is a worker-safe boundary. It does not share an in-process LeanCancellationToken or LeanCallbackHandle with the child.

Current Limits

The adapter intentionally does not mirror every LeanSession method. It does not support arbitrary capability protocols, cross-process callback handles, MetaM services, evidence handles, source-range handles, or expression transport. Add operations only when a production worker use case needs a process-safe value shape.

Worker Data Streaming

lean-rs-worker needs a row stream for downstream protocols that produce arbitrary user data while a worker request is running. The host-session adapter can already return copied theorem-prover values and progress events, but that is not enough for tools that need a sequence of downstream-owned rows such as JSONL-like lean-dup output.

Worker data rows are worker IPC data. They are not L1 callback payloads and not Lean runtime handles. The worker owns process framing, ordering, cancellation boundaries, fatal-exit behavior, and sink panic containment. Downstream crates own the row schema.

Public Row Shape

The selected public row type is:

#![allow(unused)]
fn main() {
pub struct LeanWorkerDataRow {
    pub stream: String,
    pub sequence: u64,
    pub payload: serde_json::Value,
}
}

stream is a caller-defined channel name, such as "rows", "warnings", or a tool-specific stream label. sequence is assigned by lean-rs-worker per stream within one request. payload is arbitrary JSON owned by the downstream protocol.

This type is intentionally generic at the worker boundary and intentionally not schema-free inside downstream tools. lean-rs-worker carries rows. It does not define lean-dup row structs, theorem-search result schemas, or application business objects.

Chosen Boundary

lean-rs-worker owns:

• length-delimited, versioned row frames in the private worker protocol;
• per-stream row ordering;
• conversion from child-side streaming callbacks to parent-side row events;
• live forwarding with pipe backpressure at row boundaries;
• terminal stream summaries for commit-after-success workflows;
• diagnostics as a separate worker channel, not row payloads;
• row-boundary cancellation behavior;
• EOF and fatal-child-exit behavior while a stream is active;
• containment of parent-side data-sink panics.

Downstream crates own:

• stream names and their meanings;
• JSON object shape;
• validation beyond “is valid JSON”;
• semantic interpretation of each row;
• persistence, indexing, deduplication, and UI policy.

The boundary follows the same rule as the worker-process boundary: the worker hides process and IPC mechanics, but it does not absorb downstream domain schemas.

Rejected Designs

Raw stdout JSONL. Rejected. It exposes process I/O, framing, completion, EOF, cancellation, and fatal-exit rules to every consumer. It also competes with structured worker diagnostics and progress for the same untyped channel. That would make each downstream tool reimplement the worker protocol outside the worker.

Public cross-process callbacks. Rejected. LeanCallbackHandle is an in-process L1 mechanism. Its handle lifetime, trampoline values, refcount rules, panic containment, and wrong-payload checks are valid only inside one process. Passing those handles across the worker boundary would turn an in-process FFI tool into an IPC API and leak exactly the mechanics the worker exists to hide.

Worker data rows. Chosen. A worker row stream is the smallest public shape that supports arbitrary downstream JSON rows while preserving the worker’s deep module boundary. Callers learn a row sink and a row type; they do not learn frame bytes, pipe reads, child exits, callback handles, or terminal-response frames.

Relationship To L1 Callback Payloads

The child may use in-process L1 callbacks to collect strings from a Lean export, but those callbacks remain child-local. For the first streaming runner, the child registers a LeanCallbackHandle<LeanStringEvent>, parses each callback string as a row, diagnostic, or terminal-metadata envelope, and sends private worker frames to the parent. The parent sees LeanWorkerDataRow, LeanWorkerDiagnosticSink events, and a terminal summary; callback handles stay inside the child.

Byte streaming and Lean-object callbacks stay in the L1 callback-payload track. They require their own ABI and soundness work because they change how Lean data enters Rust in one process. Worker row streaming does not shortcut that work: it serializes process-safe JSON values over IPC.

The reverse is also true: worker row streaming does not need wider callback payloads. Worker-class data already travels to the parent as JSON or validated raw JSON frames. Add byte or object callback payloads only for real same-process L1 interop needs, not to improve worker ergonomics.

Consumer Guidance

Use direct L1 string callbacks when the Lean extension is trusted, in-process, and the application does not need crash isolation or memory reset.

Use worker data rows when the application needs the worker process boundary. The row payload can be any JSON value, but lean-rs-worker treats it as data. Schema ownership remains with the downstream crate.

For throughput, private DataRow frames carry validated raw JSON payloads. The public schema-less LeanWorkerDataRow still exposes serde_json::Value; that conversion happens only for callers that choose the low-level raw-row API. The typed command facade decodes the raw payload directly into the downstream row type, avoiding an intermediate JSON tree.

The normal worked recipe is ../recipes/worker-capability-runner.md. The lower-level process-boundary and raw-row escape hatch is documented in ../recipes/worker-process-boundary.md.

Request timeout is the watchdog for streams that stop producing terminal success. It is enforced by the parent supervisor, not by the Lean callback. If the deadline expires after some rows have been delivered, those rows are still tentative: callers that need atomic commit must discard them unless run_data_stream returns Ok(LeanWorkerStreamSummary).

Worker Capability Layer

A subprocess worker does more than move rows. It defines when rows become committable, how diagnostics are separated from data, how request timeouts are handled, how callers discover capability versions, how the worker is built and started, and how performance is measured. Those concerns belong above raw row transport and below downstream business schemas; this is the crate’s home for them.

Chosen Boundary

lean-rs-worker exposes a generic worker capability layer. That layer owns:

• process lifecycle and restart behavior;
• private worker framing and live bounded row forwarding;
• row ordering, row-boundary cancellation, and sink failure handling;
• terminal completion metadata and commit-after-success semantics;
• diagnostics as a channel distinct from data rows;
• per-request timeout and watchdog behavior;
• capability metadata and doctor checks;
• build/session setup ergonomics for downstream capabilities;
• typed command facades over downstream-owned serde request, row, and summary types;
• performance evidence for large streams.

Downstream crates own:

• command names and their semantic meaning;
• request, row, and terminal summary schemas;
• validation beyond the generic worker envelope;
• cache policy, persistence, indexing, and user-facing workflows.

This keeps the worker layer somewhat general-purpose. It hides process and IPC mechanics that every production consumer would otherwise reimplement, but it does not encode lean-dup declarations, features, probes, or cache validity as first-party lean-rs-worker concepts.

Rejected Designs

Raw run_data_stream. Rejected as the final downstream interface. It is a useful primitive, but it asks every caller to know export names, request JSON encoding, row sink wiring, session setup, completion policy, and failure classification. That is too much worker machinery at the call site.

lean-dup-specific worker APIs. Rejected for lean-rs-worker. Methods such as extract, features, index, or probe would make the worker crate a lean-dup adapter. Those commands are valid downstream examples, not generic worker responsibilities.

Generic worker capability layer. Chosen. The worker owns lifecycle, framing, live streaming, timeout, cancellation, diagnostics, metadata, completion, and restart behavior. Downstream crates own schemas and semantic commands.

Capability Surface

The capability layer fills the gap between row transport and a production worker replacement:

1. Live bounded forwarding. Rows reach the parent while Lean produces them. The worker owns bounded buffering, pipe backpressure at row boundaries, cancellation checks, and sink-failure handling.
2. Terminal completion and diagnostics. Streams return per-stream row counts, elapsed time, optional downstream terminal JSON, and clear commit-after-success semantics. Diagnostics have a separate sink and are not smuggled through row payloads.
3. Timeouts and watchdogs. Startup timeout, request timeout, cancellation, child crash, and policy restart are distinct outcomes with distinct typed errors or restart reasons.
4. Capability metadata and doctor checks. Downstream tools can report protocol versions, capability versions, supported commands, supported features, Lean version, and health diagnostics without hard-coding one tool’s command set into lean-rs-worker.
5. Builder ergonomics. LeanWorkerCapabilityBuilder composes Lake target build, shim resolution, worker child path, capability dylib path, imports, restart policy, metadata validation, and session opening without handwritten path mangling.
6. Typed command facade. Downstream callers use serde request, row, and summary types while lean-rs-worker owns transport, lifecycle, diagnostics, timeout, cancellation, and completion.
7. High-throughput row payload path. Large streams use a private raw-JSON representation so typed commands can deserialize directly into downstream row types without first building a serde_json::Value tree.

Relationship To Callback Payloads

Worker capability streaming is IPC work. It does not replace the L1 callback payload track in lean-rs.

Inside the child, a streaming runner may use LeanCallbackHandle<LeanStringEvent> to receive row JSON from Lean. Across the worker boundary, the parent receives worker rows and diagnostics. Callback handles, raw Lean object lifetimes, and trampoline values remain in-process mechanisms.

Future byte or object callback work remains L1 lean-rs payload work. It is not a shortcut for worker capability streaming, and worker capability streaming is not a reason to expose arbitrary downstream LeanCallbackPayload implementations. Byte callbacks need a concrete same-process binary callback caller before they earn public surface. Object callbacks are not exposed until a soundness proof produces a scoped API.

Consumer Guidance

Use typed worker commands for production-style downstream tools that need live row delivery, request completion metadata, diagnostics, timeouts, capability discovery, restart policy, and measured performance. Use run_data_stream directly only for low-level experiments, fixtures, and schema-less tooling. The source-of-truth recipe for this path is docs/recipes/worker-capability-runner.md.

run_data_stream forwards rows live, keeps diagnostics on a separate sink, and returns terminal summaries with total rows, per-stream counts, elapsed time, and optional downstream metadata. Treat it as a low-level escape hatch once the builder and typed command facade hide export names, request JSON encoding, and setup sequencing.

Startup and request deadlines are separate. LeanWorkerConfig::startup_timeout covers only child handshake. LeanWorkerConfig::request_timeout, LeanWorker::set_request_timeout, and LeanWorkerSession::set_request_timeout configure the parent-enforced deadline for one request. A timeout kills and replaces the child, records LeanWorkerRestartReason::RequestTimeout, returns LeanWorkerError::Timeout, and invalidates the open session. Partial rows delivered before the timeout remain tentative because no terminal success summary was returned.

Runtime metadata and capability metadata are separate. LeanWorker::runtime_metadata reports worker protocol facts captured during handshake. LeanWorkerSession::capability_metadata and LeanWorkerSession::capability_doctor call downstream Lean exports with ABI String -> IO String and decode returned JSON into generic command, capability, version, and diagnostic envelopes. The worker transports and validates those envelopes; downstream crates decide which command names, capability names, semantic versions, and doctor diagnostics affect caches or user-facing support workflows.

LeanWorkerCapabilityBuilder is the normal setup path for downstream capabilities. It builds the named Lake lean_lib target through lean-toolchain, resolves and starts the worker child, health-checks the worker, opens the configured import session, applies the selected restart/timeout policy, and optionally validates capability metadata. The caller still names the Lake project root, package, target, and imports; those are capability identity, not worker internals. The default child resolver checks LEAN_RS_WORKER_CHILD, sibling Cargo profile paths, and the workspace development build. Low-level LeanWorker remains available for tests, custom supervision, and focused lifecycle examples.

Use downstream crates for domain schemas. A lean-dup integration maps its own request and row types onto the generic worker capability layer; it does not require lean-rs-worker to know what a declaration row, feature row, index update, or probe result means.

LeanWorkerJsonCommand<Req, Resp> and LeanWorkerStreamingCommand<Req, Row, Summary> are the preferred downstream interfaces over capability exports. They name an export while keeping request, row, and terminal-summary schemas in downstream serde types. The worker still owns process lifecycle, private framing, live row forwarding, diagnostics, timeouts, cancellation, and terminal completion. Typed row decode failures carry the command export, stream, and sequence; raw LeanWorkerDataRow access remains available through run_data_stream for callers that want schema-less rows.

The private worker protocol uses an adjacent tag shape so DataRow can carry a serde_json::value::RawValue payload. Typed streaming commands deserialize that validated raw JSON directly into downstream row types. The public LeanWorkerDataRow { payload: serde_json::Value } surface remains for schema-less tooling but is not on the typed command hot path.

Private row batching is not implemented. The microbenchmark and the broader 512-row worker stream did not justify adding DataRowBatch frames or a public batch sink; row delivery stays live and per-row until a workload proves batching improves the full worker path, not just a synthetic frame loop.

lean-rs-worker ships a downstream-shaped fixture that combines the pieces above without adding business methods. It exports command-like names version, doctor, extract, features, index, and probe only to stress the generic capability layer: metadata discovery, doctor diagnostics, typed JSON commands, typed streaming commands, terminal summaries, cancellation, request timeouts, fatal child exits, explicit cycling, and RSS/throughput measurement. The row schemas are deliberately small. They do not define declaration rows, feature rows, probe results, cache policy, ranking, or any other downstream semantic contract.

Lean capability authors can use 24-lean-side-worker-streaming.md’s LeanRsInterop.Worker.Stream helpers to build worker row, diagnostic, progress, and terminal-metadata envelopes. Those helpers live below the worker capability facade: they reduce Lean-side envelope boilerplate, but they do not define command semantics, row schemas, pool scheduling, or session keys.

The scenario benchmark and worker_capability_probe example are the performance envelope for this shape. They measure cold startup, first import, import-once streaming, row throughput, cancellation latency, fatal-exit recovery, worker cycling, and memory growth. A comparison against an existing subprocess worker is optional and must name the exact downstream command and revision; it is not part of the lean-rs-worker API.

Worker Pool

A single worker is the right unit for panic containment and process-global memory reset, but it is not enough for mathlib-scale or multi-package workloads. Those workloads need parallelism, warm session reuse, memory admission, and failure isolation across more than one child process.

The pool boundary keeps that operational machinery inside lean-rs-worker. Downstream callers submit capability work keyed by session requirements. The pool decides whether to reuse a warm worker, start a new child, cycle a stale child, or delay work until policy permits it.

Chosen Boundary

LeanWorkerPool is the local multi-worker orchestration boundary. It owns:

• worker child lifecycle;
• work queueing and admission;
• session leases and session-key matching;
• worker restart and session invalidation sequencing;
• memory-aware scheduling and RSS sampling policy;
• failure isolation between child processes;
• cancellation and timeout propagation into leased work;
• pool-level observability.

The pool does not replace LeanWorkerCapabilityBuilder or typed commands. It sits above them: the builder describes how to open one capability-backed worker session, while the pool decides which local child should host that session for one piece of work.

The public surface is a lease-first API:

• LeanWorkerPool owns a bounded set of local capability workers;
• LeanWorkerPoolConfig exposes a fixed max_workers limit;
• LeanWorkerSessionKey records the worker reuse facts;
• LeanWorkerSessionLease runs typed JSON and streaming commands without exposing LeanWorkerSession as the primary pool API.

A lease becomes invalid after timeout, cancellation, child fatal exit, explicit cycle, or capability metadata mismatch. The caller acquires a fresh lease for follow-up work. That rule keeps session invalidation explicit without making callers learn which child process or warm worker was selected.

The same pool boundary carries local memory-aware scheduling:

• max_total_child_rss_kib rejects a new distinct worker when known total child RSS already reaches the configured budget;
• per_worker_rss_ceiling_kib cycles a warm worker before assigning more work when its sampled RSS reaches the configured ceiling;
• idle_cycle_after cycles an idle worker before stale leased work continues;
• queue_wait_timeout bounds synchronous admission waits for a full pool.

RSS sampling is best effort and platform-specific. Unsupported samples are recorded as unavailable; the pool does not claim a budget decision from missing RSS data. Memory-driven cycles are reported as policy restarts and invalidate stale leases before downstream command execution.

Pool-level observability and bounded row-delivery backpressure also live at this boundary:

• LeanWorkerPoolSnapshot summarizes worker counts, warm leases, queue depth, restart reasons, child RSS samples, stream request outcomes, delivered row counts, payload bytes, stream elapsed time, and backpressure counters;
• LeanWorkerSessionLease::snapshot samples the leased worker without exposing child identity;
• row delivery uses a bounded internal event buffer, so a slow sink blocks the request path instead of growing memory without bound;
• rows are never dropped for committed streams, and delivered rows remain tentative until terminal success.

Snapshots are operational summaries, not protocol traces. They do not expose worker ids, child pids, pipe handles, protocol frames, or which warm worker was selected.

Designs Considered

Single worker only. Rejected as the scale foundation. It preserves a clean process boundary, but it serializes independent module groups. A downstream tool that wants to use available cores would have to build its own worker fanout, queueing, and restart policy.

Caller-managed worker fanout. Rejected. It would push child counts, restart timing, session reuse, memory ceilings, lease invalidation, and failure classification into every downstream tool. That duplicates the same production rules that lean-rs-worker already owns for one worker.

LeanWorkerPool. Chosen. The pool is a deeper module because it hides orchestration decisions that every local production consumer would otherwise reimplement. The public surface should describe capability work and policy intent, not child process mechanics.

Remote workers are out of the current arc. The local pool should not expose APIs that assume a worker is identified by a child pid or a local pipe, because that would make a future remote backend harder. The first supported backend is local child processes.

Session Keys

Pool reuse is keyed by the facts that make a worker session safe and useful to reuse:

• Lake project root;
• capability package and target;
• import set;
• capability metadata expectations;
• Lean toolchain and lean-rs protocol fingerprint;
• restart-policy class.

The key is not a downstream cache key. Downstream crates still decide whether a row, index, probe, or report is semantically valid. The pool key only answers a worker question: can this already-open child session run the next compatible request without repeating setup or violating policy?

The key records capability metadata expectations as opaque generic metadata facts. lean-rs-worker can compare the expected and actual metadata envelopes, but it does not interpret downstream command versions or decide cache invalidation.

What The Pool Hides

Callers should not learn:

• worker ids or child pids;
• stdin/stdout pipes or frame order;
• child spawn and handshake sequencing;
• queue internals;
• stderr parsing or fatal-exit classification;
• restart timing;
• RSS sampling details;
• which session values are invalidated by a cycle;
• which warm worker is selected for a request.

Those details are volatile and operational. Keeping them private lets lean-rs-worker change scheduling, memory policy, batching, and future backend internals without rewriting downstream tools.

What Callers Still Know

Callers still own the facts that are part of their domain:

• capability identity;
• typed command request, row, and summary schemas;
• request values;
• timeout and cancellation intent;
• row commit policy after terminal success;
• row semantics, cache validity, ranking, reporting, and source provenance.

This is the same boundary as the worker capability layer. lean-rs-worker owns process and transport behavior; downstream crates own semantic commands and schemas. A lean-dup integration would map its own commands onto the pool, but lean-rs-worker should not grow first-party extract, features, index, or probe methods.

Failure And Memory Model

A child crash, request timeout, cancellation-triggered cycle, explicit cycle, or policy restart invalidates the sessions hosted by that child. The pool must report those outcomes distinctly so callers can distinguish downstream command failure from infrastructure failure.

Only process exit resets Lean process-global runtime and import state. SessionPool::drain() can release Rust-owned cached environments inside a child, but it is not an RSS reset. Pool memory policy therefore operates by admitting work, selecting warm sessions carefully, and cycling child processes when measured policy says a reset is needed.

The pool memory policy is local-child policy, not a remote placement model. Callers may configure worker count and RSS budgets, but they do not poll child RSS, inspect child pids, or decide which child to cycle.

Related docs

• 21-import-set-planning.md — stable work batches that make pool reuse effective.
• 22-worker-row-batching.md, 23-worker-data-plane-format.md — batching and data-plane format decisions.
• 24-lean-side-worker-streaming.md — Lean-side streaming helpers.
• 25-mathlib-scale-worker-fixture.md — mathlib-scale fixture.
• 26-worker-pool-observability.md — pool observability.
• 27-lean-dup-readiness.md — downstream readiness proof.
• 28-production-scale-release.md — production-scale contract.

Import Set Planning

The planner sits above the memory-aware worker pool and groups module work by the same facts the pool uses for session reuse, so downstream tools can avoid repeating Lean imports without learning worker process mechanics.

Crate Boundary

Two concerns are better apart:

Planner in lean-rs-worker. Rejected as the only layer. Worker sessions and pool keys matter for batching, but Lake module discovery is useful without a worker child process.

Discovery in lean-toolchain, batching in lean-rs-worker. Chosen. lean-toolchain owns Lake root detection, module-root discovery, module-name validation, source-set fingerprints, and capability-target declaration checks. lean-rs-worker owns the worker-facing batch plan because the batch key is a LeanWorkerSessionKey and feeds LeanWorkerPool leases.

This split keeps Lake layout policy in one general-purpose crate and keeps worker session policy in the worker crate. Neither crate learns downstream commands, row schemas, cache validity, ranking, or reporting.

Discovery

lean-toolchain::discover_lake_modules accepts a requested root and optional selected module roots. It resolves conventional Lake project locations, discovers lean_lib roots from lakefile.lean or lakefile.toml, enumerates Lean source modules deterministically, and returns:

• LeanModuleDescriptor values with module name, source path, and source root;
• LeanModuleSetFingerprint with the build-baked toolchain fingerprint, lakefile digest, optional manifest digest, source count, and maximum source mtime;
• typed LeanModuleDiscoveryDiagnostic errors for missing Lake roots, missing selected module roots, invalid module names, unsupported toolchains, and I/O failures.

The fingerprint carries cache-key-relevant facts. It does not decide whether a downstream cache entry is fresh.

Worker Batches

LeanWorkerImportPlanner consumes discovery output or explicit LeanWorkerModuleWork values. It groups work by:

• Lake project root;
• capability package and target;
• source root;
• import set;
• optional capability metadata expectation;
• Lean toolchain and lean-rs protocol fingerprint;
• restart-policy class.

Each LeanWorkerPlannedBatch contains a LeanWorkerSessionKey, module work items, a batch fingerprint, and enough capability material to create a LeanWorkerCapabilityBuilder. The plan contains no worker ids, child pids, pipe handles, protocol frames, queue positions, or scheduling decisions. The pool still decides which local child hosts a batch.

Downstream Use

A downstream tool should treat planned batches as execution groups, not cache records. The group says: “these modules can run against the same worker session requirements.” It does not say whether a declaration row, feature row, probe result, or report is valid for reuse. That remains downstream policy.

The import planner is therefore deliberately not a lean-dup API. A lean-dup integration can map its source modules into planned batches, then run typed worker commands through pool leases. lean-rs-worker still does not define extract, features, index, or probe methods.

Performance Claim

The fixture test records the shape rather than claiming universal speedup: naive per-module execution opened one worker capability per module, while the planned path used one batch and one pool worker. On a local run, two interop fixture modules took 1049 ms in the naive path and 573 ms through a single planned pool lease. Larger projects should use their own workload numbers before turning a batch plan into a cache or scheduling policy.

Worker Row Batching

Worker row frames are per-row, not batched. A measurement campaign on mathlib-scale streams showed batching neither improves throughput nor pays for the failure-mode complexity it adds. Batching stays out until a workload shows it improves the full worker path.

Boundary

The public row interface remains unchanged:

• typed downstream commands use LeanWorkerStreamingCommand<Req, Row, Summary>;
• schema-less callers can use LeanWorkerDataRow;
• raw JSON rows remain an internal fast path for typed decoding;
• no caller learns protocol frames, child pipes, worker ids, or batch boundaries.

This preserves the capability-layer boundary from 19-worker-capability-layer.md. Worker throughput work must deepen the worker implementation; it should not ask downstream tools to coordinate process or framing mechanics.

Measurement

The workload was the 512-row interop streaming export lean_rs_interop_consumer_worker_data_stream_many. Three variants of the worker, same fixture:

The protocol-batching microbenchmark (worker::row_payload::protocol_batching) compares per-row raw JSON framing against simulated batch sizes at the protocol layer alone:

The micro result does not justify adding a public batch sink, and the broader worker result rejects private batch frames.

Reproduce with:

cargo bench -p lean-rs-worker --bench row_payload -- \
  worker::row_payload::stream/typed_many_512 --quiet
cargo bench -p lean-rs-worker --bench row_payload -- \
  worker::row_payload::protocol_batching --quiet
cargo test -p lean-rs-worker --test streaming_runner \
  large_stream_records_live_forwarding_throughput_and_rss -- --nocapture

Decision

LeanWorkerDataBatch, a typed batch sink, and private DataRowBatch frames are not implemented. The live per-row protocol keeps stronger failure behavior: rows are forwarded as soon as Lean emits them, fatal exits after a row are still reported once the parent observes that row, and sink-driven cancellation remains row-boundary precise.

A future data-plane format change may still be benchmarked separately. Any batch work must show both a microbenchmark win and a broader pool/lease scenario win before adding public surface area.

Worker Data-Plane Format

The current JSON and raw-JSON row data plane is kept. Format candidates (MessagePack, CBOR, a manual binary envelope) were measured against large worker streams; none earned a protocol or public-API change.

Boundary

The normal downstream surface remains the worker capability layer:

• callers run typed commands through capability sessions or pool leases;
• typed commands decode downstream-owned request, row, and summary types;
• LeanWorkerDataRow and raw rows remain lower-level escape hatches;
• callers do not learn protocol frames, child pipe bytes, child ids, or callback handles.

The data-plane format is an implementation detail below that surface. Changing it is justified only by an end-to-end worker workload, not by a standalone encoding microbenchmark.

L1 callback payload expansion is deliberately unrelated. Same-process callbacks remain the lean-rs mechanism layer. Worker row throughput is a worker IPC question and should be solved with worker framing, scheduling, chunking, and measured encoding changes.

Measurement

The benchmark command was:

cargo bench -p lean-rs-worker --bench row_payload -- \
  worker::row_payload::data_plane --quiet

It compares serde_json::Value, Box<serde_json::value::RawValue>, batched raw JSON, a manual binary envelope carrying raw JSON payload bytes, MessagePack, and CBOR. The two named row shapes were:

• small_rows_8192: many small declaration-like rows;
• large_rows_512: fewer 4 KiB payload rows.

One representative frame size from each shape:

data_plane_size shape=small_rows_8192 value_json=97 raw_json=97 binary_json_payload=76 messagepack=40 cbor=76
data_plane_size shape=large_rows_512 value_json=4154 raw_json=4154 binary_json_payload=4133 messagepack=4108 cbor=4139

Median throughput (mid-range estimate, sorted by small-row speed):

End-to-end remeasurement of the current worker path:

cargo bench -p lean-rs-worker --bench row_payload -- \
  worker::row_payload::stream/typed_many_512 --quiet
# typed_many_512 ≈ 2 K rows/s

cargo run --release -p lean-rs-worker --example row_perf_probe
# worker_data_stream_many (512 rows): ~2.4 K rows/s, parent RSS ~6 MiB,
#   child RSS growth ~400 MiB
# worker_data_stream_large_payload (1 row): ~200 ms,
#   child RSS growth ~370 MiB

The encoding microbenchmarks dominate the end-to-end numbers by an order of magnitude: the bottleneck is elsewhere on the worker path, not in the row encoder. Re-capture on the same hardware before declaring a regression.

Decision

Keep the current public worker data plane and raw-JSON typed decode path.

The microbenchmarks identify two useful future candidates, but not a single format that should replace the worker protocol now:

• the manual binary envelope is the best small-row microbenchmark;
• MessagePack is the best large-row typed microbenchmark;
• CBOR does not win either workload;
• raw JSON remains much faster than serde_json::Value while preserving the existing typed command facade.

The winning microbenchmarks do not yet have a Lean-side, end-to-end worker path. Implementing either a binary envelope or MessagePack now would add protocol complexity before proving that it improves the real child process stream. The Lean-side worker helpers in 24-lean-side-worker-streaming.md remove envelope boilerplate while keeping the current raw-JSON row path. Future format work must show a broader worker or pool/lease benchmark win before changing the protocol or public API.

No LeanBytesEvent, object callback, raw frame API, MessagePack API, CBOR API, or binary row API is exposed.

Lean-Side Worker Streaming Helpers

Worker capability authors should not repeat the JSON envelope details needed by lean-rs-worker, but the helper package must not become a downstream command framework. The stable boundary is small Lean-side primitives in LeanRsInterop.Worker.Stream:

• jsonString escapes a Lean String as JSON text.
• row builds a worker row envelope with caller-owned stream and payload JSON.
• diagnostic builds a diagnostic envelope.
• progress and chunkProgress build progress envelopes.
• metadata builds the terminal metadata envelope.
• emitAll calls the in-process string callback trampoline inside the child process. Capability exports should build an array of envelopes locally and call emitAll once.
• countChunks computes chunk counts for downstream-owned chunk plans.

These helpers own worker callback-envelope mechanics. Downstream Lean code still owns request parsing, row schemas, semantic algorithms, command names, chunk contents, and terminal metadata shape. The Rust worker and pool still own worker selection, lease invalidation, memory policy, backpressure, cancellation, and timeout behavior.

Packaging Boundary

The helpers live in lean-rs-interop-shims, not in lean-rs-host-shims. That package is the reusable ABI layer for downstream Lean capabilities. It has no theorem-prover host policy, no declaration-query API, no session key logic, and no worker scheduling policy.

Worker parent-facing APIs still expose typed commands, rows, diagnostics, progress, summaries, and timeouts. They do not expose callback handles. LeanCallbackHandle<LeanStringEvent> stays inside the child as the bridge from Lean exports to private worker frames.

Chunking Decision

The verified helper path is envelope construction plus one callback loop per export. The fixture emits a chunked stream by building an array of envelopes with row, chunkProgress, diagnostic, and metadata, then calling emitAll once. Single-envelope convenience functions are intentionally absent: the active worker shared-library path is stable when the downstream capability constructs the envelope array and hands it to emitAll.

A more ambitious generic Lean-side chunk runner was tested and rejected for this prompt. Runtime helpers that looped over Array String in lean-rs-interop-shims, source macros that expanded the same loop, and single-envelope helpers that allocated a one-element array in the shared shim package caused the worker child to terminate with SIGSEGV under Lean 4.29.1 in the shared library worker path. The safe release surface therefore keeps chunk scheduling in downstream Lean code and factors only worker envelope construction plus emitAll into the helper package.

This is not a pool scheduling feature. Real parallelism for large workloads belongs in LeanWorkerPool, session leasing, import planning, and memory-aware admission. Lean-side helpers can emit progress at chunk boundaries, but they do not choose workers, spawn tasks, or define session keys.

Consumer Rule

Use these helpers when authoring a Lean capability that will be run through lean-rs-worker. They remove repeated worker-envelope boilerplate while keeping downstream schemas and algorithms downstream-owned.

Use direct L1 callbacks only for trusted same-process interop. Use lean-rs-host for trusted in-process theorem-prover sessions. Use lean-rs-worker or LeanWorkerPool when the caller needs process isolation, timeouts, memory cycling, row streaming, diagnostics, or pool orchestration.

Mathlib-Scale Worker Fixture

A large-workload fixture for the worker capability layer. It is deliberately not a lean-dup implementation; it uses mathlib-shaped module names and command-like exports to stress the operational boundary:

import planner -> LeanWorkerPool -> session lease -> typed command

Boundary

The fixture may simulate version, doctor, index, extract, features, and probe command shapes, but the row schemas remain small test data owned by lean-rs-worker fixtures. It does not copy lean-dup declaration rows, feature rows, cache rules, ranking, reporting, or source-provenance policy.

The normal path is the pool path:

• LeanWorkerImportPlanner groups module work into stable session batches.
• LeanWorkerPool chooses a compatible local child and returns a lease.
• A typed command runs through the lease.
• Rows, diagnostics, progress, terminal metadata, cancellation, timeout, fatal exits, and cycling use the same worker capability contracts as downstream callers.

Low-level worker calls remain useful for focused tests, but they are not the source-of-truth scale path.

Workload

The fixture export lean_rs_interop_consumer_worker_shape_mathlib_scale_index emits:

• declaration-like rows on the declarations stream;
• feature-like rows on the features stream;
• probe-like rows on the probes stream;
• start/finish diagnostics;
• chunk progress for the simulated import/index pass;
• terminal metadata with fixture name, command, row count, and module count.

The fallback workload uses 16 mathlib-shaped module names and emits 47 rows: 16 declarations, 16 features, and 15 probes. This keeps CI deterministic while still exercising mixed streams and terminal accounting.

When LEAN_RS_MATHLIB_ROOT points at a mathlib checkout, the mathlib_scale_probe example uses the discovered mathlib module list as the planning workload shape. The current fixture still emits deterministic test rows; a run with a mathlib module list is evidence about planning, pool leases, and session reuse, not a claim that lean-rs-worker has indexed mathlib semantics.

Commands

Build the fixture and run the focused tests:

cd fixtures/interop-shims && lake build
cargo test -p lean-rs-worker --test mathlib_scale_fixture -- --nocapture

Run the local scale probe:

cargo build -p lean-rs-worker --bin lean-rs-worker-child
cargo run -p lean-rs-worker --example mathlib_scale_probe

Use a real mathlib module list when available:

LEAN_RS_MATHLIB_ROOT=/path/to/mathlib4 \
LEAN_RS_MATHLIB_SCALE_LIMIT=128 \
cargo run -p lean-rs-worker --example mathlib_scale_probe

Run the benchmark group:

cargo build --release -p lean-rs-worker --bin lean-rs-worker-child
cargo bench -p lean-rs-worker --bench worker_capability -- mathlib_scale

Sample capture

On macOS/aarch64 with Lean 4.29.1, the fallback probe (16 modules, 47 rows) ran at ~140 rows/s for both single_worker and pool_max_2 (the fallback produces one planned batch, so pool_max_2 is a pool-API smoke test, not evidence of parallel speedup). Cancellation, fatal-exit recovery, and post-cycle replay all worked; RSS sampling was unavailable from ps on that machine. A claim about mathlib-scale performance must record the command, module limit, Lean version, and whether RSS sampling was available. Re-capture on the same hardware before declaring a regression.

Non-Goals

This fixture does not add remote workers, search/ranking/cache semantics, downstream row schemas, or new callback payloads. Worker throughput still flows through worker IPC, pool leases, scheduling, row formats, and batching decisions; L1 object callbacks are not a worker-scale shortcut.

Worker Pool Observability

The operating view for large local worker runs. The pool reports cheap snapshots and applies bounded row-delivery backpressure without exposing worker internals.

Boundary

LeanWorkerPoolSnapshot is the public summary type. It reports aggregate pool state:

• configured and active worker counts;
• warm lease count and queue depth;
• request/import counters;
• restart reasons;
• best-effort child RSS samples;
• streaming request success/failure counters;
• delivered row count and raw payload bytes;
• accumulated stream elapsed time;
• backpressure wait and failure counters.

A snapshot intentionally does not expose child pids, local worker ids, pipe handles, protocol frames, child stderr, or the selected warm worker. Those are supervisor and pool mechanics. Callers can sample the snapshot during a large run, log it, or use it to choose their own cancellation policy without learning how the child process is wired.

LeanWorkerSessionLease::snapshot provides the same aggregate shape for the leased worker while the lease is active. It is a sampling hook, not an identity handle. A stale lease remains stale after timeout, cancellation, crash, explicit cycle, memory policy restart, or metadata mismatch.

Backpressure

Worker row delivery uses a bounded internal event buffer between the supervisor reader thread and the request owner. When the request owner or row sink is slow, the reader blocks after the internal capacity is reached. That blocking propagates naturally to the child through the pipe instead of allowing unbounded parent memory growth.

Rows are never dropped for committed streams. A row delivered to the sink is still tentative until the terminal success response arrives. Sustained backpressure can be stopped by request timeout or cooperative cancellation; the request then returns a typed worker error and the affected session is invalidated according to the normal worker lifecycle rules.

Backpressure counters are observability, not an event bus:

• backpressure_waits counts reader-side waits on the bounded event buffer;
• backpressure_failures counts failed streaming requests that had already observed backpressure;
• data_rows_delivered counts rows successfully handed to the data sink;
• terminal summaries remain the source of committed row counts.

Diagnostics, progress events, data rows, and pool stats stay separate channels. Progress is control/observability; it is not a row stream. Diagnostics describe capability or worker issues; they are not downstream data.

RSS And Throughput

RSS sampling remains best effort. Unsupported platforms record unavailable samples rather than pretending that the pool can enforce a budget from missing data. A memory reset still means cycling the child process. In-process host cache draining does not reset Lean process-global RSS.

The mathlib-scale probe prints pool snapshot fields during normal typed-command execution and a slow-sink workload:

cargo build -p lean-rs-worker --bin lean-rs-worker-child
cargo run -p lean-rs-worker --example mathlib_scale_probe

The slow_sink line records parent RSS before/after, child RSS, delivered rows, payload bytes, and backpressure waits. Use those numbers as workload evidence; do not describe memory or throughput behavior as bounded without a recorded run.

Rejected Designs

Public worker identity metrics. Rejected. Child pids and worker ids make local process details part of the API and would complicate a future remote or alternate backend.

Unbounded row queues. Rejected. They make slow sinks a parent-memory leak under mathlib-scale streams.

Dropped rows. Rejected. Worker streams have commit-after-success semantics; dropping rows would make terminal success ambiguous for downstream schemas.

Metrics framework integration. Rejected for this layer. The pool exposes a cheap snapshot. Applications adapt it to logs, tracing, Prometheus, or another metrics backend outside lean-rs-worker.

Lean-Dup Readiness Proof

A boundary check showing that the generic worker foundation can replace the subprocess-worker shape used by a lean-dup-class tool. The lean-rs-worker pool hosts the operational responsibilities; downstream crates keep their schemas and semantic policy. This is not a lean-dup implementation and not a migration guide.

What The Proof Covers

The readiness example runs:

cargo run -p lean-rs-worker --example lean_dup_readiness

The example uses the normal large-scale path:

LeanWorkerImportPlanner -> LeanWorkerPool -> LeanWorkerSessionLease -> typed command

It exercises six command shapes through generic typed commands:

• version as a typed JSON command;
• doctor as a typed JSON command;
• extract as a typed streaming command;
• features as a typed streaming command;
• index as a typed streaming command;
• probe as a typed streaming command.

The fixture exports use command-like names only to stress the worker capability layer. They do not define declaration rows, feature rows, probe results, cache keys, ranking, report policy, or source provenance for lean-dup.

Responsibility Map

This deletes caller-owned subprocess plumbing: ad hoc child spawning, stdin JSON request writing, stdout JSONL framing, stderr parsing, EOF classification, manual timeout kills, manual restart sequencing, pipe-draining loops, and RSS/pool bookkeeping.

What Remains Downstream-Owned

A downstream project still owns:

• request, row, and terminal summary schemas;
• semantic algorithms for extraction, features, indexing, and probes;
• cache validity and persistence;
• ranking and reporting;
• source provenance and user-facing paths;
• command names and CLI policy;
• any compatibility decisions based on downstream metadata.

This is the intended split. lean-rs-worker carries typed commands, rows, diagnostics, terminal summaries, timeouts, cycling, backpressure, and pool state; it does not know what a downstream row means.

Comparison Input

A read-only downstream checkout (e.g., a lean-dup clone) can be supplied via the LEAN_RS_LEAN_DUP_ROOT environment variable. The readiness example records the checkout revision when the path is set and points to a git repository. If LEAN_RS_WORKER_COMPARE_COMMAND is also set, the example runs that command and prints its status and elapsed time. The comparison is optional because lean-rs-worker should not depend on a local downstream checkout.

Any comparison must name the command, revision, workload, and limits. Without that, the readiness proof only claims generic coverage and local worker-pool operating behavior.

Measured Local Envelope

The example prints:

• command-shape coverage and row counts;
• diagnostic and progress counts;
• terminal summary command names;
• timeout, cancellation, fatal-exit recovery, explicit cycle, and backpressure outcomes;
• pool snapshot counters;
• parent and child RSS when the platform permits sampling;
• optional subprocess comparison status.

Do not treat the fixture rows as lean-dup rows. They are small generic test data used to prove that the worker substrate can carry the shape.

Production-Scale Worker Release Contract

The release claim for lean-rs-worker as a local worker-pool foundation for mathlib-scale worker-class workloads, and the boundaries that must stay true.

Release Claim

LeanWorkerPool is the supported local orchestration boundary for mathlib-scale worker-class workloads. The normal path is:

LeanWorkerImportPlanner -> LeanWorkerPool -> LeanWorkerSessionLease
  -> typed command -> live rows -> terminal summary -> pool stats

The pool owns local scheduling, session leases, memory-aware admission, restart policy, backpressure, observability, and failure isolation. Callers do not choose child pids, worker ids, pipes, protocol frames, restart sequencing, or row-buffering mechanics.

The pool sits above LeanWorkerCapabilityBuilder. The builder knows how to open one capability-backed worker session. The pool decides when compatible work can reuse a warm session, when a new local child may be spawned, and when policy requires a cycle before more work is admitted.

What Callers Still Own

lean-rs-worker does not own downstream semantics. Downstream crates still define:

• command names and exported Lean functions;
• request, row, and terminal-summary serde types;
• row schemas and schema versions;
• cache validity and persistence;
• ranking, reporting, and source provenance;
• user-facing CLI or service policy.

This is why the lean-dup readiness proof uses command-like fixture names but does not define lean-dup rows or cache policy.

Data Plane

Worker throughput is handled through worker IPC, raw-JSON typed decoding, bounded row delivery, and measured batching/data-plane decisions. It is not handled through cross-process callback handles.

The worker keeps per-row frames and the raw-JSON typed decode path. The measured broader worker workloads did not justify public row batch sinks, binary row APIs, MessagePack, CBOR, Postcard, or a public protocol frame surface. LeanWorkerDataRow is the schema-less escape hatch; LeanWorkerStreamingCommand is the normal downstream streaming surface.

Callback Payload Decision

L1 callbacks are same-process interop mechanisms in lean-rs. They are useful for trusted extensions that intentionally run in the same process as Lean. They are not the scale path for worker-class tools.

Supported callback payloads are the sealed payloads already implemented: LeanProgressTick and LeanStringEvent. Byte callbacks are not exposed until a concrete same-process binary callback caller appears. Object callbacks are not exposed until a soundness proof produces a scoped API. Neither byte nor object callbacks are needed for worker row ergonomics.

Evidence

The scale claim is backed by named workloads, not by intent:

• pool API and lease tests cover reuse, death, cancellation, timeout, metadata mismatch, memory-policy invalidation, and typed command execution;
• memory scheduling workloads record fixture import reuse, mathlib-shaped fallback imports, repeated cycle/reuse, parent RSS, and child RSS or explicit RSS-unavailable status;
• row payload benches compare JSON tree rows, raw JSON, simulated batch frames, simulated binary envelopes, MessagePack, and CBOR;
• Lean-side helper tests cover streaming envelopes, chunked streams, diagnostics, progress, terminal metadata, and error conversion;
• the mathlib-scale fixture exercises planner, pool, lease, typed command, diagnostics, terminal summaries, cancellation, fatal-exit recovery, cycling, row throughput, and RSS sampling;
• pool observability tests cover snapshots and bounded backpressure;
• the readiness proof exercises generic version, doctor, extract, features, index, and probe command shapes without importing downstream schemas.

Numbers are machine-local. Any performance claim must name the workload, command, platform, row counts, throughput, RSS status, and caveats.

Non-Goals

Remote workers are future work. The local pool should avoid public APIs that would make a remote backend impossible, but this release supports only local child processes.

lean-rs-worker does not implement lean-dup, define downstream row schemas, add worker pools across machines, or expose new callback payload types.

Ship A Crate With Lean Code

Use this recipe when a Rust crate owns Lean source code and should build on another developer’s machine with ordinary Cargo commands.

Run The Template

From the repository root:

cargo run --manifest-path templates/shipped-lean-crate/Cargo.toml
cargo build --manifest-path templates/shipped-lean-crate/Cargo.toml --bin shipped-lean-crate-worker
cargo run --manifest-path templates/shipped-lean-crate/Cargo.toml --example worker

The first command builds the Lean shared library in build.rs and calls a Lean export in process. The second builds the app-owned worker child binary. The third starts that worker child and opens the same capability behind lean-rs-worker.

The template uses path dependencies because it lives inside this repository. Published crates use normal version dependencies:

[dependencies]
lean-rs = "0.1"
lean-rs-worker = "0.1" # only for worker apps

[build-dependencies]
lean-toolchain = "0.1"

File Layout

The canonical shape is build-time first:

1. build.rs builds the Lake shared-library target.
2. Rust opens the built dylib through lean-rs, or starts it behind lean-rs-worker.
3. Worker applications ship their own tiny worker-child binary.

The crate author names the Lake root, package, module, imports, and worker child binary. The helper APIs hide Lean link directives, Lake output paths, dylib env-var plumbing, worker protocol frames, pipes, and child startup sequencing.

Build The Lean Capability

Add lean-toolchain as a build dependency:

[build-dependencies]
lean-toolchain = "0.1"

Use the high-level helper in build.rs:

fn main() -> Result<(), Box<dyn std::error::Error>> {
    lean_toolchain::CargoLeanCapability::new("lean", "MyCapability")
        .package("my_app")
        .module("MyCapability")
        .build()?;
    Ok(())
}

This emits Lean link directives, Cargo rerun triggers, runs lake build MyCapability:shared, resolves Lake’s supported dylib naming conventions, writes a JSON artifact manifest, and emits:

cargo:rustc-env=LEAN_RS_CAPABILITY_MY_CAPABILITY_MANIFEST=<manifest path>
cargo:rustc-env=LEAN_RS_CAPABILITY_MY_CAPABILITY_DYLIB=<built dylib path>

The manifest path is the canonical runtime handoff. The dylib env var remains for compatibility and simple low-level callers.

Use build_lake_target directly only when a crate really needs lower-level control over the build-script policy.

Open The Capability In Process

For trusted same-process interop, embed the compile-time path with env!:

let runtime = lean_rs::LeanRuntime::init()?;
let capability = lean_rs::LeanCapability::from_build_manifest(
    runtime,
    lean_rs::LeanBuiltCapability::manifest_path(
        env!("LEAN_RS_CAPABILITY_MY_CAPABILITY_MANIFEST"),
    ),
)?;

let module = capability.module()?;
let add = module.exported::<(u64, u64), u64>("my_app_add")?;
let answer = add.call(40, 2)?;

LeanCapability is a convenience layer over LeanLibrary: it reads the manifest, opens the primary dylib and dependency bundle, initializes the configured module, and keeps the initializer names with the opened library. For doctor commands or installer checks, run LeanCapabilityPreflight against the same manifest descriptor first; it reports missing package files, unsupported toolchain fingerprints, stale manifests, and missing initializers with stable loader codes and repair hints.

Run The Capability In A Worker

Worker applications should ship an app-owned child binary. Do not rely on a dependency binary being installed automatically.

// src/bin/my_app_lean_worker.rs
fn main() -> std::process::ExitCode {
    lean_rs_worker::run_worker_child_stdio()
}

Then point the worker builder at that binary:

let spec = lean_rs::LeanBuiltCapability::manifest_path(
    env!("LEAN_RS_CAPABILITY_MY_CAPABILITY_MANIFEST"),
)
.manifest_env_var("LEAN_RS_CAPABILITY_MY_CAPABILITY_MANIFEST");

let builder =
    lean_rs_worker::LeanWorkerCapabilityBuilder::from_built_capability(&spec, ["MyCapability"])?
        .worker_child(
            lean_rs_worker::LeanWorkerChild::sibling("my_app_lean_worker")
                .env_override("MY_APP_LEAN_WORKER"),
        );

let report = builder.check();
if let Some(first) = report.first_error() {
    return Err(format!("worker bootstrap check failed: {}", first.message()).into());
}

let mut capability = builder.open()?;

The builder consumes the same manifest-backed descriptor as LeanCapability. It checks the worker child, capability artifact, protocol handshake, import session, and optional metadata expectation without exposing child pids, pipes, protocol frames, or loader environment variables. Typed commands, rows, diagnostics, timeout, and cycling remain behind the worker API.

Publishing Checklist

Keep the Lean source and Lake metadata in the published crate:

include = [
  "Cargo.toml",
  "build.rs",
  "src/**/*.rs",
  "lean/**/*.lean",
  "lean/lakefile.lean",
  "lean/lean-toolchain",
  "lean/lake-manifest.json",
]

Do not include .lake/; each downstream build should materialize Lake outputs for its local platform and Lean toolchain.

Gotchas

• Use env!("LEAN_RS_CAPABILITY_MY_CAPABILITY_MANIFEST"), not a runtime environment lookup, when the manifest is emitted by your own build.rs.
• Include Lean sources, lakefile.lean, lean-toolchain, and lake-manifest.json in the published crate.
• Exclude .lake/; it is platform- and toolchain-specific build output.
• Worker applications should ship an app-owned worker child binary that calls lean_rs_worker::run_worker_child_stdio.
• Do not rely on dependency binaries for the worker child; normal Cargo packaging does not install them as part of your application.
• Avoid nullary unboxed scalar exports in examples and app APIs. Give exported functions at least one argument, as in my_app_add, so Lake emits a function symbol rather than a persistent global.

The checked-in template under templates/shipped-lean-crate/ shows the full layout.

Downstream Lean/Rust Interop

Run the worked example from a clean checkout:

cargo run -p lean-rs --example interop_callback

The example stays below lean-rs-host. Rust builds a generic Lean interop shim target and a downstream-style Lake target, opens both dylibs through lean-rs, calls one ordinary Lean export, and then lets Lean call a Rust callback through LeanCallbackHandle.

This is the advanced L1 same-process path. Use it when the Lean extension is trusted, lives in the same process, and really needs to push data back into Rust before the exported function returns. Worker-style applications should start with worker-capability-runner.md, where lean-rs-worker hides callbacks behind typed commands, live rows, diagnostics, terminal summaries, timeouts, and worker cycling.

Files A Consumer Needs

A downstream package needs the same pieces as fixtures/interop-shims/:

• A Lake package with a lean_lib shared facet.
• A require lean_rs_interop_shims from ... line pointing at the bundled crates/lean-rs/shims/lean-rs-interop-shims package when Lean will call Rust callbacks.
• Explicit @[export] definitions for every Rust-callable Lean entry point.
• A Rust build script that calls lean_toolchain::emit_lean_link_directives_checked and lean_toolchain::build_lake_target.
• Rust code that opens the downstream capability as a LeanLibraryBundle when callback helpers add dependent Lean dylibs.

The build helper returns the dylib path. Consumers should pass that path through cargo:rustc-env=... or another build-script output of their choosing; they should not construct .lake/build/lib paths by hand.

Calling Lean From Rust

Lean exports are explicit ABI boundaries:

@[export lean_rs_interop_consumer_add]
def add (a b : UInt64) : UInt64 :=
  a + b

Rust opens the build-script capability, initializes the Lake module, resolves the exported symbol, and calls it through a typed handle:

#![allow(unused)]
fn main() {
let capability = LeanCapability::from_build_env(
    runtime,
    LeanBuiltCapability::path(env!("MY_CAPABILITY_DYLIB"))
        .package("my_package")
        .module("MyCapability"),
)?;
let module = capability.module()?;
let add = module.exported::<(u64, u64), u64>("lean_rs_interop_consumer_add")?;
let answer = add.call(20, 22)?;
}

The argument tuple and return type are checked by lean-rs’s sealed ABI traits. Unsupported Rust types fail at compile time.

Calling Rust From Lean In The Same Process

Callbacks are a low-level mechanism. They use the generic interop shim package:

@[export lean_rs_interop_consumer_callback_loop]
def callbackLoop (handle trampoline : USize) (total : UInt64) : IO UInt8 :=
  LeanRsInterop.Callback.Tick.loop handle trampoline total

Rust registers a callback and passes the opaque handle plus crate-owned trampoline to Lean:

#![allow(unused)]
fn main() {
let bundle = LeanLibraryBundle::open(
    runtime,
    env!("MY_CAPABILITY_DYLIB"),
    [LeanLibraryDependency::path(env!("LEAN_RS_INTEROP_SHIMS_DYLIB"))
        .export_symbols_for_dependents()
        .initializer("lean_rs_interop_shims", "LeanRsInterop")],
)?;
let module = bundle.initialize_module("my_package", "MyCapability")?;
let callback_loop =
    module.exported::<(usize, usize, u64), LeanIo<u8>>("lean_rs_interop_consumer_callback_loop")?;

let callback = LeanCallbackHandle::<LeanProgressTick>::register(|event| {
    eprintln!("{} / {}", event.current, event.total);
    LeanCallbackFlow::Continue
})?;
let (handle, trampoline) = callback.abi_parts();
let status = callback_loop.call(handle, trampoline, 4)?;
}

Keep the LeanCallbackHandle alive until Lean cannot call it again. Dropping the handle unregisters the id; a stale Lean call returns LeanCallbackStatus::StaleHandle instead of dereferencing freed Rust memory. Callbacks run synchronously on the Lean-bound thread and must not re-enter the same Lean call stack.

String callbacks use the same handle/trampoline lifetime rules with a different payload helper:

@[export lean_rs_interop_consumer_string_callback_loop]
def stringCallbackLoop (handle trampoline : USize) (payloads : Array String) : IO UInt8 :=
  LeanRsInterop.Callback.String.loop handle trampoline payloads

Rust registers LeanCallbackHandle::<LeanStringEvent> for that export. The trampoline copies the borrowed Lean string into an owned Rust String before calling user code. For a complete same-process string callback example, see string-callback-streaming.md.

What This Is Not

This is closer to PyO3/maturin in build wiring and typed calls, but it is not Python-style reflection. Lean does not expose a stable C API for discovering and invoking arbitrary definitions at runtime. A Lean/Rust boundary is an explicit @[export], and a downstream crate still builds a Lake target.

Use lean-rs-host only when the application needs theorem-prover host policy: sessions, imports, declaration introspection, elaboration, kernel checking, or bounded MetaM services.

Use lean-rs-worker when the application needs a production worker boundary: process isolation, memory cycling, live rows, diagnostics, terminal completion, timeouts, or worker-level cancellation. The worker parent API does not expose callback handles.

Same-Process String Callbacks

Run the example from a clean checkout:

cargo run -p lean-rs --example string_streaming

This recipe stays below lean-rs-host. It shows the advanced L1 same-process mechanism for sending strings from a Lean export to Rust through LeanCallbackHandle<LeanStringEvent>. lean-rs owns the callback handle, trampoline, string copy, stale-handle status, and panic boundary. Any row schema belongs to the downstream application.

Do not use this as the public interface for a worker-style tool. If the caller needs process isolation, live rows, diagnostics, terminal summaries, timeout policy, or memory cycling, use worker-capability-runner.md. The worker child may use string callbacks internally, but the parent-facing API is typed worker commands and row sinks.

Lean Export

The fixture under fixtures/interop-shims/ depends only on the generic interop shims:

require «lean_rs_interop_shims» from "../../crates/lean-rs/shims/lean-rs-interop-shims"

It exports a function that accepts the opaque callback handle and trampoline values, then sends a fixed sequence of strings through the string helper:

@[export lean_rs_interop_consumer_jsonl_stream]
def jsonlStream (handle trampoline : USize) : IO UInt8 :=
  LeanRsInterop.Callback.String.loop handle trampoline jsonlRows

Each payload is just a String. The example uses JSONL-like text only as a compact same-process demonstration; neither Lean nor Rust parses it here.

Rust Call Site

Rust builds the generic shim target and the downstream fixture target with lean_toolchain::build_lake_target, opens the generic shim dylib globally, then opens the consumer dylib normally.

The callback is typed to the string payload:

#![allow(unused)]
fn main() {
let rows = Arc::new(Mutex::new(Vec::new()));
let callback_rows = Arc::clone(&rows);
let callback = LeanCallbackHandle::<LeanStringEvent>::register(move |event| {
    callback_rows.lock().unwrap().push(event.value);
    LeanCallbackFlow::Continue
})?;
let (handle, trampoline) = callback.abi_parts();
let status = stream.call(handle, trampoline)?;
}

Keep the LeanCallbackHandle<LeanStringEvent> alive until the Lean export has returned and cannot call the handle again. Dropping the handle unregisters the id. A stale call returns LeanCallbackStatus::StaleHandle; it does not dereference freed Rust memory.

The trampoline copies the borrowed Lean string into an owned Rust String before it invokes user code, so no Lean object lifetime escapes the callback boundary.

Relationship To Progress

String streaming and host progress use the same callback registry, but they are different payloads:

• LeanProgressTick carries (current, total) counters. lean-rs-host maps it into LeanProgressEvent for session progress.
• LeanStringEvent carries one owned Rust String. Same-process downstream code can use it for line-oriented protocols such as JSONL.

Payloads are sealed. Downstream crates cannot implement arbitrary callback payloads or pass raw callback pointers to Lean.

Limits

This is not a transport framework and not the worker data-streaming interface. lean-rs does not define a JSON schema, parse rows, multiplex streams, or retry failed callbacks. It provides the typed Lean-to-Rust string callback boundary; application protocol belongs above it.

Worker Capability Runner

Run the capability runner from a clean checkout:

cargo run -p lean-rs-worker --example worker_capability_runner

This is the normal downstream shape for a project that wants a Lean worker process, live rows, typed decoding, diagnostics, timeout policy, terminal completion, and explicit worker cycling without writing a subprocess protocol. It uses the generic fixture under fixtures/interop-shims/; the command names are shaped like a downstream tool, but the row schemas are deliberately small fixture schemas.

If you are packaging your own application, start with ship-crate-with-lean.md. That recipe shows the build.rs helper, runtime capability open, and app-owned worker child binary. This page explains the worker capability behavior using the in-tree fixture.

What The Example Shows

The example opens a worker-backed capability with LeanWorkerCapabilityBuilder:

#![allow(unused)]
fn main() {
let mut capability = LeanWorkerCapabilityBuilder::new(
    workspace.join("fixtures").join("interop-shims"),
    "lean_rs_interop_consumer",
    "LeanRsInteropConsumer",
    ["LeanRsInteropConsumer.Callback"],
)
.validate_metadata(
    "lean_rs_interop_consumer_worker_shape_metadata",
    serde_json::json!({"source": "worker_capability_runner"}),
)
.open()?;
}

The builder builds the Lake target, resolves and starts lean-rs-worker-child, health-checks the child, opens the configured imports, and optionally validates generic capability metadata. The caller still names the Lake project, package, target, and imports because those identify the capability. The caller does not construct .lake/build/lib paths, wire stdio pipes, decode private frames, or repeat startup ordering.

Packaged applications should use the manifest-backed form shown in ship-crate-with-lean.md. The same builder exposes check() for startup probes and doctor commands; it validates the app-owned worker child, capability manifest/artifacts, worker handshake, import session, and optional metadata expectation before real work starts.

The row command uses the typed facade:

#![allow(unused)]
fn main() {
let command = LeanWorkerStreamingCommand::<ShapeRequest, ShapeRow, ShapeSummary>::new(
    "lean_rs_interop_consumer_worker_shape_index",
);
let summary = session.run_streaming_command(
    &command,
    &ShapeRequest::default(),
    &rows,
    Some(&diagnostics),
    None,
    Some(&progress),
)?;
}

ShapeRequest, ShapeRow, and ShapeSummary are ordinary serde types owned by the downstream crate. lean-rs-worker owns the transport: child lifecycle, private framing, live bounded row forwarding, typed diagnostics, progress events, request timeout, cancellation, terminal completion, and fatal-child classification.

Rows are live and tentative. A sink sees each row while Lean produces it, but the caller should commit buffered rows only after run_streaming_command returns terminal success. The terminal summary reports total row count, per-stream counts, elapsed duration, and optional downstream-defined metadata.

Channels

Keep the channels separate:

• Rows carry downstream data. The worker assigns per-stream sequence values and decodes payloads into the caller’s row type.
• Diagnostics carry worker or capability observations. They are delivered through LeanWorkerDiagnosticSink, not through row payloads.
• Progress carries coarse operation ticks. It is useful for user feedback and cancellation boundaries, but it is not the row stream.
• Terminal summary says whether delivered rows are committable.

LeanWorkerSession::run_data_stream remains available for low-level fixtures and schema-less tooling. Prefer typed commands for application code because decode errors include command, stream, and sequence context.

Timeout And Cycling

The example also runs a command that emits one tentative row and then sleeps. It lowers the request timeout and expects LeanWorkerError::Timeout. On timeout, the supervisor kills and replaces the child, records a timeout restart reason, and invalidates the open session. The example then explicitly cycles the worker and proves a later typed command succeeds in the fresh child.

Use cancellation when the caller knows it wants to stop and can wait for a row or progress boundary. Use request timeout as the parent-enforced watchdog for unresponsive Lean work.

What Downstream Projects Own

lean-rs-worker does not define business commands or row schemas. A downstream project still owns:

• semantic command names and export names;
• request, row, and terminal-summary serde types;
• cache validity rules;
• persistence and reporting;
• any ranking, indexing, or domain-specific interpretation.

The fixture uses command-like names such as version, doctor, extract, features, index, and probe only to exercise the generic worker capability layer. They are examples of shape, not APIs that lean-rs-worker reserves.

Worker Process Boundary

For the normal worker-capability path, start with worker-capability-runner.md. This page explains the lower-level process-boundary mechanics and the raw row escape hatch.

Run the worker streaming example from a clean checkout:

cargo run -p lean-rs-worker --example worker_streaming

The example uses LeanWorkerCapabilityBuilder to build the downstream Lake target, start a worker child, open a worker session, validate capability metadata, run a streaming Lean export, print JSONL-like rows, cycle the worker, and prove that the next request succeeds in a fresh child.

Use this path when the application needs process isolation or memory cycling. Use direct L1 callbacks, such as string-callback-streaming.md, when the Lean extension is trusted and same-process execution is acceptable.

What The Example Builds

The fixture at fixtures/interop-shims/ depends on the generic interop shims and exports:

@[export lean_rs_interop_consumer_worker_data_stream]
def workerDataStream (requestJson : String) (handle trampoline : USize) : IO UInt8 := ...

The worker runner fixes the ABI:

String request_json -> USize callback_handle -> USize callback_trampoline -> IO UInt8

request_json is downstream-owned request text. The child creates an in-process LeanCallbackHandle<LeanStringEvent>, passes the handle and trampoline to Lean, validates each callback string as a row envelope, and forwards rows to the parent as LeanWorkerDataRow values. The callback handle never crosses the process boundary.

Row Shape

Each callback string must be a JSON object:

{
  "stream": "rows",
  "payload": {
    "kind": "done",
    "ordinal": 1
  }
}

The parent receives:

#![allow(unused)]
fn main() {
pub struct LeanWorkerDataRow {
    pub stream: String,
    pub sequence: u64,
    pub payload: serde_json::Value,
}
}

stream is a caller-defined channel name. sequence is assigned by lean-rs-worker per stream inside one request. payload is arbitrary JSON. The worker validates the envelope and ordering mechanics; the downstream crate owns the row schema.

Rust Call Site

The preferred call site uses the typed command facade. The caller defines its own serde request, row, and terminal metadata types:

#![allow(unused)]
fn main() {
#[derive(serde::Serialize)]
struct ScanRequest {
    source: String,
}

#[derive(Clone, serde::Deserialize)]
struct ScanRow {
    kind: String,
    ordinal: u64,
}

#[derive(serde::Deserialize)]
struct ScanSummary {
    fixture: String,
    ok: bool,
}

struct Rows;

impl LeanWorkerTypedDataSink<ScanRow> for Rows {
    fn report(&self, row: LeanWorkerTypedDataRow<ScanRow>) {
        // Commit policy belongs to the caller. The row is still tentative
        // until the command returns terminal success.
        println!("{}:{} {:?}", row.stream, row.sequence, row.payload.kind);
    }
}
}

Then it builds and opens the worker-backed capability:

#![allow(unused)]
fn main() {
let mut capability = LeanWorkerCapabilityBuilder::new(
    "fixtures/interop-shims",
    "lean_rs_interop_consumer",
    "LeanRsInteropConsumer",
    ["LeanRsInteropConsumer.Callback"],
)
.validate_metadata(
    "lean_rs_interop_consumer_worker_metadata",
    serde_json::json!({"source": "worker_streaming_example"}),
)
.open()?;
}

The builder uses lean-toolchain::build_lake_target_quiet to materialize the Lake shared library, starts and health-checks the worker, opens the import session once, and stores the validated metadata. The caller names the Lake project, package, target, and imports because those are capability identity; it does not construct .lake/build/lib paths, locate the worker child by hand, or repeat startup ordering. The default resolver checks LEAN_RS_WORKER_CHILD, sibling Cargo profile paths, and the in-tree workspace development build. Packaged applications can set LEAN_RS_WORKER_CHILD or call worker_executable when the child binary is shipped outside those defaults.

Then it runs the export through a worker session:

#![allow(unused)]
fn main() {
let mut session = capability.open_session(None, None)?;
let command = LeanWorkerStreamingCommand::<ScanRequest, ScanRow, ScanSummary>::new(
    "lean_rs_interop_consumer_worker_data_stream",
);
let summary = session.run_streaming_command(
    &command,
    &ScanRequest {
        source: "worker_streaming_example".to_owned(),
    },
    &Rows,
    None,
    None,
    None,
)?;
assert_eq!(summary.total_rows, 2);
assert_eq!(summary.per_stream_counts["rows"], 2);
assert_eq!(summary.metadata.unwrap().ok, true);
}

Rows are live: the worker forwards each row while Lean produces it. They remain tentative until terminal success. If a caller needs atomic commit, it should buffer rows in its sink and commit them only after run_streaming_command returns Ok. The terminal summary reports total rows, per-stream counts, elapsed time, and optional downstream-defined metadata decoded into the caller’s summary type.

LeanWorkerSession::run_data_stream remains available for low-level fixtures and schema-less callers. It returns raw LeanWorkerDataRow values with serde_json::Value payloads. Production downstream code should prefer typed commands so row and summary decode errors are reported with command, stream, and sequence context.

The typed path is also the high-throughput path. Internally the worker keeps row payloads as validated raw JSON until it decodes them into the caller’s row type. The raw LeanWorkerDataRow escape hatch still parses payloads into serde_json::Value, which is convenient for ad hoc inspection but costs more on large streams.

Request timeout is configured on LeanWorkerConfig or changed on a live worker or session:

#![allow(unused)]
fn main() {
let config = LeanWorkerConfig::new(worker_child)
    .request_timeout(LEAN_WORKER_REQUEST_TIMEOUT_LONG_RUNNING);
}

Startup timeout only covers the child handshake. Request timeout covers one request after it has been sent, including live rows, diagnostics, progress, and terminal response. If it expires, the supervisor kills and replaces the child, returns LeanWorkerError::Timeout, records LeanWorkerRestartReason::RequestTimeout, and invalidates the open session.

Failure And Lifecycle Rules

Malformed row JSON, missing stream, and missing payload are typed worker errors. Nonzero downstream status bytes are typed worker errors. Lean internal panics and aborts kill the child, not the parent; the supervisor reports the fatal child exit.

Progress and diagnostics use typed worker messages. They do not share the row schema. A streaming request may take a LeanWorkerDiagnosticSink for diagnostic events; data rows remain downstream data. Use cancellation when the caller knows it wants to stop and can wait for a row or progress boundary. Use request timeout as a parent-enforced watchdog for unresponsive Lean work; it may kill the child without cooperative cleanup.

Capability discovery uses metadata and doctor exports, not row streams. The worker’s own protocol facts come from LeanWorker::runtime_metadata. A downstream capability can also expose JSON-returning exports with ABI String -> IO String; LeanWorkerSession::capability_metadata decodes command names, capability names, semantic versions, optional Lean version text, and extra JSON, while LeanWorkerSession::capability_doctor decodes pass, warning, and error diagnostics. The worker validates the generic envelope, but the downstream crate decides which versions affect cache keys.

LeanWorkerCapabilityBuilder::validate_metadata runs the metadata export during setup when the caller wants metadata as a startup contract. Doctor checks remain an explicit request because they may be slower or environment-specific.

Cycling the worker is the memory-reset boundary. SessionPool::drain() remains an in-process cache operation; it is not an RSS reset.

lean-dup Readiness

For a downstream tool such as lean-dup, this replaces ad hoc runtime Lean subprocess management:

• Lake build stays build-time and uses lean-toolchain.
• Worker startup replaces hand-written Command setup for runtime Lean work.
• JSONL-like rows are projected from LeanWorkerDataRow by the downstream tool; lean-rs-worker does not define lean-dup business objects.
• Progress and diagnostics use typed worker channels, not stdout conventions.
• Metadata and doctor checks report cache/support facts without baking lean-dup command semantics into lean-rs-worker.
• Fatal exits become typed worker failures that the parent can classify.
• Cancellation and timeout policy are caller decisions layered over worker requests.

The result is a process boundary with structured rows, not a lean-dup protocol embedded in lean-rs-worker.

Operational Fixture

For a larger worker-capability check, run:

cargo run --release -p lean-rs-worker --example worker_capability_probe

The probe uses fixture exports with command-like names version, doctor, extract, features, index, and probe. These names exercise the same operational shape as a downstream semantic worker, but the schemas are generic: rows contain small declaration, feature, and probe-like JSON objects owned by the fixture, not lean-dup business types.

The probe records:

• cold builder startup;
• first import/session opening;
• import-once streaming row throughput;
• cancellation latency at a row boundary;
• fatal child-exit recovery;
• explicit worker cycling;
• parent and child RSS samples.

Use it as an envelope check for the worker capability layer. It is not a lean-dup parity benchmark. If you want a local comparison against an existing subprocess worker, pass the command explicitly:

LEAN_RS_WORKER_COMPARE_COMMAND='cargo run -p lean-dup -- --help' \
  cargo run --release -p lean-rs-worker --example worker_capability_probe

Record the exact command, revisions, and output limits with any comparison. The comparison command is outside the lean-rs-worker contract.

Long-Session Memory

Repeated fresh Lean.importModules calls in one process drive resident set size from tens of MiB into the GiB range and never give it back. Steady operations against a reused imported environment (bulk introspection, elaboration, kernel checks, MetaM) do not accumulate. The shipped consumer pattern follows directly: pool imported environments, and cycle the worker process when an import sweep exhausts the pool.

The rest of this document records what Drop reclaims, what the reproducer measures, and what shape the measurement has on the supported toolchains.

Retention Model

lean-rs has several lifetime boundaries. Drop reclaims only the Rust-owned Lean reference counts attached to those boundaries; it does not reset Lean’s process-global runtime state.

The split has direct support in Lean’s own sources. The runtime reference requires foreign code to initialize the runtime before calling any Lean code, and the FFI reference describes Lean-owned objects as reference-counted. initialize/init.cpp initializes core libraries once per process; include/lean/lean.h documents compact-region and persistent objects as bypassing normal reference counting; library/module.cpp loads .olean data through compacted regions. Module-initializer state is idempotent on both the C++ side (_G_initialized short-circuit, used by crates/lean-rs/src/module/initializer.rs) and the interpreted side (Compiler.InitAttr tracks already-run initializers).

References:

• Lean Reference Manual, Run-Time Code
• Lean Reference Manual, Foreign Function Interface

Reproducer

The retained-memory counterpart to the latency benches. It runs one long-lived process through fresh imports, pooled reuse, bulk introspection, and elaboration, printing RSS checkpoints in KiB (ps -o rss=) and SessionPool counters between phases.

cd fixtures/lean && lake build && cd -
LEAN_RS_NUM_THREADS=1 cargo run --release -p lean-rs-host --example long_session_memory

The default workload is RSS-shaped, not latency-shaped:

• 192 fresh import/drop acquisitions through SessionPool::with_capacity(runtime, 0).
• 192 bounded-pool acquisitions through SessionPool::with_capacity(runtime, 4).
• 512 query_declarations_bulk calls over 16 fixture names.
• 512 elaboration calls, 50/50 success vs. diagnostic-producing terms.
• Snapshots before/after runtime init, host/capability load, import loops, bulk introspection, elaboration, drop, and a short steady-state pause.

Environment overrides:

LEAN_RS_LONG_SESSION_IMPORTS=64 \
LEAN_RS_LONG_SESSION_BULK=512 \
LEAN_RS_LONG_SESSION_ELAB=512 \
LEAN_RS_LONG_SESSION_POOL_CAPACITY=4 \
LEAN_RS_LONG_SESSION_CHECKPOINT_EVERY=16 \
LEAN_RS_NUM_THREADS=1 \
cargo run --release -p lean-rs-host --example long_session_memory

This is not a Criterion bench by design. Criterion answers per-iteration latency questions; this workload answers whether RSS returns at lifetime boundaries after LeanSession, SessionPool, and Obj<'lean> drops. A single long-running process with named checkpoints answers that directly.

Measured Shape

The numbers below are local snapshots on macOS aarch64 against lean=4.29.1. They are not portable: macOS RSS is noisy under memory pressure and compression, and absolute KiB values vary between machines. The shape—order-of-magnitude growth during fresh imports, flat reuse, flat introspection and elaboration, no return to baseline after drop—is the load-bearing claim and reproduces across the supported window.

Fresh-import-then-drop, capacity 0:

Sixteen imports of the fixture workload move RSS from ~50 MiB into the multi-GiB range, despite a pool capacity of zero and every session environment being dropped immediately.

Full sweep with LEAN_RS_LONG_SESSION_IMPORTS=64:

The pool counters confirm the Rust-side bookkeeping:

fresh_import_drop  imports=64 reused=0  acquired=64 released_to_pool=0  released_dropped=64
bounded_pool       imports=4  reused=64 acquired=68 released_to_pool=68 released_dropped=0
mixed_before_drop  imports=1  reused=0  acquired=1  released_to_pool=1  released_dropped=0

Three attributable findings:

• Fresh imports drive growth. Repeated Lean.importModules calls grow RSS even when every imported environment is dropped immediately.
• Reuse is flat. Bulk introspection (512 calls), elaboration (512 calls), and bounded-pool reuse (64 acquires across 4 cached environments) add no measurable RSS.
• Drop does not return RSS to baseline. Dropping the pool and session after the sweep does not reclaim the imported-module residue.

Open questions the reproducer does not answer: how the retained bytes split between interned names, globally registered module state, compacted .olean regions, and mimalloc arena retention; behaviour on mathlib or other large downstream module sets; cross-toolchain variation beyond the current resolved version.

Recycling API

SessionPool::drain() is the shipped recycle surface. It drops every cached free-list environment, increments PoolStats::{drains, drained}, and leaves checked-out PooledSession values valid. It is useful at idle boundaries when a worker wants to release Rust-owned cached environments without discarding the pool object. It is not an RSS reset: the process-global Lean state in the retention model above remains live until the process exits.

LeanRuntime::recycle() and LeanCapabilities::reopen() are not provided. The safe Rust lifetime model treats LeanRuntime::init() as a process-once anchor: every Obj<'lean>, LeanSession<'lean, '_>, LeanCapabilities<'lean, '_>, and SessionPool<'lean> value is tied to that borrow. An in-process recycle would have to prove that no Lean-derived value, cached symbol address, thread-local runtime attachment, task, initializer global, or persistent object from the old runtime can be observed after reinitialization; Lean’s embedding surface provides no global stop-the-world / finalize / reinitialize contract strong enough to back that claim. Reopening capabilities was rejected for a separate reason: the measured growth is not attributable to loaded dylib handles or symbol-resolution caches.

Consumer Pattern

Reuse imported environments. Keep a small SessionPool keyed by the import set and run introspection, elaboration, kernel checks, and MetaM calls against pooled sessions. Steady operations against a warm environment do not accumulate RSS.

Avoid repeatedly creating fresh imported environments in one process. If a workload must sweep many distinct import sets, put a process boundary around the sweep: restart the worker after a bounded number of fresh imports. Sixty-four fresh imports of the fixture workload were already enough to push RSS into the multi-GiB range; use a lower limit for larger module sets.

Call SessionPool::drain() when a worker is idle, when a project closes, or before handing a worker to a different stable import set. Drain cadence is policy for the embedding application: drain releases cached environments, but cannot bound workloads that continuously create fresh import sets. Those still require cycling the worker process at a bounded import count or RSS ceiling.

lean-rs-worker provides that process-cycling policy. Its restart policy can cycle explicitly, before a configured request count, before a configured import-like request count, after an idle interval, or when a best-effort child RSS sample reaches a ceiling. The worker memory reproducer is:

cargo build -p lean-rs-worker --bin lean-rs-worker-child
LEAN_RS_WORKER_MEMORY_IMPORTS=6 \
LEAN_RS_WORKER_MEMORY_MAX_IMPORTS=2 \
cargo run -p lean-rs-worker --example memory_cycling

On a local macOS aarch64 run, the worker cycled after every two import-like fixture requests. Child RSS moved from about 345 MiB after the first request in each child to about 717 MiB after the second request, then returned to about 345 MiB in the replacement child. This supports the operational claim: process cycling bounds retained RSS for this workload; in-process drain does not reset it.

LeanWorkerPool applies the same memory fact at the local orchestration layer. Pool policy can reject new distinct workers when known total child RSS reaches a budget, cycle a warm worker when its sampled RSS reaches a per-worker ceiling, cycle idle workers, and bound admission waits for a full pool. RSS sampling remains best effort and platform-specific: an unavailable sample is recorded as unavailable, not treated as proof that the pool is under budget. The pool memory-scheduling workload is:

cargo build -p lean-rs-worker --bin lean-rs-worker-child
cargo run -p lean-rs-worker --example pool_memory_scheduling

Use the pool knobs to avoid multiplying Lean import RSS across many local children. They do not change the underlying reset rule: only process exit resets Lean process-global retained memory.

Unsafe Inventory

Every unsafe block and pub unsafe fn in the workspace, paired with two things: the caller’s precondition (what the call site must guarantee before invoking) and the block’s invariant (what it promises in return). Audience: auditors reviewing the safety story, and maintainers about to change an unsafe seam.

Maintenance rule. Any commit that adds, removes, or reshapes an unsafe block must update the matching row in this file in the same commit. CI catches unsafe without a // SAFETY: comment (the missing_safety_doc lint at warn); this file catches the inverse—invariants that drifted away from what the code actually relies on.

The thesis these invariants serve is in docs/architecture/01-safety-model.md. Raw lean_* symbols enter the workspace only through lean-rs-sys; lean-rs consumes them through narrow per-file #![allow(unsafe_code)] opt-outs; lean-toolchain has no unsafe.

lean-rs-sys—the load-bearing boundary

lean-rs-sys is the one crate-wide #[allow(unsafe_code)] opt-out (crates/lean-rs-sys/src/lib.rs:32). lean_object is opaque ([u8; 0] + PhantomData<(*mut u8, PhantomPinned)>) and downstream code reaches state only through pub unsafe fn helpers. Each helper documents its caller obligations in a # Safety block; each in-body unsafe { ... } restates the ABI/layout invariant it relies on.

The blanket allow is justified by two cross-checks:

• SUPPORTED_TOOLCHAINS digest pins lean.h bytes across every release in the supported window.
• REQUIRED_SYMBOLS link-time test confirms every symbol the inline helpers cast through is exported by libleanshared for every release in the window.

Each table below groups blocks by pub unsafe fn; the function-level # Safety doc is the authoritative statement, and in-body blocks rely on the same caller obligations.

crates/lean-rs-sys/src/object.rs—13 pub unsafe fn, 12 blocks

Object inspection, tagging, and runtime-mode reads. Mirrors lean.h:312–630.

crates/lean-rs-sys/src/refcount.rs—6 pub unsafe fn, 8 blocks

Refcount fast paths. The atomic operations go through AtomicI32::from_ptr(&raw mut (*repr).m_rc) (Rust 1.75+), so the load/store/fetch_sub sites see a safe &AtomicI32.

crates/lean-rs-sys/src/ctor.rs—24 pub unsafe fn, 36 blocks

Constructor objects, polymorphic boxing, per-width scalar getters and setters. Mirrors lean.h:642–760 and lean.h:2811–2873.

crates/lean-rs-sys/src/array.rs—11 pub unsafe fn, 13 blocks

Object arrays (Array α) and scalar arrays (ByteArray, FloatArray, …). Mirrors lean.h:815–1028.

crates/lean-rs-sys/src/closure.rs—7 pub unsafe fn, 8 blocks

Closure objects. Mirrors lean.h:762–813.

crates/lean-rs-sys/src/string.rs—5 pub unsafe fn, 6 blocks

String objects. Mirrors lean.h:1157–1234.

crates/lean-rs-sys/src/scalar.rs—12 pub unsafe fn, 12 blocks

Boxed-scalar conversions. Mirrors lean.h:1356–2065.

crates/lean-rs-sys/src/io.rs—5 pub unsafe fn, 6 blocks

IO result helpers. Mirrors lean.h:2893–2907.

crates/lean-rs-sys/src/external.rs—3 pub unsafe fn, 3 blocks

External objects (C void* payloads). Mirrors lean.h:295–1332.

Other lean-rs-sys files

• init.rs—0 blocks; 7 extern declarations (lean_initialize, lean_initialize_runtime_module, lean_initialize_thread, lean_finalize_thread, lean_setup_args, lean_init_task_manager, lean_init_task_manager_using, lean_finalize_task_manager). Calling any of them is unsafe per Lean’s runtime entry-point rules: lean_initialize exactly once per process; lean_initialize_thread paired with lean_finalize_thread on every worker thread; lean_setup_args argv must outlive readers.
• nat_int.rs—0 blocks; bignum externs from lean.h:1334–1853 (lean_cstr_to_nat, lean_cstr_to_int, bignum arithmetic helpers).
• repr.rs—1 block in a #[cfg(test)] layout assertion that the in-memory layout matches the bytes pinned by every SUPPORTED_TOOLCHAINS entry. Production paths never touch repr directly except through layout casts in the inline accessors of the sibling modules.
• lib.rs—1 block and 2 pub unsafe fn; the block forwards a discovery helper returning a &'static view of the REQUIRED_SYMBOLS table. The unsafe is the caller’s invariant that the link-time test has succeeded.
• consts.rs, types.rs—0 blocks. consts.rs holds the build.rs-resolved version and digest constants. types.rs defines opaque lean_object and calling-convention typedefs; its one pub unsafe fn is a Default-like constructor stub with no body that callers cannot reach.

lean-rs—per-file opt-outs

Every block below ultimately calls a pub unsafe fn from lean-rs-sys; the invariant is what that # Safety doc requires, satisfied by the call site’s local context. Per-file #![allow(unsafe_code)] keeps the opt-out as narrow as the safety model demands.

Runtime—crates/lean-rs/src/runtime/

runtime/obj.rs—19 blocks (#![allow(unsafe_code)] at line 20)

Owned (Obj<'lean>) and borrowed (ObjRef<'lean, 'a>) handles. Six production blocks plus test-module RC observations.

runtime/init.rs—3 blocks (#![allow(unsafe_code)] at line 14)

LeanRuntime::init calls lean_initialize_runtime_module, lean_initialize, and lean_init_task_manager. The triple block at line 106 carries one // SAFETY: comment covering all three: process-once initialisation, sequenced as Lake’s compiler expects.

Line 128—unsafe { NonNull::<LeanRuntime>::dangling().as_ref() }—synthesises the ZST &LeanRuntime from the runtime cell pointer; sound because LeanRuntime is zero-sized and the caller has just verified the cell is initialised.

runtime/thread.rs—3 blocks (#![allow(unsafe_code)] at line 13)

LeanThreadGuard::attach calls lean_initialize_thread; Drop calls lean_finalize_thread. The blocks at lines 67 and 84 each pair an attach / finalize on the same OS thread, guarded by an RAII handle that cannot be Send (the FFI calls require thread-local Lean state).

ABI—crates/lean-rs/src/abi/

Every block in this directory either (a) wraps a freshly-allocated Lean value as a fresh Obj<'lean> via Obj::from_owned_raw (sys symbol is the matching lean_alloc_* or lean_*_to_nat), or (b) inspects a borrowed object’s header via a sys predicate (lean_is_scalar, lean_is_ctor, lean_obj_tag, lean_ctor_num_objs, …).

Module—crates/lean-rs/src/module/

module/library.rs—6 blocks (#![allow(unsafe_code)] at line 32)

Calls libloading::Library::new (line 112) and library.get (lines 186, 212, 233, 253). All unsafe for dlopen-time reasons: the loaded library may run constructors, and resolved symbols are typed by the caller.

module/initializer.rs—4 blocks (#![allow(unsafe_code)] at line 34)

Calls a Lake-emitted module initializer function pointer (line 198, wrapped in catch_unwind) and wraps the returned IO α result as an Obj (line 218). Block 116 is a from_utf8_unchecked on bytes already validated by the symbol-bytes builder.

module/exported.rs—7 blocks (#![allow(unsafe_code)] at line 59)

The typed LeanExported::call machinery. Each block at lines 246, 310, 314, 473, 489, 512, 517 either wraps a freshly-returned lean_object* as an Obj, transmutes between R::CRepr and *mut lean_object (line 517—sound because R: LeanAbi constrains CRepr to either a scalar primitive or *mut lean_object), or dispatches the function-pointer call through the per-arity macro.

Fuzzing entry—crates/lean-rs/src/fuzz_entry.rs

Feature-gated by fuzzing (off by default, not semver-stable). Seven pub unsafe fn wrappers (decode_string, decode_bytearray, decode_array_u64, decode_option_u64, decode_except, decode_nat_u64, decode_ctor_tag) plus seven matching inner blocks. Each takes a *mut lean_object owning one transferred refcount and wraps it in an Obj<'lean> via unsafe { Obj::from_owned_raw(runtime, raw) }; the invariant is the same as Obj::from_owned_raw’s # Safety doc, discharged by the fuzz harness constructing inputs through lean-rs-sys’s public allocators. The module sits at the crate root so the pub(crate) abi boundary stays intact when the feature is off.

Error—crates/lean-rs/src/error/

error/io.rs—16 blocks (#![allow(unsafe_code)] at line 28)

The IO α result decoder. Blocks at lines 64, 69, 73, 80, 125, 136, 153, 158, 163, 165, 169, 175 read the IO.Error constructor’s fields via lean_io_result_*, lean_obj_tag, lean_ctor_num_objs, lean_ctor_obj_cptr, lean_is_scalar, lean_is_string, lean_string_cstr/lean_string_len. The test-support block at line 247 transmutes a resolved dlsym address into a typed function pointer.

error/panic.rs—0 blocks

catch_callback_panic is pure safe Rust around std::panic::catch_unwind.

Host—crates/lean-rs/src/host/

host/session.rs—16 blocks (#![allow(unsafe_code)] at line 89)

Each LeanSession method that dispatches into a Lake-installed function constructs a typed LeanExported via unsafe { LeanExported::from_function_address(runtime, address) }. The address comes from SessionSymbols, populated by one dlsym per symbol at capability load. from_function_address’s # Safety requires the address to have been resolved as the correct typed symbol; SessionSymbols::resolve is the one place that obligation is discharged.

host/handle/{name,level,expr,declaration}.rs—1 block each (per-block)

Each constructs the public handle’s inner Obj from a freshly-returned lean_object* produced by a fixture export. Invariant is the LeanExported::call return contract.

host/elaboration/failure.rs—2 blocks (#![allow(unsafe_code)] at line 14)

lean_ctor_get_uint8 reads the Severity byte off the failure ctor.

host/elaboration/diagnostic.rs—5 blocks (#![allow(unsafe_code)] at line 25)

lean_ctor_get_uint8, lean_is_scalar, lean_unbox, lean_obj_tag reads on the diagnostic ctor and its severity tag.

host/evidence/handle.rs—1 block (per-block)

Wraps the evidence handle’s Obj from a fixture-returned pointer.

host/evidence/status.rs—2 blocks (per-block, lines 103 and 108)

Reads the EvidenceStatus scalar tag (lean_is_scalar + lean_unbox), with a heap-ctor fallback gated by lean_obj_tag (not currently triggered but kept for forward-compat with a Lean representation change).

lean-toolchain—0 unsafe blocks

rg -n "unsafe" crates/lean-toolchain/src returns nothing. The crate is build-time-only (toolchain discovery, fingerprinting, link diagnostics) and consumes lean-rs-sys constants through their safe re-export. Any new unsafe here would require a #![allow(unsafe_code)] opt-out with reviewer sign-off per docs/architecture/01-safety-model.md.

Sanitizer and leak-check coverage

Local—AddressSanitizer on Linux nightly

rustup toolchain install nightly --component rust-src
RUSTFLAGS="-Z sanitizer=address -Cdebug-assertions=on" \
RUSTDOCFLAGS="-Z sanitizer=address" \
cargo +nightly test -p lean-toolchain --target x86_64-unknown-linux-gnu \
  -- --test-threads=1

-Z sanitizer=address instruments pure-Rust helper code. CI intentionally does not run in-process Lean runtime tests under Linux ASan: Lean’s shared runtime is not ASan-instrumented and currently crashes the sanitizer before it can produce actionable Rust diagnostics. The in-process Lean paths are instead covered by normal workspace tests, loader regressions, worker crash-containment tests, and the release/manual ABI fuzz target. Loader-negative-path regressions also run outside ASan because they intentionally exercise platform dynamic-loader failure behavior with uninstrumented Lean shared libraries. --test-threads=1 preserves the per-thread Lean runtime invariant for the helper checks that do touch runtime discovery.

Local—fuzz target (Linux or macOS, nightly)

rustup toolchain install nightly --component rust-src
cargo install cargo-fuzz                 # one-shot
(cd crates/lean-rs/shims/lean-rs-interop-shims && lake build)
(cd fixtures/lean && lake build)
cd crates/lean-rs/fuzz
cargo +nightly fuzz run abi_decode -- \
  -runs=200000 -max_total_time=120

abi_decode drives lean_rs::abi’s {string, bytearray, array, option, except, structure} decoders with Arbitrary-generated Lean-shaped inputs constructed via lean-rs-sys’s public helpers. Every input must decode to Ok(_) or Err(LeanError::Host(stage = Conversion)); any panic, exception kind, or sanitizer-detected fault is a finding.

CI

A dedicated workflow at .github/workflows/sanitizer.yml runs the Rust-only Linux ASan command above on ubuntu-latest nightly and runs loader regressions outside ASan. The ASan job runs on every push to main, every pull request, a weekly cron, and manual dispatch. The ABI fuzz smoke is manual-only in the sanitizer workflow and is a release gate in .github/workflows/release.yml; it is not part of routine push/PR CI. The stable workspace matrix at .github/workflows/ci.yml is unchanged.

Coverage gaps

• macOS AddressSanitizer is not yet run in CI. ASan is available on aarch64-apple-darwin nightly, but the interaction between Lean’s runtime (libleanrt links its own mimalloc) and ASan’s allocator-shim on macOS has not been validated. Open future work.
• Miri does not cover the Lean C runtime. Miri can validate the pure-Rust seams in lean-rs-sys (refcount mirror’s AtomicI32::from_ptr, layout casts in repr tests, NonNull arithmetic on mock pointers), but it cannot execute libleanshared. The safety-test guidance in docs/architecture/01-safety-model.md accepts this by naming sanitizers and stress tests as the alternative.

Testing

The workspace gate is cargo-nextest, not cargo test. cargo test (single-process) is not the gate—cumulative Lean state OOMs the binary after ~150 tests (see Why nextest below).

Run the suite

Install once:

cargo install cargo-nextest --locked

Run:

cargo nextest run --workspace

Doctests are not picked up by nextest:

cargo test --doc --workspace

Tuning

The workspace’s .config/nextest.toml caps concurrent test processes at 4 so total memory stays bounded across CI runners (~7 GiB on {ubuntu-latest, macos-latest}). The workspace’s .cargo/config.toml sets LEAN_RS_NUM_THREADS=1 so each Lean process spawns a single worker thread; product is at most 4 Lean workers across the full run.

Unset LEAN_RS_NUM_THREADS (unset LEAN_RS_NUM_THREADS in the shell, or prefix the command with LEAN_RS_NUM_THREADS=) when you need Lean to use its own worker-count heuristic—typically for benchmarks.

Per-process Lean threads

The Lean task manager starts in LeanRuntime::init. By default worker count is Lean’s compiled-in heuristic (typically one worker per hardware core). Set LEAN_RS_NUM_THREADS to a positive integer before the first init call to pin the count for the process; invalid values fall back to the Lean default with a tracing::warn!. See the LeanRuntime::init docstring at crates/lean-rs/src/runtime/init.rs for the full contract.

CI

CI runs the ci nextest profile (cargo nextest run --workspace --profile ci), which adds one automatic retry on transient failures. See .github/workflows/ci.yml.

Why nextest

Each test that exercises a LeanSession imports LeanRsFixture.Handles, which transitively imports the full Lean compiler environment. Per-test working set is several hundred megabytes. In single-process cargo test, Lean’s interned name table, mimalloc heap, and globally-registered environments grow monotonically across tests—Drop releases per-session refcounts but cannot reclaim what Lean’s process-global tables hold. After ~150 of ~225 tests, a developer machine or CI runner with limited memory OOMs (observed: macOS memorystatus kills the process at ~30 GB compressed memory).

cargo nextest run runs each test in its own process, so cumulative Lean state resets at every process boundary.

Why not fix the cumulative growth instead

Two alternatives, both rejected:

• Hoist LeanHost / LeanCapabilities into per-binary shared state. The LeanHost: !Send + !Sync contract (docs/architecture/04-concurrency.md) prevents this; OnceLock/LazyLock require Sync.
• Find and fix the leak. Lean’s interned name table and mimalloc retention are process-global by design; the work-to-payoff ratio is poor compared to process isolation.

Nextest’s process-per-test model dissolves both problems with no public-API churn. The trade-off is wall-clock cost from repeated cold LeanRuntime::init calls; on a 12-core M4 Pro the full suite runs in ~30 seconds—well under the inner-loop attention threshold.

Performance

Benchmarks and the regression-detection recipe. Numbers themselves are not tracked here; they are non-portable across machines and ship with each capture.

Run the benches

cargo bench -p lean-rs --bench hot_paths
cargo bench -p lean-rs-host --bench session
cargo bench -p lean-rs-worker --bench row_payload
cargo bench -p lean-rs-worker --bench worker_capability

hot_paths covers lean_rs::module and lean_rs::abi: LeanExported::call and the String/Vec<String> round-trip decoders. session covers LeanSession::*: query_declarations_bulk, the three declaration_*_bulk 5k-vs-loop comparisons, elaborate_small, run_meta_whnf, and SessionPool hits.

row_payload covers the worker row transport hot path: JSON tree rows versus validated raw-JSON rows, typed command decode, row throughput, and allocation pressure. Two guards live alongside it: worker::row_payload::protocol_batching compares per-row raw JSON frames with batched raw JSON frames so any future batch protocol must justify itself against the current per-row baseline. worker::row_payload::data_plane compares JSON, raw JSON, simulated binary envelopes, MessagePack, and CBOR so any future format change must show a measured win. worker_capability covers the downstream-shaped worker fixture: cold startup, first import, import-once streaming, cancellation latency, fatal-exit recovery, worker cycling, row throughput, and memory growth.

Progress changes must benchmark the no-progress path explicitly. The retained fast path for bulk introspection is:

cargo bench -p lean-rs-host --bench session -- \
  host::session::declaration_kind_bulk_vs_loop/bulk_5000 --save-baseline before
# ... make progress changes ...
cargo bench -p lean-rs-host --bench session -- \
  host::session::declaration_kind_bulk_vs_loop/bulk_5000 --baseline before

progress = None should stay within Criterion noise because it allocates no callback handle and dispatches the same bulk shim as before.

Worker row-performance changes must benchmark the worker row path explicitly:

cargo bench -p lean-rs-worker --bench row_payload -- --save-baseline before
# ... make row transport changes ...
cargo bench -p lean-rs-worker --bench row_payload -- --baseline before

Do not add public worker batch sinks or private row-batch protocol frames from a microbenchmark alone. The protocol_batching and typed_many_512 measurements showed no improvement over per-row delivery on the real worker path; row delivery stays per-row. See docs/architecture/22-worker-row-batching.md. Do not replace the worker data-plane format from a microbenchmark alone either. Small- and large-row format candidates were measured; the raw-JSON typed decode path stays until an end-to-end worker workload justifies a replacement. See docs/architecture/23-worker-data-plane-format.md.

The Lean-side worker envelope helper fixture runs through the typed command path:

cargo test -p lean-rs-worker --test typed_command helper_ -- --nocapture

The focused chunked-stream test prints the named helper workload as helper_chunked_stream rows=<n> chunks=<n> chunk_size=<n> parallelism=1 elapsed_ms=<n>. Keep parallelism=1; Rust worker pools are the supported parallelism boundary. A safe Lean-side parallel chunk emitter would have to be proved out before raising this.

Capability-layer changes should also run the downstream-shaped scenario bench:

cargo bench -p lean-rs-worker --bench worker_capability -- --sample-size 10

Record parent/child RSS alongside throughput with:

cargo run --release -p lean-rs-worker --example worker_capability_probe
cargo run --release -p lean-rs-worker --example row_perf_probe

The mathlib-scale fixture runs through the planner, pool, session lease, and typed command path:

cargo build -p lean-rs-worker --bin lean-rs-worker-child
cargo run -p lean-rs-worker --example mathlib_scale_probe
cargo bench -p lean-rs-worker --bench worker_capability -- mathlib_scale

Set LEAN_RS_MATHLIB_ROOT=/path/to/mathlib4 and LEAN_RS_MATHLIB_SCALE_LIMIT=<n> to use a real mathlib module list as the planning workload. The fixture emits deterministic generic rows, so only claim mathlib-scale behavior for the parts actually measured: planning, pool leases, session reuse, row throughput, cancellation, fatal-exit recovery, worker cycling, and RSS sampling availability.

The same probe records pool snapshots and bounded row-delivery backpressure. The single_worker, pool_max_2, and post_cycle lines print active workers, warm leases, queue depth, stream request outcomes, delivered rows, payload bytes, stream elapsed time, and backpressure counters. The slow_sink line runs a deliberately slow row sink and records parent RSS before/after, child RSS, delivered row count, payload bytes, and backpressure waits/failures:

cargo build -p lean-rs-worker --bin lean-rs-worker-child
cargo run -p lean-rs-worker --example mathlib_scale_probe

Rows are not dropped under backpressure. A delivered row is still tentative until terminal success. Use the snapshot counters as operating evidence and terminal summaries as committed row counts.

The lean-dup-class readiness fixture exercises the full path end to end:

cargo run -p lean-rs-worker --example lean_dup_readiness

It drives the planner, pool, session lease, and typed command facade for generic version, doctor, extract, features, index, and probe command shapes, and records row throughput, diagnostics, progress, terminal summaries, timeout/cancellation/fatal-exit recovery, explicit cycling, backpressure, pool stats, parent/child RSS when available, and optional subprocess comparison status. Treat its rows as generic fixture data, not downstream schemas.

The supported scale path is planner → pool → session lease → typed command → live rows → terminal summary → pool stats. Any throughput change must report a named workload, row counts, throughput, allocation or payload-size evidence where relevant, and parent/child RSS (or explicit RSS-unavailable status). The standing scale contract is docs/architecture/28-production-scale-release.md.

Sample capture (macOS, Lean 4.29.1, declaration_kind_bulk_vs_loop/bulk_5000): baseline 100.0 µs vs. comparison 101.1 µs; Criterion reports no change. Re-capture on the same hardware before declaring a regression.

The cold-path probes (runtime_init, library_open, module_initialize) are not Criterion benches because they only fire once per process. Run them via:

cargo build --release -p lean-rs --example cold_probe
for i in $(seq 1 25); do ./target/release/examples/cold_probe; done

Output is one name=<workload> elapsed_us=<u64> line per stage.

Long-session RSS reproducer

long_session_memory is the retained-memory counterpart to the latency benches. It runs one long-lived process through fresh imports, pooled reuse, bulk introspection, and elaboration, printing RSS checkpoints and SessionPool counters:

LEAN_RS_NUM_THREADS=1 cargo run --release -p lean-rs-host --example long_session_memory

This is deliberately not a Criterion bench. Criterion answers per-iteration latency questions; this workload answers whether RSS returns at lifetime boundaries after LeanSession, SessionPool, and Obj<'lean> drops. See docs/safety/long-session-memory.md for the measured LEAN_RESOLVED_VERSION result and consumer guidance.

Detect a regression

Save a baseline before any change you suspect of moving the numbers:

cargo bench -p lean-rs-host --bench session -- --save-baseline before
# ... make changes ...
cargo bench -p lean-rs-host --bench session -- --baseline before

Criterion’s report calls out per-workload deltas with confidence intervals. Treat any change outside the 95% CI on a workload that exercises the changed code path as load-bearing; treat uniform shifts across unrelated workloads as CPU-state noise between captures.

Allocation snapshots

dhat output for the conversion-heavy workloads, when an allocation question needs an answer:

# Run from the workspace root.
WORKSPACE=$(pwd)
cargo build --release -p lean-rs --example alloc_probe
mkdir -p /tmp/dhat-runs && cd /tmp/dhat-runs
"$WORKSPACE/target/release/examples/alloc_probe" string_identity_4096
# dhat-heap.json carries per-call-site backtraces; inspect with
# https://nnethercote.github.io/dh_view/dh_view.html

dhat sees Rust allocations only. Lean’s internal mimalloc is statically linked into libleanrt.a and is invisible to #[global_allocator]; allocation numbers capture ABI conversions, Vec/String buffers, and error-message bounding on the host stack, not the Lean kernel heap.

Diagnostics and Observability

lean-rs and lean-rs-host project errors to the same stable [lean_rs::LeanDiagnosticCode] taxonomy and emit structured tracing spans against the lean_rs target. Long-running host session operations can also report live progress through lean_rs_host::LeanProgressSink; see architecture/13-structured-progress.md. lean-rs-worker uses its own LeanWorkerError surface for process-boundary outcomes such as child exit, request timeout, cancellation, data-sink panic, diagnostic-sink panic, and typed command decode failures. A downstream caller gets:

• a stable identifier (err.code()) to react by family, independent of internal stage tags that may grow new variants;
• visibility into where time is spent and where failures originate, without rebuilding the crates.

The taxonomy is unified across lean-rs and lean-rs-host (every recoverable failure on either side maps to a stable code); the span catalogue is split by emitting crate so the layer boundary is visible at the log line. Lean internal panics are outside this error taxonomy: there is no SessionPoisoned code. A Lean runtime panic during a LeanSession call may terminate the process; see architecture/06-panic-containment.md. When the same failure happens inside lean-rs-worker, the parent observes a typed worker exit instead of an in-process LeanDiagnosticCode.

Diagnostic codes

The enum is #[non_exhaustive]; new variants may be added. Variant names and as_str() ids are stable across patch releases.

Loader preflight

Manifest-backed shipped capabilities can be checked before LeanCapability opens any dylib:

#![allow(unused)]
fn main() {
let report = lean_rs::LeanCapabilityPreflight::new(
    lean_rs::LeanBuiltCapability::manifest_path(env!("LEAN_RS_CAPABILITY_MY_CAPABILITY_MANIFEST")),
)
.check();

if let Some(check) = report.first_error() {
    eprintln!("{}: {}", check.code(), check.repair_hint());
}
}

LeanCapability::from_build_manifest runs the same preflight internally when that produces a clearer failure. The broad LeanError still reports LeanDiagnosticCode::ModuleInit, but the bounded message includes the stable loader code and repair hint.

Normal users should not repair shipped apps by setting LD_LIBRARY_PATH or DYLD_*. A missing search path in the canonical flow is a packaging or artifact-manifest problem, not a caller-managed loader-flag problem.

Worker bootstrap checks

Packaged worker applications can check deployment state before running a real command:

#![allow(unused)]
fn main() {
let report = builder.check();
if let Some(check) = report.first_error() {
    eprintln!("{}: {}", check.code(), check.repair_hint());
}
}

LeanWorkerCapabilityBuilder::check() validates the app-owned worker child, manifest-backed capability artifact, protocol handshake, import session, and optional metadata expectation. It returns LeanWorkerBootstrapReport, not raw child pids, pipe handles, protocol frames, loader flags, or std::process configuration.

Internal covers Rust callback panics caught before they unwind across C or Lean. It does not mean a Lean kernel/runtime panic was contained. Those failures require a worker-process boundary.

L1 callback shims also return LeanCallbackStatus for callback-local outcomes. Ok = 0 continues the Lean-side callback loop; StaleHandle = 1 means Lean called a dropped handle; Panic = 2 means Rust contained a callback panic and recorded LeanError::Host on the live handle; WrongPayload = 3 means Lean used a handle with the wrong payload trampoline; and Stopped = 4 means the Rust callback asked Lean to stop cleanly.

lean-toolchain uses a separate LinkDiagnostics enum for build-script work. Those diagnostics cover Lean discovery, unsupported toolchains, missing lake, missing Lake targets, Lake build failures, and unresolved Lake outputs. They render as one line so a build.rs can either return them or print them through cargo:warning=.

Cancelled is cooperative. It is returned only when lean-rs-host regains control and checks the token; it does not pre-empt an in-flight Lean call. See architecture/07-cooperative-cancellation.md.

Progress sink panics are caught at the Rust callback boundary and surfaced as LeanError::Host with stage CallbackPanic, code lean_rs.internal.

Worker process diagnostics and pool snapshots

lean-rs-worker deliberately uses a separate worker error surface for process boundary failures. Child panic/abort, request timeout, cancellation-triggered cycle, stale lease use, row sink panic, diagnostic sink panic, and typed command decode failure are worker outcomes, not LeanDiagnosticCode values from the in-process host stack.

For large local runs, use LeanWorkerPoolSnapshot and LeanWorkerSessionLease::snapshot() for operational state. Snapshots summarize queue depth, active workers, warm leases, restart reasons, best-effort child RSS, stream outcomes, delivered row counts, payload bytes, elapsed stream time, and backpressure counters. They intentionally do not expose child pids, worker ids, pipe handles, protocol frames, or scheduling internals.

Matching on codes

LeanError, LeanElabFailure, and LeanMetaResponse all project to the same taxonomy via .code():

#![allow(unused)]
fn main() {
use lean_rs::{LeanDiagnosticCode, LeanError};

fn report(err: &LeanError) {
    match err.code() {
        LeanDiagnosticCode::Linking => eprintln!("rebuild the capability: {err}"),
        LeanDiagnosticCode::ModuleInit => eprintln!("check `lake build` produced the dylib: {err}"),
        LeanDiagnosticCode::LeanException => {
            if let LeanError::LeanException(exc) = err {
                eprintln!("Lean raised {:?}: {}", exc.kind(), exc.message());
            }
        }
        LeanDiagnosticCode::Cancelled => eprintln!("caller cancelled the operation"),
        other => eprintln!("unhandled {other}: {err}"),
    }
}
}

LeanMetaResponse::code() returns an Option: None on Ok, Some(Unsupported) when the capability lacked the requested service, and Some(Elaboration) on the other two failure shapes (which carry a LeanElabFailure). LeanElabFailure::code() always returns Elaboration.

Tracing

lean-rs and lean-rs-host declare spans against the lean_rs target. Neither installs a subscriber—pick one downstream, or use DiagnosticCapture for tests.

Recommended RUST_LOG scopes:

info covers init, library open, and session import (once-per-cycle events). debug adds per-session-method dispatch (query_declaration, elaborate, kernel_check, bulk methods, pool acquire/release). trace adds per-dispatch (LeanExported::call) and per-decoder events.

A typical tracing-subscriber wire-up:

#![allow(unused)]
fn main() {
tracing_subscriber::fmt()
    .with_env_filter(
        tracing_subscriber::EnvFilter::try_from_default_env()
            .unwrap_or_else(|_| tracing_subscriber::EnvFilter::new("lean_rs=info")),
    )
    .init();
}

Spans emitted by lean-rs (L1)

FFI-primitive spans: init, library open, module initializer, typed-export dispatch, ABI decode. Fire whether the caller is lean-rs-host or any other downstream of lean-rs.

Spans emitted by lean-rs-host (L2)

Host-stack session and pool spans. Fire only if the caller opted into the L2 stack and is driving a session.

Capturing diagnostics in tests

DiagnosticCapture is an in-process buffer for spans and events emitted against the lean_rs target. Thread-local and bounded; the guard restores the previous subscriber on Drop.

#![allow(unused)]
fn main() {
use lean_rs::{DiagnosticCapture, LeanDiagnosticCode, LeanRuntime};
use lean_rs_host::LeanHost;

#[test]
fn rebuild_advice_fires_on_missing_dylib() {
    let capture = DiagnosticCapture::install();

    let runtime = LeanRuntime::init().unwrap();
    let host = LeanHost::from_lake_project(runtime, "/path/to/lake").unwrap();
    let err = host
        .load_capabilities("my_pkg", "DefinitelyMissingLib")
        .expect_err("missing dylib must fail");

    assert_eq!(err.code(), LeanDiagnosticCode::ModuleInit);

    let events = capture.events();
    assert!(events.iter().any(|e| e.span.as_deref()
        == Some("lean_rs.module.library.open")));
}
}

The guard is !Send + !Sync: it pins to the installing thread. Default capacity is 256 events; over-capacity drops the oldest entry and bumps capture.overflowed(). Use DiagnosticCapture::with_capacity(N) for larger budgets. Scope is just lean_rs; events from other crates pass through untouched.

Redaction and bounding

Two values can grow without bound: Lean-authored text (capability messages, diagnostic messages) and filesystem paths. Both are bounded at the construction site:

• Lean-authored strings pass through bound_message (the same 4 KiB cap that protects LeanError::message). Enforced on the UTF-8 char boundary, so multibyte sequences are never split.
• Filesystem paths emitted as span fields are shortened to the basename plus up to two parent components (build/lib/lib.dylib). The full absolute path is only emitted at trace level by call sites that explicitly need it.

Paths are not treated as secrets; shortening is a bounding decision, not a redaction decision. If a downstream policy requires full path suppression, install a tracing-subscriber filter that drops the relevant fields.

Cross-references

• lean_rs::LeanDiagnosticCode—the enum; defined on L1, lean-rs and lean-rs-host project to it.
• lean_rs::DiagnosticCapture—the in-process capture; captures spans from lean-rs and lean-rs-host against the shared lean_rs target.
• Host stack surface—methods on LeanSession and SessionPool that emit the L2 spans above.
• Concurrency contract—why spans are per-thread.
• Safety model—why messages are bounded at construction.
• Panic containment—why Lean internal panics are process-scoped.
• Cooperative cancellation—where cancellation tokens are checked and what they cannot interrupt.
• Callback registry—how L1 callback statuses relate to the error taxonomy.
• Interop build and link—typed lean-toolchain build diagnostics and cache behavior.
• Structured progress—live in-process progress events for long-running host calls.

Release Checklist

The lean-rs workspace publishes via .github/workflows/release.yml. Pushing a v<semver> git tag fires the workflow, which runs the pre-flight gate set, the public-API diff, workspace package creation, the five-crate live publish in dependency order, and opens a GitHub Release whose body is the matching ## [<version>] section of CHANGELOG.md.

This document is the human checklist for the steps before the tag push. The steps after the tag push are owned by the workflow.

Supported Lean window for v0.1.x: 4.26.0 through 4.29.1 plus the 4.30.0-rc2 release candidate. Adding the next release follows the bump procedure; re-confirm against the version matrix and crates/lean-rs-sys/src/supported.rs before any release.

Crate publish order is load-bearing: lean-rs-sys → lean-toolchain → lean-rs → lean-rs-host → lean-rs-worker. cargo publish enforces the dependency direction via the crates.io index—downstream publishes fail with “no matching package” until upstream is indexed. The workflow sleeps 90s between each publish step.

One-time setup

1. Create a scoped publish token on crates.io with publish-new, publish-update, and yank scopes. Token format: cio….
2. Add the token in the GitHub repo settings (Settings → Secrets and variables → Actions) as CARGO_REGISTRY_TOKEN.
3. If you sign git tags (recommended), set up your GPG / SSH signing key in your local git config—the workflow doesn’t verify signatures, but a signed tag is the audit trail the GitHub Release UI surfaces.

Step 1—Pre-flight (local)

The gates the release workflow will run; running them locally is the fast feedback loop.

cargo fmt --check
cargo clippy --all-targets -- -D warnings
cargo nextest run --workspace --profile ci
cargo test --doc --workspace
cargo test -p lean-rs-worker --test loader_regressions -- --nocapture --test-threads=1
RUSTDOCFLAGS="-D warnings" cargo doc --no-deps --workspace
DOCS_RS=1 RUSTDOCFLAGS="-D warnings" cargo doc --no-deps --workspace
python3 scripts/check_package_docsrs.py
cargo package --workspace --no-verify
actionlint .github/workflows/ci.yml .github/workflows/release.yml .github/workflows/sanitizer.yml

Stop on any failure. cargo test (single-process) is not the gate—see docs/testing.md.

Step 2—CHANGELOG + version bump

1. Move ## [Unreleased] entries into a new ## [X.Y.Z] section (or compose fresh). The workflow extracts the section body whose heading matches the pushed tag—heading text must match exactly (e.g., ## [0.1.1] for tag v0.1.1).

2. Bump [workspace.package].version and [workspace.dependencies] in the root Cargo.toml if they don’t already match. The workflow asserts "v${workspace.package.version}" == "${GITHUB_REF_NAME}" before any publish.

3. If the public API changed intentionally, regenerate the baselines in the same commit:

   for c in lean-rs-sys lean-toolchain lean-rs lean-rs-host lean-rs-worker; do
     cargo public-api -p "$c" --simplified > "docs/api-review/${c}-public.txt"
   done
   

   The workflow re-runs cargo public-api --simplified for each crate and diffs against these baselines. Drift fails the workflow before any publish.

Step 3—PR and merge

Open a PR with CHANGELOG + version + (if needed) baseline changes. Merge after CI is green on the existing ci.yml matrix. The release workflow does not run until the tag is pushed; the regular CI run on the PR is the final correctness gate.

Step 4—(Optional) Workflow dry-run

Before tagging, manually trigger the release workflow with dry_run: true from the Actions UI (Actions → Release → “Run workflow” → check dry_run). Runs every gate including workspace package creation and the public-API diff but skips the live publish and the GitHub Release. Useful when CHANGELOG section extraction or the public-API diff needs a sanity check that doesn’t show up in the regular CI run.

The workflow intentionally does not run cargo publish --workspace --dry-run before the live publish. Cargo verifies each downstream package against the crates.io index, so a new interdependent workspace version fails dry-run until the upstream crates have actually been published and indexed. The live workflow publishes in dependency order and sleeps between crates so each later cargo publish performs the real verification against the just-published upstream version.

Step 5—Cut the tag

Only after the merge commit is on main:

git tag -s v0.1.2 -m "lean-rs v0.1.2"
git push origin v0.1.2

-s for a signed tag (recommended) or -a for unsigned annotated. The tag fires the workflow.

Step 6—Watch the workflow

gh run watch --workflow=release.yml

The workflow:

1. Installs elan + Lean (head of the supported window).
2. Asserts the tag matches the workspace version.
3. Runs fmt, clippy, nextest, doctests, doc build.
4. Runs the docs.rs-compatible doc build with DOCS_RS=1.
5. Runs the public-API diff against the committed baselines.
6. Runs python3 scripts/check_package_docsrs.py, which packages the workspace, checks crate/template package contents, unpacks the normalized tarballs, hides Lean/elan/lake from PATH, and builds docs with DOCS_RS=1.
7. Runs cargo package --workspace --no-verify to create the package tarballs.
8. Publishes the five crates in order with 90s sleeps between steps.
9. Extracts the matching ## [<version>] section from CHANGELOG.md.
10. Creates a GitHub Release with that body. Tags containing - (e.g. v0.1.0-rc.1) are marked prerelease automatically.

If the workflow fails after one crate has published, crates.io versions are immutable—do not retry with the same version. Bump the failed crate’s patch version, repeat steps 1–3, and re-tag at the new merge commit. The tag-vs-version assertion prevents re-tagging against the wrong workspace version.

Step 7—Post-publish

• Verify the release on crates.io: cargo search lean-rs (all five crates should appear with the new version).
• Verify docs.rs built each crate cleanly: visit https://docs.rs/lean-rs/<version> (and the same for the other four) within ~10 minutes. A docs.rs failure is recoverable only by a patch publish with the doc fix.
• Open PRs against the downstream proof repos (lean-rs-downstream, lean-rs-host-downstream) to bump crate dependencies. Shim sources are bundled with lean-rs and lean-rs-host, so downstream Lake files should not pin a separate shim tag.
• Add a fresh ## [Unreleased] heading at the top of CHANGELOG.md.

Fallback—local publish when CI is unavailable

Use only when CI is genuinely blocked (account suspension, runner outage, secret loss).

version=$(cargo metadata --no-deps --format-version 1 \
  | python3 -c 'import json,sys; m=json.load(sys.stdin); print(next(p["version"] for p in m["packages"] if p["name"]=="lean-rs"))')

cargo publish -p lean-rs-sys
sleep 90 && cargo publish -p lean-toolchain
sleep 90 && cargo publish -p lean-rs
sleep 90 && cargo publish -p lean-rs-host
sleep 90 && cargo publish -p lean-rs-worker

git tag -s "v${version}" -m "lean-rs v${version}"
git push origin "v${version}"
gh release create "v${version}" \
  --notes-file <(awk -v ver="$version" '$0 ~ "^## \\[" ver "\\]" {f=1;next} f&&/^## \\[/{exit} f' CHANGELOG.md)

Prerequisite: cargo login once with the same scoped publish token.

If any cargo publish fails—stop. Do not re-run with --allow-dirty or attempt to overwrite the published version. crates.io versions are immutable; a failed publish that uploaded but failed to index requires bumping the patch version. cargo publish --dry-run doesn’t need credentials and is safe to run anytime.

Adding a Lean release to the supported window

Adding a version requires two verifications: the lean.h layout is unchanged from an existing entry, and every symbol in REQUIRED_SYMBOLS still resolves in the new libleanshared. The single source of truth is crates/lean-rs-sys/src/supported.rs; the steps below either update that file or follow from it. Budget ~30 minutes plus CI time. End state: the workspace builds and tests cleanly against the new release on every CI cell.

Steps

1. Install the toolchain

elan toolchain install leanprover/lean4:vX.Y.Z

~500 MB. Skip if already installed.

2. Capture the lean.h SHA-256

shasum -a 256 \
  ~/.elan/toolchains/leanprover--lean4---vX.Y.Z/include/lean/lean.h | cut -d' ' -f1

Compare against existing entries in SUPPORTED_TOOLCHAINS:

• Digest matches an existing entry → append "X.Y.Z" to that entry’s versions array, then jump to step 4. The common case; Lean often ships point releases without touching lean.h.
• New digest → run step 3 first.

3. (New digest only) Verify layout + symbols

Two checks. Both must pass; either failure means do not silently add the entry.

Layout check. The 10 #[repr(C)] struct definitions in lean-rs-sys/src/repr.rs must be byte-identical to the new header’s relevant block:

scripts/check-lean-header.sh <existing-version> X.Y.Z

Empty output: layouts unchanged, safe to add. Non-empty: stop and revisit 02-versioning-and-compatibility.md.

Symbol check. Every REQUIRED_SYMBOLS entry must resolve:

scripts/check-lean-symbols.sh X.Y.Z

Empty output: every required symbol resolves. Non-empty: a symbol disappeared upstream. Either add it to the entry’s missing_symbols list (and update consumer call sites to tolerate absence), or file an upstream issue and stop.

4. Update the SUPPORTED_TOOLCHAINS table

Edit crates/lean-rs-sys/src/supported.rs:

• Add a new SupportedToolchain { versions: &["X.Y.Z"], header_digest: "<digest>", missing_symbols: &[] } entry in version order, or append "X.Y.Z" to an existing entry’s versions array when the digest matched.
• Mirror the entry in crates/lean-rs-sys/digests/manifest.json and docs/version-matrix.md.

5. Update the CI matrix

Edit .github/workflows/ci.yml: add "X.Y.Z" to matrix.lean_version. If X.Y.Z is the new highest version, also update the head version in .github/workflows/sanitizer.yml.

6. Run the local sweep

scripts/test-all-toolchains.sh

Iterates every version in digests/manifest.json, repoints the workspace lean-toolchain files (root + bundled shim packages under crates/lean-rs/shims/ and crates/lean-rs-host/shims/ + fixtures/lean + fixtures/interop-shims), rebuilds the Lake packages, runs cargo nextest run --workspace, and prints a per-version pass/fail summary. Restores the original lean-toolchain files on exit (even on failure).

7. Commit and PR

Commit message: Add Lean X.Y.Z to the supported toolchain window. PR description includes:

• The new digest (and whether it matched an existing entry).
• The step 6 summary.
• Any missing_symbols updates and why.

When the bump fails

A test failure on the new version does not justify pinning around it with brittle wrappers or version-specific allowlists. The right resolution depends on what broke:

Version Matrix

Tested configurations for the five published lean-rs crates. Configurations outside these tables are unsupported, even if they happen to compile.

• Policy: docs/architecture/02-versioning-and-compatibility.md
• Release procedure: docs/release.md
• Bump procedure: docs/bump-toolchain.md

Lean toolchain window

Supported window: Lean 4.26.0–4.29.1 plus the 4.30.0-rc2 release candidate (seven entries). Authoritative list, including lean.h SHA-256 digests, lives in crates/lean-rs-sys/src/supported.rs. Releases that ship a byte-identical lean.h share one entry. CI verifies every row × {ubuntu-latest, macos-latest} cell. The header is platform-independent; digests are identical across the two target triples.

Extending the window is the bump procedure. Untested versions are not supported.

The bundled Lake packages under crates/lean-rs/shims/ and crates/lean-rs-host/shims/, plus fixtures/lean and fixtures/interop-shims, use the same toolchain window. lean-rs-worker uses the same window because its child process loads the host stack and fixture/capability dylibs built against that toolchain. The reusable interop release contract is documented in docs/architecture/14-interop-release-contract.md.

lean-rs-sys symbol coverage

pub const REQUIRED_SYMBOLS in crates/lean-rs-sys/src/lib.rs enumerates the 87 LEAN_EXPORT’d symbols the crate’s extern "C" blocks declare. tests/linkage.rs resolves every entry against libleanshared at link time on every version × OS cell; the parallel test in lean-toolchain imports the same set via lean_rs_sys::REQUIRED_SYMBOLS. All 87 symbols are present in every release in the window (SupportedToolchain::missing_symbols is empty for every entry).

Rust

The MSRV is the floor a downstream consumer can rely on; the CI release matrix runs on the current stable.

Platforms

Explicitly unsupported (do not file as bugs without a compatibility-decision proposal):

• Windows (any toolchain). Adding requires a CI cell and a compatibility-decision proposal against docs/architecture/02-versioning-and-compatibility.md.
• BSDs, embedded targets, WASM.

See also

For how to run the benchmarks and detect regressions, see docs/performance.md. For the frozen public API of each crate, see docs/api-review/.

Public-API Review

docs/api-review/*-public.txt are cargo public-api --simplified baselines for the five published crates. CI diffs the live surface against these files on every PR; intentional changes regenerate the matching baseline in the same commit.

Regenerate

for c in lean-rs-sys lean-toolchain lean-rs lean-rs-host lean-rs-worker; do
  cargo public-api -p "$c" --simplified > "docs/api-review/${c}-public.txt"
done

Red-flag checklist (review before regenerating)

Walk the diff with these questions. Any “yes” is a stop-and-discuss signal, not necessarily a block.

1. Shallow module. Does a new module own enough state and behaviour to be its own concept, or is it a file-per-symbol split?
2. Pass-through wrapper. Does a new wrapper type add real transformation, or just rename an existing one?
3. Temporal decomposition. Do new error variants model lifecycle stages of one concern (Ousterhout ch. 5.3), instead of independent failure classes?
4. Information leakage. Does per-call C ABI shape (unboxed vs boxed, IO-wrap vs pure) leak into the caller’s types?
5. Special-general mixture. Are optional or specialised items being mixed into the crate root alongside mandatory ones?
6. Conjoined methods. Does a single method bundle two operations callers should be able to pay for independently?
7. Hard-to-describe API. Can a new reader reduce the surface to one sentence and a five-line snippet?
8. Implementation details in comments. rg -nE "(land(s|ed|ing)|follow(s|ed)|scheduled).*\b(prompt|RD-[0-9])" crates/ should return no matches.

Doc rules

Each pub item carries:

• # Errors on every fallible function returning LeanResult, naming failure modes.
• # Safety on every pub unsafe fn in lean-rs-sys, naming the precondition. No placeholder patterns (“see lean.h”, “uphold all Lean invariants”).
• Doc links: bare [`Type`] for crate-root items; crate::-qualified for sub-modules.

RUSTDOCFLAGS="-D warnings" cargo doc --no-deps --workspace --document-private-items must be clean.

Verification

cargo fmt --check
cargo clippy --all-targets -- -D warnings
cargo test
RUSTDOCFLAGS="-D warnings" cargo doc --no-deps --workspace --document-private-items
test -f docs/api-review/lean-rs-sys-public.txt
test -f docs/api-review/lean-toolchain-public.txt
test -f docs/api-review/lean-rs-public.txt
test -f docs/api-review/lean-rs-host-public.txt
test -f docs/api-review/lean-rs-worker-public.txt