leo3-codegen: From cdylib to Lean `extern` Declarations

leo3-codegen is a standalone CLI that reads the binding metadata embedded in a Leo3 cdylib and generates the matching Lean 4 @[extern] declaration files. It is a static binary inspection tool: it does not load the library, does not execute any of its code, and does not require a Lean installation.

The macros #[leanmodule] and #[leanclass] serialize a JSON description of every export (schema v2) into the compiled artifact. leo3-codegen recovers those JSON blobs and renders them as .lean files you can drop into a Lake project.

Installation

Published on crates.io since Leo3 0.3.1:

cargo install leo3-codegen

Verify:

leo3-codegen --help

To generate declarations for a given cdylib, that cdylib must have been built with leo3 >= 0.3.0 (metadata embedding) — and for macOS/Windows artifacts, with leo3 >= 0.3.1 (see Cross-platform metadata extraction).

Complete Walkthrough

This walkthrough is verified end-to-end on Linux (Rust 1.97, Lean 4.30.0).

Step 1: Create the cdylib crate

# native/Cargo.toml
[package]
name = "calc-native"
version = "0.1.0"
edition = "2021"

[lib]
crate-type = ["cdylib"]

[dependencies]
leo3 = { version = "0.3.1", features = ["macros"] }

[build-dependencies]
leo3-build-config = "0.3.1"

// native/build.rs
fn main() {
    leo3_build_config::use_leo3_cfgs();
}

crate-type = ["cdylib"] is required: the metadata lives in the shared library, and the generated @[extern] symbols must be dynamically linkable.

Step 2: Export functions and classes

// native/src/lib.rs
use leo3::prelude::*;

#[leanmodule(name = "Calc")]
mod calc {
    use leo3::prelude::*;

    #[leanfn(name = "calc_add")]
    pub fn add(a: u64, b: u64) -> u64 {
        a + b
    }

    #[leanfn(name = "calc_greet")]
    pub fn greet(name: String) -> String {
        format!("Hello, {name}!")
    }
}

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

#[leanclass]
impl Counter {
    pub fn new(initial: i64) -> Self {
        Counter { value: initial }
    }

    pub fn get(&self) -> i64 {
        self.value
    }

    pub fn increment(&mut self) {
        self.value += 1;
    }
}

Step 3: Build

cd native
LEO3_NO_LEAN=1 cargo build --release

LEO3_NO_LEAN=1 skips Lean detection/linking so the cdylib does not link libleanshared itself — the host Lean executable provides those symbols at runtime, and linking them twice causes duplicate-symbol failures.

Step 4: Run the code generator

leo3-codegen target/release/libcalc_native.so -o ../lean/CalcGuide

../lean/CalcGuide/Counter.lean
../lean/CalcGuide/Calc.lean

One file per #[leanmodule] and one per #[leanclass]. Module output:

-- lean/CalcGuide/Calc.lean
-- Generated by leo3-codegen. Do not edit.
-- Module: Calc

@[extern "calc_add"] opaque calc_add : UInt64 → UInt64 → UInt64

@[extern "calc_greet"] opaque calc_greet : String → String

Class output:

-- lean/CalcGuide/Counter.lean
-- Generated by leo3-codegen. Do not edit.
-- Class: Counter

opaque Counter.ffi : NonemptyType
def Counter : Type := Counter.ffi.val
instance : Nonempty Counter := Counter.ffi.property

@[extern "__lean_ffi_Counter_new"] opaque Counter.new : Int64 → Counter
@[extern "__lean_ffi_Counter_get"] opaque Counter.get : Counter → Int64
@[extern "__lean_ffi_Counter_increment"] opaque Counter.increment : Counter → Counter

Output naming rules:

A module #[leanmodule(name = "Calc")] is written to Calc.lean.
Dotted module names generate nested paths: #[leanmodule(name = "Foo.Bar")] produces Foo/Bar.lean, exactly where import Foo.Bar resolves it relative to the output directory.
A class Counter is written to Counter.lean.
Existing files are overwritten; the header marks them as generated.

Step 5: Reference the declarations from a Lake project

The generated files contain no import lines and no module header — Lake derives module names from their paths. Placing them under lean/CalcGuide/ makes them modules CalcGuide.Calc and CalcGuide.Counter:

lean/
├── lakefile.lean
├── lean-toolchain
├── CalcGuide.lean          # library root
├── CalcGuide/
│   ├── Calc.lean           # generated
│   └── Counter.lean        # generated
└── Main.lean

-- lean/lakefile.lean
import Lake
open Lake DSL

package «CalcGuide» where
  leanOptions := #[⟨`autoImplicit, false⟩]

@[default_target]
lean_lib «CalcGuide» where
  moreLinkArgs := #["-L", "../native/target/release", "-l", "calc_native"]

lean_exe «app» where
  root := `Main
  moreLinkArgs := #["-L", "../native/target/release", "-l", "calc_native"]

moreLinkArgs points the linker at the cdylib: -L <dir> plus -l calc_native (the crate name with the lib prefix and .so suffix removed).

-- lean/CalcGuide.lean
import CalcGuide.Calc
import CalcGuide.Counter

-- lean/Main.lean
import CalcGuide.Calc

def main : IO Unit := do
  IO.println s!"calc_greet(\"Lean\") = {calc_greet "Lean"}"

Build and run:

cd lean
lake build app
LD_LIBRARY_PATH=../native/target/release .lake/build/bin/app

calc_greet("Lean") = Hello, Lean!

On macOS use DYLD_LIBRARY_PATH instead of LD_LIBRARY_PATH; on Windows the DLL must be on PATH or next to the executable.

Calling convention and class declarations

The generated declarations follow Lean's extern calling convention, and the macro-generated wrappers match it:

Fixed-width scalars (UInt8–UInt64, Int8–Int64, USize, ISize, Float32, Float, Bool, Char) cross the FFI boundary unboxed as raw C values, so calc_add 20 22 calls uint64_t calc_add(uint64_t, uint64_t).
Everything else (String, Array, Option, Except, Prod, class objects) crosses as a boxed lean_object*.

(On the released 0.3.1 crates both properties were broken — boxed wrappers plus a bare opaque Counter : Type that Lean rejected for missing Inhabited/Nonempty — tracked in leanOxide/leo3#159; the fix lands in the next release. Until then, scalar APIs can use the hand-written pattern from examples/lake-integration.)

Class types are introduced through NonemptyType (the standard library's own IO.RealWorld pattern) so constructor/updater declarations elaborate; see the class output sample above.

#[leanfn] exports additionally get an all-boxed {name}_boxed companion symbol (Lean's own _boxed entry-point convention), used by Leo3's dynamic loading path (leo3::module::LeanModule, see the module_loading example).

Cross-platform Metadata Extraction

The macros embed each metadata entry twice: as #[no_mangle] #[used] statics (JSON in the data segment, named __leo3_module_metadata_json_* / __leo3_class_metadata_json_*), and as a framed copy (magic marker + explicit lengths) in a dedicated leo3meta link section. leo3-codegen then reads from every source available on the target and merges the results, deduplicated by name. The redundancy exists because each platform's linker treats unreferenced data symbols differently:

Platform	What codegen reads	Why
Linux (ELF)	Symbol table (primary) + `leo3meta` section	The ELF linker keeps unreferenced `#[used]` symbols visible in the dynamic symbol table
macOS (Mach-O)	`__DATA,__leo3meta` section	The Mach-O linker does not surface the unreferenced metadata statics in the dylib's symbol table
Windows (PE)	Export table + `leo3meta` section	Linked DLLs strip the COFF symbol table, but `#[no_mangle]` statics survive as exports. The section name is kept ≤ 8 bytes because MSVC `link.exe` truncates longer PE section names

Recovering the section-based copies requires leo3 >= 0.3.1 on the build side (that is the release whose macros embed the framed section); the leo3-codegen binary must likewise be >= 0.3.1 to scan sections and export tables.

Common failure modes

no leo3 metadata found in library
- The file is not a cdylib (a staticlib, rlib, or host binary carries no dynamic metadata symbols).
- The crate was built without the macros feature, or with leo3 < 0.3.0, so nothing was embedded.
- On macOS/Windows the crate was built with leo3 < 0.3.1, where only the (invisible to the linker) symbol-table path existed.
Stripping is not a problem on leo3 >= 0.3.1: when the symbol table is gone (or never existed, on Mach-O/PE), codegen falls back to the framed leo3meta section that the macros embed on every platform.
failed to parse object file — the argument is not a recognized ELF/Mach-O/PE object (e.g. a JSON file or an archive).
failed to parse module metadata — version skew: the metadata JSON schema is tied to the leo3 release that built the library. Upgrade leo3-codegen to the same minor version as the library's leo3.

CLI Reference

leo3-codegen [OPTIONS] <cdylib>...

OPTIONS:
    -o, --output <DIR>    Output directory for generated .lean files (default: .)
    -h, --help            Print this help message

Multiple libraries can be passed; each is processed in order into the same output directory.
The output directory (and any module-path subdirectories) is created if missing.
Exit code is non-zero on the first error; already-written files from earlier libraries are not rolled back.

Relationship to the examples

The repository ships two working Lean↔Rust templates:

examples/lake-integration — hand-written raw extern "C" functions with hand-written declarations;
examples/class-integration — exactly the macro + codegen pipeline described in this guide, built and verified end to end in CI.

They cover different routes to the same destination:

	`examples/lake-integration`	`leo3-codegen`
Rust side	Hand-written `extern "C"` functions using `leo3::ffi` directly	`#[leanmodule]` / `#[leanclass]` macros
Lean declarations	Hand-written `@[extern]` files	Generated from cdylib metadata
Scalar ABI	Native C types (`u64`, `i64`, ...) — Lean's unboxed extern convention	Same convention, generated automatically
Best for	Small, stable APIs	Large or frequently changing surfaces; keeping declarations in sync automatically

The lakefile mechanics (moreLinkArgs, runtime library path) are identical; see the getting-started Lake integration section for the template walkthrough.

Navigation Menu

Uh oh!

leo3-codegen: From cdylib to Lean `extern` Declarations

Installation

Complete Walkthrough

Step 1: Create the cdylib crate

Step 2: Export functions and classes

Step 3: Build

Step 4: Run the code generator

Step 5: Reference the declarations from a Lake project

Calling convention and class declarations

Cross-platform Metadata Extraction

Common failure modes

CLI Reference

Relationship to the examples

See Also

Uh oh!

FilesExpand file tree

codegen.md

Latest commit

History

codegen.md

File metadata and controls

leo3-codegen: From cdylib to Lean extern Declarations

Installation

Complete Walkthrough

Step 1: Create the cdylib crate

Step 2: Export functions and classes

Step 3: Build

Step 4: Run the code generator

Step 5: Reference the declarations from a Lake project

Calling convention and class declarations

Cross-platform Metadata Extraction

Common failure modes

CLI Reference

Relationship to the examples

See Also

leo3-codegen: From cdylib to Lean `extern` Declarations