FFI between Lean 4 and Rust

A simple example demonstrating FFI between Lean 4 and Rust. Successfully compiled on Lean 4.22.0-rc4.

Features

• Call Rust functions from Lean
• Pass strings and custom data structures between languages

Structure

• LeanFFI/FFI.lean - FFI bindings
• Main.lean - Call Rust functions
• ffi/ - Rust library
  • src/lib.rs - Rust implementation
  • shim.c - C wrapper

Build and Run

Make sure you have Lean 4 and Rust installed, then run:

lake build && lake exe lean_ffi

This will output messages from both Lean and Rust, demonstrating the FFI integration.

If you modify the code, you may need to run lake clean and cargo clean to rebuild everything.

🦀