lean-rs 0.1.1

Safe Rust bindings for Lean 4 interop: runtime initialization, object handles, typed ABI conversions, module loading, exported function calls, semantic handles, and callback handles.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91

//! L1 string streaming callback example.
//!
//! The example stays below `lean-rs-host`: Lean emits JSONL-like strings through
//! the generic interop shim, and Rust receives them through
//! `LeanCallbackHandle<LeanStringEvent>`.

#![allow(clippy::print_stdout)]

use std::io;
use std::path::{Path, PathBuf};
use std::sync::{Arc, Mutex};

use lean_rs::module::{LeanIo, LeanLibrary};
use lean_rs::{LeanCallbackFlow, LeanCallbackHandle, LeanCallbackStatus, LeanRuntime, LeanStringEvent};

fn workspace_root() -> PathBuf {
    let manifest_dir = PathBuf::from(env!("CARGO_MANIFEST_DIR"));
    manifest_dir
        .parent()
        .and_then(Path::parent)
        .map(Path::to_path_buf)
        .unwrap_or(manifest_dir)
}

fn require(condition: bool, message: &'static str) -> Result<(), io::Error> {
    if condition {
        Ok(())
    } else {
        Err(io::Error::other(message))
    }
}

fn main() -> Result<(), Box<dyn std::error::Error>> {
    let workspace = workspace_root();
    let interop_shims = lean_toolchain::build_lake_target(
        &workspace
            .join("crates")
            .join("lean-rs")
            .join("shims")
            .join("lean-rs-interop-shims"),
        "LeanRsInterop",
    )?;
    let consumer = lean_toolchain::build_lake_target(
        &workspace.join("fixtures").join("interop-shims"),
        "LeanRsInteropConsumer",
    )?;

    let runtime = LeanRuntime::init()?;
    let interop_library = LeanLibrary::open_globally(runtime, &interop_shims)?;
    let _interop_module = interop_library.initialize_module("lean_rs_interop_shims", "LeanRsInterop")?;

    let consumer_library = LeanLibrary::open(runtime, &consumer)?;
    let consumer_module = consumer_library.initialize_module("lean_rs_interop_consumer", "LeanRsInteropConsumer")?;
    let add = consumer_module.exported::<(u64, u64), u64>("lean_rs_interop_consumer_add")?;
    let stream = consumer_module.exported::<(usize, usize), LeanIo<u8>>("lean_rs_interop_consumer_jsonl_stream")?;

    let sum = add.call(20, 22)?;
    require(sum == 42, "ordinary Lean export returned an unexpected value")?;

    let rows = Arc::new(Mutex::new(Vec::<String>::new()));
    let callback_rows = Arc::clone(&rows);
    let callback = LeanCallbackHandle::<LeanStringEvent>::register(move |event| {
        if let Ok(mut guard) = callback_rows.lock() {
            guard.push(event.value);
        }
        LeanCallbackFlow::Continue
    })?;

    let (handle, trampoline) = callback.abi_parts();
    let status = stream.call(handle, trampoline)?;
    let status = LeanCallbackStatus::from_abi(status).unwrap_or(LeanCallbackStatus::Panic);
    require(status == LeanCallbackStatus::Ok, status.description())?;
    require(callback.last_error().is_none(), "string callback recorded an error")?;

    let observed = rows.lock().map(|guard| guard.clone()).unwrap_or_default();
    let expected = vec![
        "{\"kind\":\"module\",\"name\":\"LeanRsInteropConsumer\"}".to_owned(),
        "{\"kind\":\"declaration\",\"name\":\"lean_rs_interop_consumer_add\"}".to_owned(),
        "{\"kind\":\"done\",\"count\":2}".to_owned(),
    ];
    require(observed == expected, "string stream sequence did not match")?;

    println!("add={sum}");
    println!("string_callback_status={status:?}");
    for row in &observed {
        println!("stream_row={row}");
    }
    println!("string streaming callback example completed");

    Ok(())
}