Help with FFI to Rust

Stream: lean4

[Marcus Rossel]

I've been trying to call Rust code from Lean the last couple of days and just can't get it to work. I fundamentally don't understand what I'm doing, so I hope somebody can point me in the right direction.

My setup is as follows:

Directory Structure

lean-egg/
  lakefile.lean
  Lean/
    LeanEgg.lean
    Main.lean
    LeanEgg/Basic.lean
  C/ffi.c
  Rust/
    Cargo.toml
    src/lib.rs

lib.rs, ffi.c and Basic.lean

#[no_mangle]
pub extern "C" fn rust_test(x: u8) -> u8 {
    x
}

#include <lean/lean.h>

extern uint8_t rust_test(uint8_t x);

@[extern "rust_test"]
opaque rustTest : UInt8 → UInt8

Cargo.toml and lakefile.lean

[package]
name = "egg-for-lean"
version = "0.1.0"
edition = "2021"

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

[dependencies]

import Lake
open Lake DSL

-- Cf. https://github.com/lurk-lab/RustFFI.lean

package «lean-egg»

lean_lib LeanEgg where
  srcDir := "Lean"
  precompileModules := true

@[default_target]
lean_exe test where
  srcDir := "Lean"
  root := `Main


def ffiC := "ffi.c"
def ffiO := "ffi.o"

target importTarget pkg : FilePath := do
  let oFile := pkg.buildDir / "c" / ffiO
  let srcJob ← inputFile <| pkg.dir / "C" / ffiC
  buildFileAfterDep oFile srcJob fun srcFile => do
    let flags := #["-I", (← getLeanIncludeDir).toString]
    compileO ffiC oFile srcFile flags

extern_lib ffi pkg := do
  let name := nameToStaticLib "ffi"
  let job ← fetch <| pkg.target ``importTarget
  buildStaticLib (pkg.nativeLibDir / name) #[job]

extern_lib egg_for_lean pkg := do
  proc { cmd := "cargo", args := #["build", "--release"], cwd := pkg.dir / "Rust" }
  let name := nameToStaticLib "egg_for_lean"
  let srcPath := pkg.dir / "Rust" / "target" / "release" / name
  IO.FS.createDirAll pkg.nativeLibDir
  let tgtPath := pkg.nativeLibDir / name
  IO.FS.writeBinFile tgtPath (← IO.FS.readBinFile srcPath)
  return (pure tgtPath)

---

Now in Main.lean I do:

import LeanEgg

def main : IO Unit :=
  IO.println "Hello world!"

#eval rustTest 123

... which produces Lean server printed an error: dyld[29803]: missing symbol called on the #eval. If I set precompileModules := false in lakefile.lean, the error changes to:

Lean server printed an error: libc++abi: terminating due to uncaught exception of type lean::exception: could not find native implementation of external declaration 'rustTest' (symbols 'l_rustTest___boxed' or 'l_rustTest')

What am I doing wrong?

[Schrodinger ZHU Yifan]

I actually don't see the reason.
Can you try lake build instead of #eval? It seems to be an interpreter problem.

---

You can see https://github.com/SchrodingerZhu/hashbrown4lean as an example.

[Marcus Rossel]

@Schrodinger ZHU Yifan Thanks for the hint! Indeed lake build fails with:

$ lake build
stderr:
    Finished release [optimized] target(s) in 0.00s
[3/8] Building LeanEgg
[6/8] Building Main
[7/8] Compiling Main
[8/8] Linking test
error: > /Users/marcus/.elan/toolchains/leanprover--lean4---nightly/bin/leanc -o ./build/bin/test ./build/ir/Main.o ./build/ir/LeanEgg/Basic.o ./build/ir/LeanEgg.o ./build/lib/libegg_for_lean.a ./build/lib/libffi.a
error: stderr:
ld64.lld: warning: ./build/lib/libegg_for_lean.a(egg_for_lean-c19ef5f08729e256.egg_for_lean.9745f57065a7532b-cgu.0.rcgu.o) has architecture arm64 which is incompatible with target architecture x86_64
ld64.lld: error: undefined symbol: _rust_test
>>> referenced by ./build/ir/LeanEgg/Basic.o:(symbol _l_rustTest___boxed+0x1f)
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command `/Users/marcus/.elan/toolchains/leanprover--lean4---nightly/bin/leanc` exited with code 1

This looks like it might be related to the problem addressed in this thread. That is, leancseems to think that it should build for x86, even though I'm on Apple Silicon:

$ arch
arm64

$ leanc --version
clang version 15.0.1 (https://github.com/llvm/llvm-project b73d2c8c720a8c8e6e73b11be4e27afa6cb75bdf)
Target: x86_64-apple-darwin23.0.0
Thread model: posix
InstalledDir: /Users/marcus/.elan/toolchains/leanprover--lean4---nightly/bin

I'm not sure why I'm seeing this behaviour though, as the linked thread concludes with the problem being fixed.

[Sebastian Ullrich]

Did you somehow install an x64 elan?

[Marcus Rossel]

Sebastian Ullrich said:

Did you somehow install an x64 elan?

How could I find that out? Apparently, yes.

[Schrodinger ZHU Yifan]

so the thing is you are actually running a emulated x64 leanc on Apple?

[Marcus Rossel]

Schrodinger ZHU Yifan said:

so the thing is you are actually running a emulated x64 leanc on Apple?

Yup, that seems to have been the problem. Sorry for the noise.