Crate lean_rs 

Safe Rust FFI primitive for embedding Lean 4 from a host application.

lean-rs is the L1 typed-FFI binding to the Lean 4 runtime — the minimum surface a Rust crate needs to drive a compiled Lean library: bring the runtime up, open a Lake-built capability bundle, initialise a module, and call typed @[export] functions with first-class type marshalling. The opinionated theorem-prover-host stack (LeanHost, LeanCapabilities, LeanSession, plus the evidence and meta surfaces) lives in the sibling lean-rs-host crate, with its own 26+4 lean_rs_host_* Lean shim contract. This crate ships only the generic interop shims used by L1 callbacks; it has no theorem-prover host shim contract.

Happy path (L1)

Bring the runtime up once, open the build-script produced capability, initialise the module, look up a typed export, and call it:

let runtime = lean_rs::LeanRuntime::init()?;
let capability = lean_rs::LeanCapability::from_build_manifest(
    runtime,
    lean_rs::LeanBuiltCapability::manifest_path(env!("MY_CAPABILITY_MANIFEST")),
)?;
let module  = capability.module()?;
let add     = module.exported::<(u64, u64), u64>("my_export_add")?;
let sum     = add.call(3, 4)?;

LeanRuntime::init is the single doorway. It brings Lean up (process-once, idempotent) and returns a 'static borrow that anchors the 'lean lifetime every later handle carries; use-before- init is structurally impossible.

Worker threads that did not start inside Lean must be attached for the duration of their Lean work via LeanThreadGuard::attach; see docs/architecture/04-concurrency.md for the contract.

Module map

• error — typed error boundary. LeanError is a three-variant #[non_exhaustive] enum (LeanException for Lean-thrown IO errors, Host for host-stack failures, Cancelled for cooperative host cancellation); payload structs (LeanException, HostFailure, LeanCancelled) have private fields so the bounded-message invariant is structural. Every error projects to a LeanDiagnosticCode via .code(). The in-process DiagnosticCapture RAII guard lets tests assert on tracing events without installing a global subscriber.
• module — load a Lake-built Lean capability and call typed exported functions. LeanCapability is the normal shipped-crate surface; LeanCapabilityPreflight reports package/loader problems before dlopen; LeanLibraryBundle anchors dependency dylibs; LeanLibrary is the advanced one-dylib RAII handle; LeanModule proves a module’s initializer succeeded; LeanExported is a single generic typed function handle whose .call impl is macro-stamped per arity 0..=12.
• handle — opaque, lifetime-bound receipts for the four core Lean semantic values (LeanName, LeanLevel, LeanExpr, LeanDeclaration). Construction and inspection happen Lean-side through LeanModule::exported against caller-authored shims.
• callback — RAII callback registrations for Lean-to-Rust calls. LeanCallbackHandle hides the registry id, payload decoder, and trampoline while still producing the two USize ABI values generic interop shims pass to Lean.
• runtime — process-wide LeanRuntime anchor, LeanThreadGuard attach RAII, and the lifetime-bound owned / borrowed object handles Obj / ObjRef.
• abi — sealed LeanAbi trait + per-Lean-type C-ABI representation impls. The trait is the bound on LeanExported’s argument and return types; the impls are crate-internal (sealing prevents downstream LeanAbi for MyType).

Layering

lean-rs-sys → lean-toolchain → lean-rs → lean-rs-host. The first two crates expose raw FFI and toolchain metadata; this crate is the L1 safe surface every (β)-binding consumer depends on. The opinionated theorem-prover-host stack lives in lean-rs-host. Embedders that genuinely need the raw lean_* symbols can depend on lean-rs-sys directly, accepting its full unsafe discipline.

Curation policy

Items at lean_rs::* are the curated semver surface. The crate root re-exports the typed-FFI primitive plus the four handle types and the L1 error model. Refactors that reshape internal modules are free as long as those re-exports stay stable. The public- surface baseline lives at docs/api-review/lean-rs-public.txt.

Re-exports

pub use crate::abi::traits::LeanAbi;

pub use crate::callback::LeanCallbackFlow;

pub use crate::callback::LeanCallbackHandle;

pub use crate::callback::LeanCallbackPayload;

pub use crate::callback::LeanCallbackStatus;

pub use crate::callback::LeanProgressTick;

pub use crate::callback::LeanStringEvent;

pub use crate::error::CapturedEvent;

pub use crate::error::DIAGNOSTIC_CAPTURE_DEFAULT_CAPACITY;

pub use crate::error::DiagnosticCapture;

pub use crate::error::HostFailure;

pub use crate::error::HostStage;

pub use crate::error::LEAN_ERROR_MESSAGE_LIMIT;

pub use crate::error::LeanCancelled;

pub use crate::error::LeanDiagnosticCode;

pub use crate::error::LeanError;

pub use crate::error::LeanException;

pub use crate::error::LeanExceptionKind;

pub use crate::error::LeanResult;

pub use crate::handle::LeanDeclaration;

pub use crate::handle::LeanExpr;

pub use crate::handle::LeanLevel;

pub use crate::handle::LeanName;

pub use crate::module::DecodeCallResult;

pub use crate::module::LeanArgs;

pub use crate::module::LeanBuiltCapability;

pub use crate::module::LeanCapability;

pub use crate::module::LeanCapabilityPreflight;

pub use crate::module::LeanExported;

pub use crate::module::LeanIo;

pub use crate::module::LeanLibrary;

pub use crate::module::LeanLibraryBundle;

pub use crate::module::LeanLibraryDependency;

pub use crate::module::LeanLoaderCheck;

pub use crate::module::LeanLoaderDiagnosticCode;

pub use crate::module::LeanLoaderReport;

pub use crate::module::LeanLoaderSeverity;

pub use crate::module::LeanModule;

pub use crate::module::LeanModuleInitializer;

pub use crate::runtime::obj::Obj;

pub use crate::runtime::obj::ObjRef;

pub use crate::runtime::LeanRuntime;

pub use crate::runtime::LeanThreadGuard;

Modules

abi

Typed first-order ABI conversions for lean-rs.

callback

Rust callback handles for Lean-to-Rust interop.

error

Typed error boundary for the safe lean-rs surface.

handle

Opaque, lifetime-bound handles for core Lean semantic values.

module

Loading and initializing compiled Lean modules.

runtime

Process-wide Lean runtime anchor.

Constants

VERSION

Version of the lean-rs crate, matching Cargo.toml.