lean_rs/
lib.rs

1//! Safe Rust FFI primitive for embedding Lean 4 from a host application.
2//!
3//! `lean-rs` is the L1 typed-FFI binding to the Lean 4 runtime — the
4//! minimum surface a Rust crate needs to drive a compiled Lean library:
5//! bring the runtime up, open a Lake-built capability bundle, initialise a
6//! module, and call typed `@[export]` functions with first-class type
7//! marshalling. The opinionated theorem-prover-host stack (`LeanHost`,
8//! `LeanCapabilities`, `LeanSession`, plus the evidence and meta
9//! surfaces) lives in the sibling
10//! [`lean-rs-host`](https://docs.rs/lean-rs-host) crate, with its own
11//! 26+4 `lean_rs_host_*` Lean shim contract. This crate ships only the generic
12//! interop shims used by L1 callbacks; it has no theorem-prover host shim
13//! contract.
14//!
15//! ## Happy path (L1)
16//!
17//! Bring the runtime up once, open the build-script produced capability,
18//! initialise the module, look up a typed export, and call it:
19//!
20//! ```ignore
21//! let runtime = lean_rs::LeanRuntime::init()?;
22//! let capability = lean_rs::LeanCapability::from_build_manifest(
23//!     runtime,
24//!     lean_rs::LeanBuiltCapability::manifest_path(env!("MY_CAPABILITY_MANIFEST")),
25//! )?;
26//! let module  = capability.module()?;
27//! let add     = module.exported::<(u64, u64), u64>("my_export_add")?;
28//! let sum     = add.call(3, 4)?;
29//! ```
30//!
31//! [`LeanRuntime::init`] is the single doorway. It brings Lean up
32//! (process-once, idempotent) and returns a `'static` borrow that
33//! anchors the `'lean` lifetime every later handle carries; use-before-
34//! init is structurally impossible.
35//!
36//! Worker threads that did not start inside Lean must be attached for
37//! the duration of their Lean work via [`LeanThreadGuard::attach`];
38//! see `docs/architecture/04-concurrency.md` for the contract.
39//!
40//! ## Module map
41//!
42//! - [`error`] — typed error boundary. [`LeanError`] is a three-variant
43//!   `#[non_exhaustive]` enum (`LeanException` for Lean-thrown `IO`
44//!   errors, `Host` for host-stack failures, `Cancelled` for cooperative
45//!   host cancellation); payload structs ([`LeanException`],
46//!   [`HostFailure`], [`LeanCancelled`]) have private fields so the
47//!   bounded-message invariant is structural. Every error projects to a
48//!   [`LeanDiagnosticCode`] via `.code()`. The in-process
49//!   [`DiagnosticCapture`] RAII guard lets tests assert on `tracing`
50//!   events without installing a global subscriber.
51//! - [`module`] — load a Lake-built Lean capability and call typed
52//!   exported functions. [`LeanCapability`] is the normal shipped-crate
53//!   surface; [`LeanCapabilityPreflight`] reports package/loader problems
54//!   before `dlopen`; [`LeanLibraryBundle`] anchors dependency dylibs;
55//!   [`LeanLibrary`] is the advanced one-dylib RAII handle; [`LeanModule`]
56//!   proves a module's initializer succeeded;
57//!   [`LeanExported`] is a single generic typed function handle whose
58//!   `.call` impl is macro-stamped per arity `0..=12`.
59//! - [`handle`] — opaque, lifetime-bound receipts for the four core
60//!   Lean semantic values ([`LeanName`], [`LeanLevel`], [`LeanExpr`],
61//!   [`LeanDeclaration`]). Construction and inspection happen Lean-side
62//!   through [`LeanModule::exported`] against caller-authored shims.
63//! - [`callback`] — RAII callback registrations for Lean-to-Rust calls.
64//!   [`LeanCallbackHandle`] hides the registry id, payload decoder, and
65//!   trampoline while still producing the two `USize` ABI values generic
66//!   interop shims pass to Lean.
67//! - [`runtime`] — process-wide [`LeanRuntime`] anchor,
68//!   [`LeanThreadGuard`] attach RAII, and the lifetime-bound owned /
69//!   borrowed object handles [`Obj`] / [`ObjRef`].
70//! - [`abi`] — sealed [`LeanAbi`] trait + per-Lean-type C-ABI
71//!   representation impls. The trait is the bound on
72//!   [`LeanExported`]'s argument and return types; the impls are
73//!   crate-internal (sealing prevents downstream `LeanAbi for MyType`).
74//!
75//! ## Layering
76//!
77//! `lean-rs-sys → lean-toolchain → lean-rs → lean-rs-host`. The first
78//! two crates expose raw FFI and toolchain metadata; this crate is the
79//! L1 safe surface every (β)-binding consumer depends on. The
80//! opinionated theorem-prover-host stack lives in `lean-rs-host`.
81//! Embedders that genuinely need the raw `lean_*` symbols can depend
82//! on `lean-rs-sys` directly, accepting its full `unsafe` discipline.
83//!
84//! ## Curation policy
85//!
86//! Items at `lean_rs::*` are the curated semver surface. The crate
87//! root re-exports the typed-FFI primitive plus the four handle types
88//! and the L1 error model. Refactors that reshape internal modules
89//! are free as long as those re-exports stay stable. The public-
90//! surface baseline lives at `docs/api-review/lean-rs-public.txt`.
91
92pub mod abi;
93pub mod callback;
94pub mod error;
95pub mod handle;
96pub mod module;
97pub mod runtime;
98
99/// **Internal extension point.** Not part of the public API; not covered
100/// by semver. Exists so the sibling `lean-rs-host` crate can construct
101/// `LeanError` values via the narrow constructor wrappers it
102/// uses without bypassing the structural bounding invariant: external
103/// callers cannot mint `LeanError` values with unbounded messages. The
104/// seam stays narrow on purpose:
105/// every extra re-export here is interface surface external readers
106/// might mistake for a stable API. Add a wrapper only when a real call
107/// site needs it.
108///
109/// External crates must not depend on anything under this path.
110#[doc(hidden)]
111pub mod __host_internals {
112    pub use crate::error::host_callback_panic;
113    pub use crate::error::host_cancelled;
114    pub use crate::error::host_internal;
115    pub use crate::error::host_module_init;
116}
117
118#[cfg(feature = "fuzzing")]
119pub mod fuzz_entry;
120
121pub use crate::abi::traits::LeanAbi;
122pub use crate::callback::{
123    LeanCallbackFlow, LeanCallbackHandle, LeanCallbackPayload, LeanCallbackStatus, LeanProgressTick, LeanStringEvent,
124};
125pub use crate::error::{
126    CapturedEvent, DIAGNOSTIC_CAPTURE_DEFAULT_CAPACITY, DiagnosticCapture, HostFailure, HostStage,
127    LEAN_ERROR_MESSAGE_LIMIT, LeanCancelled, LeanDiagnosticCode, LeanError, LeanException, LeanExceptionKind,
128    LeanResult,
129};
130pub use crate::handle::{LeanDeclaration, LeanExpr, LeanLevel, LeanName};
131pub use crate::module::{
132    DecodeCallResult, LeanArgs, LeanBuiltCapability, LeanCapability, LeanCapabilityPreflight, LeanExported, LeanIo,
133    LeanLibrary, LeanLibraryBundle, LeanLibraryDependency, LeanLoaderCheck, LeanLoaderDiagnosticCode, LeanLoaderReport,
134    LeanLoaderSeverity, LeanModule, LeanModuleInitializer,
135};
136pub use crate::runtime::obj::{Obj, ObjRef};
137pub use crate::runtime::{LeanRuntime, LeanThreadGuard};
138
139/// Version of the `lean-rs` crate, matching `Cargo.toml`.
140pub const VERSION: &str = env!("CARGO_PKG_VERSION");
141
142#[cfg(test)]
143mod tests {
144    use super::VERSION;
145
146    #[test]
147    fn version_constant_matches_package() {
148        assert_eq!(VERSION, env!("CARGO_PKG_VERSION"));
149    }
150}
lean_rs/lib.rs

lean_rs/
lib.rs
