1 unstable release

0.1.0 Jun 13, 2023

#12 in #lake

MIT license

145KB
4K SLoC

Lean4 sys

very low level bindings to the Lean4 runtime

Usage

first ensure you install lean4 with elan and lake

and ensure there is at least one C compiler in your path

and how do I use Rust libraries in Lean4?

add following to your 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)

then you can use like following:

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

then you can enjoy Rust in Lean4

@[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)) 
    }
}

No runtime deps

~0–2MB
~39K SLoC