Lean4 sys

对 Lean4 运行时的非常底层的绑定

用法

首先确保使用 lean4 和 elan 以及 lake 安装了 lean4

并确保您的路径中至少有一个 C 编译器

我在 Lean4 中如何使用 Rust 库？

将以下内容添加到您的 lakefile.lean

def cargoBuildRelease (name : String) (tomlFileDir : FilePath) (moreArgs : Array String := #[]) : BuildM Unit := do
  let manifestPath  :=  (tomlFileDir / "Cargo.toml").toString
  logStep s!"Compiling {name} with manifest path {manifestPath}"
  
  proc {
    cmd := "cargo"
    args := #["build", "--release", "--manifest-path", manifestPath] ++ moreArgs
  }


def buildCargo (name : String) (tomlFileDir : FilePath) (moreArgs : Array String := #[]) : SchedulerM (BuildJob FilePath) := do
  let file := tomlFileDir / "target" / "release" / (nameToStaticLib name)
  BuildJob.nil.bindSync fun _ _ => do
    let trace ← buildFileUnlessUpToDate file (← (pure BuildTrace.nil)) <| (cargoBuildRelease name tomlFileDir moreArgs)
    return (file, trace)

然后您可以使用以下方式使用它

target lean_test_rs (pkg : Package) : FilePath := do
  buildCargo "lean_test" (pkg.dir / "lean_test")


extern_lib lean_test (pkg : Package) := do
  fetch <| pkg.target ``lean_test_rs

然后您就可以在 Lean4 中享受 Rust 的功能了

@[extern "rust_hello"]
opaque hello : BaseIO Unit

// in your cargo project
use lean4_sys::*;

#[no_mangle]
pub extern "C" fn lean_rust_hello(_: lean_obj_arg) -> lean_obj_res {
    unsafe { 
        println!("Hello from Rust🦀!");
        lean_io_result_mk_ok(lean_box(0)) 
    }
}