Leo3: Rust Bindings for Lean4

Leo3 provides safe, ergonomic Rust bindings to the Lean4 theorem prover, inspired by PyO3's architecture.

Quick Start

Requires Lean 4.25.2 (install via elan).

[dependencies]
leo3 = "0.2.1"

use leo3::prelude::*;

fn main() -> LeanResult<()> {
    leo3::prepare_freethreaded_lean();

    leo3::with_lean(|lean| {
        let s = LeanString::mk(lean, "Hello from Rust!")?;
        println!("{}", LeanString::cstr(&s)?);

        let n = LeanNat::from_usize(lean, 42)?;
        println!("{}", LeanNat::to_usize(&n)?);
        Ok(())
    })
}

with_lean() is the canonical safe entry point for caller code. It ensures the shared runtime worker exists and attaches the current thread before handing out a Lean<'l> token. prepare_freethreaded_lean() is still useful when you want to pay initialization cost eagerly during startup.

Cargo Features

Default features: none. The default build keeps the public surface intentionally minimal: runtime initialization, smart pointers, core type wrappers/conversions, closures, thunks, and synchronization helpers are always available.

Feature	Enables
default (none)	Core runtime/token APIs, conversions, closures, thunks, sync helpers, Lean type wrappers
experimental-containers	Experimental container wrappers for HashMap, HashSet, RBMap; all three now use real Lean runtime semantics for a narrow key matrix
macros	#[leanfn], #[leanclass], #[leanmodule], #[derive(IntoLean, FromLean)]
meta	leo3::meta::* metaprogramming APIs
io	leo3::io::* IO / filesystem / process / environment helpers
task	leo3::task, leo3::task_combinators, leo3::promise
module-loading	leo3::module::* dynamic shared-library loading
tokio	leo3::tokio_bridge::* (implies task)
runtime-tests	Runtime-dependent integration tests (for development/CI)

Example dependency declarations:

# Minimal core surface
leo3 = "0.2.1"

# Opt into specific subsystems
leo3 = { version = "0.2.1", features = ["macros", "meta", "task"] }

# Opt into currently experimental container wrappers
leo3 = { version = "0.2.1", features = ["experimental-containers"] }

Lean Discovery

Leo3 build scripts resolve Lean in a single shared order:

1. LEO3_NO_LEAN=1 disables Lean detection and linking entirely.
2. LEO3_CONFIG_FILE=/path/to/leo3-build-config.txt provides an explicit key/value config.
3. Host discovery tries LEO3_CROSS_*, then LEAN_HOME (with optional LEAN_LIB_DIR / LEAN_INCLUDE_DIR), then lake, then elan, then PATH.

leo3-ffi is the authoritative detector. It exports the resolved config through Cargo's DEP_LEAN4_LEO3_CONFIG, and leo3 consumes that propagated config so both crates always agree on Lean version cfgs and linker settings.

Explicit overrides are authoritative: if DEP_LEAN4_LEO3_CONFIG, LEO3_CONFIG_FILE, LEO3_CROSS_*, LEAN_HOME, LEAN_LIB_DIR, or LEAN_INCLUDE_DIR is set but invalid, Leo3 reports that error instead of silently falling back to a lower-priority source.

Capability Overview

Core Type Conversions

Leo3's built-in IntoLean / FromLean support matrix is intentionally small and explicit:

Rust shape	Lean shape	IntoLean	FromLean	Cost / ownership rule
u8-u64, usize, i8-i64, isize, f32, f64, bool, char, ()	scalar wrappers / Unit	yes	yes	value conversion; allocating the Lean object on Rust -> Lean
String	String	yes	yes	allocative copy
&str	String	yes	no	allocative copy into Lean only
Vec<T>	Array	yes	yes	allocates the container and converts elements one by one
Option<T>	Option	yes	yes	recursive container conversion
Result<T, E>	Except E T	yes	yes	recursive container conversion; Lean keeps the error type first
(A, B)	Prod A B	yes	yes	recursive pair conversion; only pairs are built in
Vec<u8> / &[u8] helpers	ByteArray	helper path	helper path	bulk memcpy fast path via vec_u8_*, slice_u8_into_lean, to_lean!, from_lean!
T: ExternalClass	Lean external object	yes	yes, if T: Clone	Rust -> Lean stores ownership in an external object; Lean -> Rust clones the inner value

Rules behind that table:

• FromLean is not implemented for &str; round-trips use String.
• Vec<u8> does not use a specialized trait impl on stable Rust. The optimized ByteArray path is exposed through helper functions and the to_lean! / from_lean! macros.
• FromLean for T: ExternalClass + Clone is clone-based extraction, not borrowing. Borrow-first access goes through LeanExternal<T>::borrow(), try_get_mut(), and try_take_inner() (with get_ref() / get_mut() still available as lower-level APIs).
• User-defined types can extend the matrix with manual impls or #[derive(IntoLean, FromLean)].

Experimental Container Wrappers (experimental-containers)

LeanHashMap, LeanHashSet, and LeanRBMap are available only behind the experimental-containers feature.

These APIs are still gated explicitly so the default public surface remains semantically honest while container support is being completed.

Current status:

• LeanHashMap now uses Lean's real runtime representation for a narrow key matrix by pairing exported Hashable closures with boxed DecidableEq closures.
• LeanHashSet now uses the same real runtime path for the same narrow key matrix.
• LeanRBMap now uses Lean's real runtime representation and reduced-arity container entry points for a narrow key matrix (Nat, Int, String, and fixed-width signed integer wrappers).
• runtime tests now cover duplicate inserts, replacement semantics, string-key support, and cross-family parity for the supported paths.

Procedural Macros (macros)

#[leanfn] — Export Rust functions to Lean:

# #[cfg(feature = "macros")]
# mod leanfn_doctest {
use leo3::prelude::*;

#[leanfn]
fn add(a: u64, b: u64) -> u64 {
    a + b
}
# }

#[leanclass] — Expose Rust structs as Lean external classes with auto-generated FFI wrappers and Lean source declarations:

# #[cfg(feature = "macros")]
# mod leanclass_doctest {
use leo3::prelude::*;

#[derive(Clone)]
#[leanclass]
struct Counter { value: i64 }

#[leanclass]
impl Counter {
    fn new() -> Self { Counter { value: 0 } }
    fn get(&self) -> i64 { self.value }
    fn increment(&mut self) { self.value += 1; }
}
# }

#[leanclass] receiver semantics are fixed:

Rust receiver	Lean-visible signature rule	Runtime rule
no receiver	A -> ... -> R	parameters use FromLean, result uses IntoLean
&self	Self -> A -> ... -> R	shared borrow of the external object
&mut self, -> ()	Self -> A -> ... -> Self	copy-on-write mutation; returns the updated object
&mut self, -> R	Self -> A -> ... -> Prod Self R	copy-on-write mutation; preserves both updated object and value
self	Self -> A -> ... -> R	exclusive receivers move out; shared receivers clone first

&mut self and self methods therefore require the class type to implement Clone, because the shared-receiver fallback is clone-based.

Generated Lean declaration strings accept a narrower type grammar than "anything that implements conversion traits". The supported declaration shapes are:

• scalars: integers, floats, bool, char, String, ()
• Self, the current struct name, and other plain non-generic path types
• Vec<T>, Option<T>, Result<T, E>
• pairs (A, B)

The macro intentionally rejects these declaration shapes at compile time:

• references such as &str or &T
• tuples with arity other than 0 or 2
• generic path types other than Vec<T>, Option<T>, and Result<T, E>
• generic #[leanclass] structs, generic impl blocks, generic methods, and non-identifier parameter patterns

Plain non-generic path types are emitted verbatim into the generated Lean type string. That means the Rust side still needs the relevant conversion impls, and the Lean side still needs a matching type name in scope.

#[derive(IntoLean)] / #[derive(FromLean)] — Automatic conversion derive macros.

#[leanmodule] now has an explicit module-registration story too: Leo3 treats inline #[leanfn] items inside the annotated module as the module's implicit export set, and generates __leo3_module_metadata() so downstream Rust code can inspect the chosen Lean-visible names.

For a single runnable example that combines module initialization, exported functions, and an external class, run:

cargo run --example macro_pipeline --features macros

That example exercises a generated initialize_* module entry point, #[leanfn] FFI wrappers, and the Lean declaration strings emitted for #[leanclass].

Meta-Programming (meta)

Full access to Lean's kernel and elaborator:

• LeanEnvironment — Create and manage declaration environments
• LeanExpr — Build expressions (binders, applications, literals, lambda, forall)
• LeanDeclaration — Define axioms, definitions, and theorems
• MetaMContext — Type inference, type checking, definitional equality, proof validation
• Tactic support

IO, Tasks, and Dynamic Loading

• io: console, filesystem, environment variables, process, and time helpers
• task: LeanTask / LeanPromise plus combinators (join, race, select, timeout)
• module-loading: LeanModule for loading compiled Lean shared libraries
• tokio: async bridge for Lean tasks
• Core (always available): LeanClosure and LeanThunk

Architecture

leo3/
├── leo3/                   # Safe high-level abstractions
├── leo3-ffi/               # Raw FFI bindings to Lean4's C API
├── leo3-build-config/      # Build-time Lean4 detection and configuration
├── leo3-macros/            # Procedural macro entry points
├── leo3-macros-backend/    # Procedural macro implementations
└── leo3-ffi-check/         # FFI layout validation (à la pyo3-ffi-check)

Design

• Lean<'l> token proves runtime initialization at compile-time
• LeanBound<'l, T> (lifetime-bound), LeanRef<T> (unbound), LeanUnbound<T> (thread-safe) smart pointers with automatic reference counting
• #[repr(transparent)] zero-cost wrappers
• Copy-on-write semantics for &mut self FFI methods
• Worker thread architecture for all Lean runtime calls (avoids mimalloc heap issues)
• Version support: Lean 4.20.0–4.30 with #[cfg(lean_4_25)] gates

Comparison with PyO3

PyO3	Leo3
Python<'py>	Lean<'l>
Bound<'py, T>	LeanBound<'l, T>
Py<T>	LeanRef<T>
#[pyfunction]	#[leanfn]
#[pyclass]	#[leanclass]

Development

See TESTING.md for the full tiered CI map, the current contract notes, architecture notes, and the contributor guide. Common local commands:

LEO3_NO_LEAN=1 cargo test --locked --workspace --exclude leo3 --lib
LEO3_NO_LEAN=1 cargo test --locked -p leo3 --no-default-features --test test_features
LEO3_NO_LEAN=1 cargo test --locked -p leo3 --no-default-features --test test_surface_contract
LEO3_NO_LEAN=1 cargo test --locked -p leo3 --no-default-features --features experimental-containers --test test_features
LEO3_NO_LEAN=1 cargo test --locked -p leo3 --features macros --test test_compile_error
cargo test --locked --all-features --workspace

License

MIT OR Apache-2.0

Acknowledgments

• PyO3 — Architectural inspiration
• Lean4 — The theorem prover Leo3 binds to