Crate lean_rs 

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

lean-rs is the 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 standard Lean service layer (LeanHost, LeanCapabilities, LeanSession, plus the evidence and meta surfaces) lives in the sibling lean-rs-host crate, with its own 28+9 lean_rs_host_* Lean shim contract. This crate ships only the generic interop shims used by same-process callbacks; it has no theorem-prover host shim contract.

Happy Path

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 add = capability.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 enum (LeanException for Lean-thrown IO errors, Host for host 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; LeanCapability::exported is the safe checked lookup path; LeanModule::exported_unchecked is the explicit unsafe path for arbitrary exports; 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_unchecked 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 safe surface every direct typed-FFI consumer depends on. The standard Lean service layer lives in lean-rs-host, and worker process facades live in lean-rs-worker-*. 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 lean-rs 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::abi::traits::LeanCReprAbi;

pub use crate::callback::LeanCallbackFlow;

pub use crate::callback::LeanCallbackHandle;

pub use crate::callback::LeanCallbackPayload;

pub use crate::callback::LeanCallbackStatus;

pub use crate::callback::LeanProgressCallback;

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::LeanCapability;

pub use crate::module::LeanCapabilityPreflight;

pub use crate::module::LeanCheckedExportError;

pub use crate::module::LeanExported;

pub use crate::module::LeanIo;

pub use crate::module::LeanLibrary;

pub use crate::module::LeanLibraryBundle;

pub use crate::module::LeanModule;

pub use crate::module::LeanRuntimePreflight;

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.

Structs

LeanBuiltCapability

Runtime descriptor for a Lean capability built by a downstream build.rs.

LeanExportArgAbi

ABI shape of one exported function argument.

LeanExportReturnAbi

ABI shape of an exported result.

LeanExportSignature

Trusted manifest signature for one Lean export.

LeanLibraryDependency

Dependency dylib that must stay alive while a capability is loaded.

LeanLoaderCheck

One bounded preflight finding.

LeanLoaderReport

Structured result of loader preflight for one capability manifest.

LeanModuleInitializer

Initializer for a Lean module hosted by a loaded dylib.

Enums

LeanExportAbiRepr

C ABI representation for one exported argument or result slot.

LeanExportOwnership

Ownership convention for one ABI slot.

LeanExportResultConvention

How an exported result is decoded.

LeanExportSymbolKind

Whether an exported symbol is callable code or a Lean persistent global.

LeanLoaderDiagnosticCode

Stable preflight diagnostic codes for manifest-backed capability loading.

LeanLoaderSeverity

Severity of one loader preflight finding.

Constants

VERSION

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