lean_rs_host/
lib.rs

1//! Opinionated Rust host stack for embedding Lean 4 as a theorem-prover
2//! capability.
3//!
4//! This crate is the L2 application framework built on top of the L1
5//! FFI primitive shipped by [`lean-rs`](https://docs.rs/lean-rs). It owns:
6//!
7//! - The high-level [`LeanHost`] / [`LeanCapabilities`] / [`LeanSession`]
8//!   trio, plus the [`SessionPool`] / [`PooledSession`] reuse helper and
9//!   [`LeanProgressSink`] for live progress from long-running calls.
10//! - The host-defined evidence / kernel-outcome / elaboration / meta
11//!   value types: [`LeanEvidence`], [`LeanKernelOutcome`],
12//!   [`ProofSummary`], [`LeanElabOptions`], [`LeanElabFailure`], the
13//!   `meta::*` service surface.
14//! - The capability contract: 26 mandatory + 4 optional `lean_rs_host_*`
15//!   `@[export]` Lean shims bundled with this crate and loaded alongside the
16//!   consumer capability dylib.
17//!
18//! Downstream applications that want the (β)-binding minimum — call any
19//! `@[export]` Lean function with typed arguments, no shim contract —
20//! should depend on `lean-rs` directly and skip this crate.
21
22pub mod host;
23
24/// Bounded `MetaM` service surface. Reachable only at this sub-module
25/// path so callers opt in explicitly via
26/// `use lean_rs_host::meta::{...};`.
27pub mod meta {
28    pub use crate::host::meta::*;
29}
30
31pub use crate::host::elaboration::{
32    LEAN_DIAGNOSTIC_BYTE_LIMIT_DEFAULT, LEAN_DIAGNOSTIC_BYTE_LIMIT_MAX, LEAN_HEARTBEAT_LIMIT_DEFAULT,
33    LEAN_HEARTBEAT_LIMIT_MAX, LeanDiagnostic, LeanElabFailure, LeanElabOptions, LeanPosition, LeanSeverity,
34};
35pub use crate::host::evidence::{
36    EvidenceStatus, LEAN_PROOF_SUMMARY_BYTE_LIMIT, LeanEvidence, LeanKernelOutcome, ProofSummary,
37};
38pub use crate::host::{LeanCancellationToken, LeanProgressEvent, LeanProgressSink};
39pub use crate::host::{
40    LeanCapabilities, LeanDeclarationFilter, LeanHost, LeanSession, LeanSourceRange, PoolStats, PooledSession,
41    SessionPool, SessionStats,
42};
lean_rs_host/lib.rs

lean_rs_host/
lib.rs
