Crate lean_rs_host 

Opinionated Rust host stack for embedding Lean 4 as a theorem-prover capability.

This crate is the L2 application framework built on top of the L1 FFI primitive shipped by lean-rs. It owns:

• The high-level LeanHost / LeanCapabilities / LeanSession trio, plus the SessionPool / PooledSession reuse helper and LeanProgressSink for live progress from long-running calls.
• The host-defined evidence / kernel-outcome / elaboration / meta value types: LeanEvidence, LeanKernelOutcome, ProofSummary, LeanElabOptions, LeanElabFailure, the meta::* service surface.
• The capability contract: 28 mandatory + 6 optional lean_rs_host_* @[export] Lean shims bundled with this crate and loaded alongside the consumer capability dylib.

Downstream applications that want the (β)-binding minimum — call any @[export] Lean function with typed arguments, no shim contract — should depend on lean-rs directly and skip this crate.

Re-exports

pub use crate::host::elaboration::LeanDiagnostic;

pub use crate::host::elaboration::LeanElabFailure;

pub use crate::host::elaboration::LeanElabOptions;

pub use crate::host::elaboration::LeanPosition;

pub use crate::host::elaboration::LeanSeverity;

pub use crate::host::evidence::EvidenceStatus;

pub use crate::host::evidence::LEAN_PROOF_SUMMARY_BYTE_LIMIT;

pub use crate::host::evidence::LeanEvidence;

pub use crate::host::evidence::LeanKernelOutcome;

pub use crate::host::evidence::ProofSummary;

pub use crate::host::LeanCancellationToken;

pub use crate::host::LeanProgressEvent;

pub use crate::host::LeanProgressSink;

pub use crate::host::LeanCapabilities;

pub use crate::host::LeanDeclarationFilter;

pub use crate::host::LeanHost;

pub use crate::host::LeanSession;

pub use crate::host::LeanSourceRange;

pub use crate::host::PoolStats;

pub use crate::host::PooledSession;

pub use crate::host::SessionPool;

pub use crate::host::SessionStats;

Modules

host

High-level surface for hosting Lean capabilities.

meta

Bounded MetaM service surface. Reachable only at this sub-module path so callers opt in explicitly via use lean_rs_host::meta::{...};.

Constants

LEAN_DIAGNOSTIC_BYTE_LIMIT_DEFAULT

Default byte budget for the diagnostic collection returned per call (64 KiB ≈ 16 default-bounded messages).

LEAN_DIAGNOSTIC_BYTE_LIMIT_MAX

Upper bound on the diagnostic byte budget (1 MiB).

LEAN_HEARTBEAT_LIMIT_DEFAULT

Default heartbeat ceiling — matches Lean’s own maxHeartbeats default at 4.29.1 (Lean.Core.maxHeartbeats).

LEAN_HEARTBEAT_LIMIT_MAX

Upper bound on the heartbeat ceiling. 1000× the default; values above saturate at this ceiling so a runaway elaborator finishes in bounded real time on every supported host.