lean.rs

A bridge between Lean 4 and Rust, in both directions.

• Rust to Lean. Call Rust from Lean with automatic marshalling of String, Nat, Int, List, and arbitrary inductives. Hold a live Rust value inside Lean as an opaque handle and call its methods. Two macros, #[derive(LeanType)] and #[lean_export], generate the boxing, refcounting, and name mangling, and the same bindings work whether Lean links the static library or loads it at runtime.
• Lean to Rust. Embed the Lean elaborator and kernel as a linear Kernel resource and drive it from Rust. Import modules, elaborate source, #eval constants to live objects, and add kernel declarations, all from Rust code.
• Swappable kernel. Swap nanoda, a pure-Rust Lean 4 kernel, in for Lean's built-in C++ one. Declarations marshal straight from live Lean heap objects into nanoda's structures, with no export file and no external checker process. We re-checked every declaration in Mathlib this way, 735,861 of them, in half an hour.

Quick start

Scalars cross the boundary unboxed, so the simplest call needs no runtime support. Declare an @[extern] on the Lean side and write the matching #[no_mangle] function on the Rust side.

@[extern "lean_rs_add"]
opaque add (a b : UInt64) : UInt64

#eval add 19 23   -- 42, computed in Rust

#[no_mangle]
pub extern "C" fn lean_rs_add(a: u64, b: u64) -> u64 { a + b }

Non-scalar values must be marshalled through the runtime. Exposing a whole Rust type takes two annotations. The macros emit the opaque handle, the field accessors, and the ABI-correct @[extern] wrappers, so a Lean program can hold the value and call its methods.

#[derive(lean_rs::LeanType)]
pub struct Stack { items: Vec<i64> }

#[lean_rs::lean_export]
impl Stack {
    pub fn empty() -> Stack { Stack { items: vec![] } }
    pub fn push(&self, x: i64) -> Stack { /* returns a fresh handle */ }
    pub fn sum(&self) -> i64 { self.items.iter().sum() }
}

Driving Lean from Rust

The reverse direction embeds Lean itself. Kernel wraps a Lean Environment as a linear resource and drives the runtime through the lean_* entry points.

let mut k = lean_rs::kernel::Kernel::new();   // LEAN_PATH auto-discovered
k.import(&["Init", "LeanRs"])?;               // import modules by name
k.elaborate_with("def x : Nat := 7").run()?;  // drive the elaborator
let n: u64 = k.eval("x")?;                     // typed eval, marshalled back to Rust
k.add_axiom("myAxiom", "Nat")?;               // add a kernel declaration

Swapping the kernel

A Lean kernel is the component that decides whether a proof is valid, so a second, independent kernel checks the first. set_kernel_backend(KernelBackend::Nanoda) turns Lean's built-in kernel off on the gate its own calls go through (debug.skipKernelTC) and hands each declaration to nanoda instead. Nothing is serialised. The marshaller walks live ConstantInfo, Expr, Level, and Name objects off the Lean heap and interns them into nanoda's own structures.

The same check is available from a .lean file. @[nanoda] certifies one declaration and #certify_module certifies a whole file; pair either with set_option debug.skipKernelTC true to make nanoda the sole checker. nanoda_certify_all(threads) checks an entire imported library in parallel, and the nanoda_check <Module> binary is how we re-checked all of Mathlib.

Where to go next

GETTING_STARTED.md walks a fresh clone through every step above, and examples/ has a self-contained walkthrough for each one, from the scalar call to the whole-Mathlib nanoda run. The Verso manual is the long-form narrative tutorial and the API reference is this rustdoc.

Installation

You need a Lean toolchain, pinned in lean-toolchain, and a Rust toolchain whose ABI agrees with Lean's. On macOS the bignum bridge wants GMP headers (brew install gmp); on Linux they are usually already present (apt install libgmp-dev).

elan toolchain install $(cat lean-toolchain)

Build and run

Lake drives cargo for you.

lake exe lean_rs     # builds liblean_rs, the C shim, links and runs the smoke test

Or work with the Rust crate on its own.

cd rust
cargo build --release     # produce liblean_rs.a / .dylib
cargo test                # unit + kernel-embedding tests (live Lean runtime)
cargo doc --no-deps --open

Checking a library with nanoda

nanoda_check imports a compiled library off LEAN_PATH and re-certifies every constant with the pure-Rust kernel. This is how we ran it over all of Mathlib.

cd rust
cargo build --release --bin nanoda_check
LEAN_PATH="<Mathlib>/.lake/build/lib/lean:<deps>:<toolchain>/lib/lean" \
  ./target/release/nanoda_check Mathlib 8
# OK: nanoda checked 735861 declarations (736618 constants enumerated) in 1884.1s

Layout

lean-toolchain      pinned Lean version (Lake and cargo must agree on the ABI)
lakefile.lean       builds the Rust staticlib via cargo, the C shim, and lean_rs
Main.lean           the smoke-test executable (reflective FFI round-trips)
LeanRs/             the Lean support library (macros, FFI bindings, @[nanoda])
rust/               the `lean_rs` crate, the Rust side of the bridge
  src/object/       marshalling: type-tagged, refcount-owning Lean handles
  src/kernel.rs     the embedded Lean elaborator and kernel
  src/nanoda.rs     the nanoda kernel swap (heap-to-heap marshalling)
  src/bin/nanoda_check.rs   the whole-library checker
  lean_derive/      the #[derive(LeanType)] / #[lean_export] proc-macros
native/leanrs.c     generic C shim re-exporting lean.h as real symbols
docs/               the Verso manual (its own Lake project)
tests/integration/  runnable consumer projects

Editing this README

The overview above is generated from the crate's doc comment, so the crate front page on docs.rs and this README never drift. Edit rust/src/lib.rs (the //! block) for the overview or rust/README.tpl for everything else, then regenerate:

cargo readme --project-root rust --template README.tpl --output README.md

CI runs the same command and fails if README.md is out of date.