Crate lean_rs_host 

Standard Lean service layer for Rust applications embedding Lean 4.

This crate is the standard service layer built on top of the typed FFI crate 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 + 9 optional lean_rs_host_* @[export] Lean shims bundled with this crate and loaded alongside the consumer capability dylib.

Downstream applications that only need to call @[export] Lean functions with typed arguments and no shim contract should depend on lean-rs directly and skip this crate.

Re-exports

pub use crate::host::meta;

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.

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.