lean-rs 0.2.1

Safe Rust bindings for Lean 4 interop: runtime initialization, object handles, typed ABI conversions, module loading, exported function calls, semantic handles, and callback handles.
Documentation

lean-rs

Safe Rust bindings for hosting Lean 4 capabilities. This crate covers runtime initialization, owned and borrowed object handles, typed first-order ABI conversions, module loading and exported functions, semantic handles (LeanName, LeanLevel, LeanExpr, LeanDeclaration), and a structured error/diagnostic boundary.

Ships the generic interop shim package used by same-process Lean-to-Rust callbacks, but no theorem-prover host shims. If you want sessions, MetaM, and kernel-checked evidence, add lean-rs-host on top.

Quick start

Inside the workspace, run the canonical shipped-crate template first:

cargo run --manifest-path templates/shipped-lean-crate/Cargo.toml

That template is the shortest executable path for a crate that owns Lean source. It uses lean-toolchain in build.rs and LeanCapability at runtime so application code does not hand-write Lake output paths or dylib env-var plumbing.

The minimum consumer is five pieces: a Lean module declaring an @[export], a lakefile.lean that builds it into a shared library, a Rust build.rs that emits the link and rpath directives, a Cargo.toml, and a Rust caller. All five together fit on one screen.

Cargo.toml:

[package]
name = "my_app"
version = "0.1.0"
edition = "2024"

[dependencies]
lean-rs = "0.2"

[build-dependencies]
lean-toolchain = "0.2"

build.rs—one helper covers link-search, link-lib, the runtime rpath, Lake build, Cargo rerun triggers, the compile-time manifest path, and trusted export signature metadata:

fn main() -> Result<(), Box<dyn std::error::Error>> {
    use lean_toolchain::{
        LeanExportAbiRepr, LeanExportArgAbi, LeanExportOwnership, LeanExportResultConvention, LeanExportReturnAbi,
        LeanExportSignature,
    };

    lean_toolchain::CargoLeanCapability::new("lean", "MyCapability")
        .package("my_app")
        .module("MyCapability")
        .export_signature(LeanExportSignature::function(
            "my_app_add",
            vec![
                LeanExportArgAbi::new(LeanExportAbiRepr::U64, LeanExportOwnership::None),
                LeanExportArgAbi::new(LeanExportAbiRepr::U64, LeanExportOwnership::None),
            ],
            LeanExportReturnAbi::new(
                LeanExportAbiRepr::U64,
                LeanExportOwnership::None,
                LeanExportResultConvention::Pure,
            ),
        ))
        .build()?;
    Ok(())
}

lean/lakefile.lean: a minimal Lake package emitting one shared library. Lake uses guillemets (« ») as its idiomatic quoting for package and library names; plain ASCII names also work.

import Lake
open Lake DSL

package «my_app»

@[default_target]
lean_lib «MyCapability» where
  defaultFacets := #[LeanLib.sharedFacet]

lean/MyCapability.lean—one Rust-callable export:

@[export my_app_add]
def add (a b : UInt64) : UInt64 := a + b

src/main.rs—open the build-script capability, dispatch typed:

use lean_rs::{LeanBuiltCapability, LeanCapability, LeanRuntime};

fn main() -> Result<(), Box<dyn std::error::Error>> {
    let runtime = LeanRuntime::init()?;
    let capability = LeanCapability::from_build_manifest(
        runtime,
        LeanBuiltCapability::manifest_path(env!("LEAN_RS_CAPABILITY_MY_CAPABILITY_MANIFEST")),
    )?;
    let add = capability.exported::<(u64, u64), u64>("my_app_add")?;
    println!("{}", add.call(40, 2)?);  // 42
    Ok(())
}

Build and run:

cargo run

CargoLeanCapability hides Lake's shared-library facet, Cargo rerun triggers, cache, filename convention, trusted export signatures, and the artifact manifest handoff. LeanCapability reads that manifest and keeps the built path, dependency bundle, initializer names, and checked export metadata together at runtime. Use build_lake_target, LeanLibraryBundle, and LeanLibrary directly only for lower-level custom interop.

See the complete shipping recipe at docs/recipes/ship-crate-with-lean.md. Worker applications use the same built capability descriptor with lean-rs-worker-parent and point LeanWorkerChild at an app-owned worker-child binary; the recipe shows that packaging path as well.

For a complete advanced same-process example that also lets Lean call a Rust callback, run cargo run -p lean-rs --example interop_callback in the workspace and read docs/recipes/downstream-interop.md. For a trusted same-process string callback example, run cargo run -p lean-rs --example string_streaming and read docs/recipes/string-callback-streaming.md. Worker tools that need process isolation, live rows, diagnostics, terminal summaries, timeouts, or memory cycling should use lean-rs-worker-parent typed commands instead of exposing callback handles.

The Args and R generics on LeanModule::exported_unchecked are sealed by the LeanAbi / LeanArgs / DecodeCallResult traits, so unsupported types fail at compile time rather than producing wrong decodes at runtime.

See also

License

Dual-licensed under MIT or Apache-2.0 at your option.