lean-rs-host 0.1.0

Opinionated Rust host stack for embedding Lean 4 as a theorem-prover capability: typed sessions, kernel-check evidence handles, bounded MetaM services, batching, and session pooling. Built on top of the `lean-rs` FFI primitive.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53

//! Bounded `MetaM` / `CoreM` capability surface.
//!
//! Rust can invoke a **closed registry** of Lean-authored meta services
//! through [`crate::LeanSession::run_meta`]. Each service is a sealed
//! [`LeanMetaService`] descriptor pinning a name, the `.olean` modules
//! required in the session, and a typed `(Req, Resp)` shape. Three
//! services are pinned:
//!
//! - [`infer_type`] — runs `Meta.inferType` on a supplied `Expr`.
//! - [`whnf`] — runs `Meta.whnf` on a supplied `Expr` under the bundle's
//!   reducibility setting.
//! - [`heartbeat_burn`] — a diagnostic loop that consumes a heartbeat
//!   per step, exercising the heartbeat-exhaustion classification path.
//!
//! Rust cannot assemble arbitrary `MetaM` programs: the only services
//! that exist are the ones with a `LeanMetaService` constructor in this
//! crate and a matching `@[export]` symbol on the Lean side
//! (`lean_rs_host_meta_*`). New services require landing both pieces
//! together.
//!
//! ## Bounded options
//!
//! [`LeanMetaOptions`] mirrors [`crate::LeanElabOptions`]: saturating
//! setters for heartbeats and diagnostic byte budget plus a
//! MetaM-specific [`LeanMetaTransparency`] knob. The heartbeat and
//! diagnostic-byte ceilings reuse the existing
//! `LEAN_HEARTBEAT_LIMIT_*` / `LEAN_DIAGNOSTIC_BYTE_LIMIT_*` constants
//! re-exported at the crate root.
//!
//! ## Status classification
//!
//! Every call returns a [`LeanMetaResponse<Resp>`] tagged by
//! [`MetaCallStatus`]:
//!
//! | Status                | Source                                                        |
//! | --------------------- | ------------------------------------------------------------- |
//! | `Ok`                  | `MetaM` action returned a payload                               |
//! | `Failed`              | `MetaM` raised a non-heartbeat Lean exception                   |
//! | `TimeoutOrHeartbeat`  | `Exception.isMaxHeartbeat` matched on the caught exception    |
//! | `Unsupported`         | Lean shim classified the request out-of-domain, **or** the loaded capability does not export the service's symbol (the Rust dispatcher synthesises this branch from a missing cached address) |
//!
//! The outer [`lean_rs::LeanResult`] still carries true host-stack
//! failures (a Lean shim *itself* raising through `IO`, or a malformed
//! return value); the four-way classification lives in the inner
//! `LeanMetaResponse`.

mod options;
mod response;
mod service;

pub use self::options::{LeanMetaOptions, LeanMetaTransparency};
pub use self::response::{LeanMetaResponse, MetaCallStatus};
pub use self::service::{LeanMetaService, heartbeat_burn, infer_type, whnf};