lean_rs_host/
lib.rs

1//! Standard Lean service layer for Rust applications embedding Lean 4.
2//!
3//! This crate is the standard service layer built on top of the typed FFI
4//! crate shipped by [`lean-rs`](https://docs.rs/lean-rs). It owns:
5//!
6//! - The high-level [`LeanHost`] / [`LeanCapabilities`] / [`LeanSession`]
7//!   trio, plus the [`SessionPool`] / [`PooledSession`] reuse helper and
8//!   [`LeanProgressSink`] for live progress from long-running calls.
9//! - The host-defined evidence / kernel-outcome / elaboration / meta
10//!   value types: [`LeanEvidence`], [`LeanKernelOutcome`],
11//!   [`ProofSummary`], [`LeanElabOptions`], [`LeanElabFailure`], the
12//!   `meta::*` service surface.
13//! - The capability contract: 28 mandatory + 9 optional `lean_rs_host_*`
14//!   `@[export]` Lean shims bundled with this crate and loaded alongside the
15//!   consumer capability dylib.
16//!
17//! Downstream applications that only need to call `@[export]` Lean functions
18//! with typed arguments and no shim contract
19//! should depend on `lean-rs` directly and skip this crate.
20
21#![forbid(unsafe_code)]
22
23pub mod host;
24
25/// Bounded `MetaM` service surface. Reachable only at this sub-module
26/// path so callers opt in explicitly via
27/// `use lean_rs_host::meta::{...};`.
28pub use crate::host::meta;
29
30pub use crate::host::elaboration::{
31    LEAN_DIAGNOSTIC_BYTE_LIMIT_DEFAULT, LEAN_DIAGNOSTIC_BYTE_LIMIT_MAX, LEAN_HEARTBEAT_LIMIT_DEFAULT,
32    LEAN_HEARTBEAT_LIMIT_MAX, LeanDiagnostic, LeanElabFailure, LeanElabOptions, LeanPosition, LeanSeverity,
33};
34pub use crate::host::evidence::{
35    EvidenceStatus, LEAN_PROOF_SUMMARY_BYTE_LIMIT, LeanEvidence, LeanKernelOutcome, ProofSummary,
36};
37pub use crate::host::{
38    DeclarationFlags, DeclarationInspection, DeclarationInspectionBudgets, DeclarationInspectionFields,
39    DeclarationInspectionRequest, DeclarationInspectionResult, DeclarationNameMatch, DeclarationProofSearchFacts,
40    DeclarationRenderedInfo, DeclarationSearchBias, DeclarationSearchFacts, DeclarationSearchPruning,
41    DeclarationSearchRequest, DeclarationSearchResult, DeclarationSearchRow, DeclarationSearchScope,
42    DeclarationSearchTimings, DeclarationVerificationFacts, DeclarationVerificationOutcome,
43    DeclarationVerificationRequest, DeclarationVerificationStatus, DeclarationVerificationTarget, LeanCapabilities,
44    LeanDeclarationFilter, LeanHost, LeanSession, LeanSourceRange, PoolStats, PooledSession, ProofAttemptEnvelope,
45    ProofAttemptOutcome, ProofAttemptRequest, ProofAttemptRow, ProofAttemptStatus, ProofCandidate, ProofEditTarget,
46    ProofPositionSelector, ProofPositionSummary, SessionPool, SessionStats,
47};
48pub use crate::host::{LeanCancellationToken, LeanProgressEvent, LeanProgressSink};
lean_rs_host/lib.rs

lean_rs_host/
lib.rs
