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: 32 mandatory + 10 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::DeclarationFlags;

pub use crate::host::DeclarationInspection;

pub use crate::host::DeclarationInspectionBudgets;

pub use crate::host::DeclarationInspectionFields;

pub use crate::host::DeclarationInspectionRequest;

pub use crate::host::DeclarationInspectionResult;

pub use crate::host::DeclarationNameMatch;

pub use crate::host::DeclarationProofSearchFacts;

pub use crate::host::DeclarationRenderedInfo;

pub use crate::host::DeclarationSearchBias;

pub use crate::host::DeclarationSearchFacts;

pub use crate::host::DeclarationSearchPruning;

pub use crate::host::DeclarationSearchRequest;

pub use crate::host::DeclarationSearchResult;

pub use crate::host::DeclarationSearchRow;

pub use crate::host::DeclarationSearchScope;

pub use crate::host::DeclarationSearchTimings;

pub use crate::host::DeclarationVerificationBatchItem;

pub use crate::host::DeclarationVerificationBatchOutcome;

pub use crate::host::DeclarationVerificationBatchRequest;

pub use crate::host::DeclarationVerificationBatchRow;

pub use crate::host::DeclarationVerificationFacts;

pub use crate::host::DeclarationVerificationOutcome;

pub use crate::host::DeclarationVerificationRequest;

pub use crate::host::DeclarationVerificationStatus;

pub use crate::host::DeclarationVerificationTarget;

pub use crate::host::LeanBracketedDeclarationInfo;

pub use crate::host::LeanBracketedImportRequest;

pub use crate::host::LeanBracketedImportResult;

pub use crate::host::LeanBracketedRejectedOperation;

pub use crate::host::LeanCapabilities;

pub use crate::host::LeanDeclarationFilter;

pub use crate::host::LeanDerivedWorkFacts;

pub use crate::host::LeanHost;

pub use crate::host::LeanImportLevel;

pub use crate::host::LeanImportProfileMode;

pub use crate::host::LeanImportProfilerOptions;

pub use crate::host::LeanImportStats;

pub use crate::host::LeanSession;

pub use crate::host::LeanSessionImportProfile;

pub use crate::host::LeanSourceRange;

pub use crate::host::PoolStats;

pub use crate::host::PooledSession;

pub use crate::host::ProofAttemptEnvelope;

pub use crate::host::ProofAttemptOutcome;

pub use crate::host::ProofAttemptRequest;

pub use crate::host::ProofAttemptRow;

pub use crate::host::ProofAttemptStatus;

pub use crate::host::ProofCandidate;

pub use crate::host::ProofEditTarget;

pub use crate::host::ProofPositionSelector;

pub use crate::host::ProofPositionSummary;

pub use crate::host::SessionPool;

pub use crate::host::SessionPoolConfig;

pub use crate::host::SessionPoolKeyMissReason;

pub use crate::host::SessionPoolMemoryPolicy;

pub use crate::host::SessionStats;

pub use crate::host::LeanCancellationToken;

pub use crate::host::LeanProgressEvent;

pub use crate::host::LeanProgressSink;

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.