Skip to content

Commit 344c5f1

Browse files
committed
chore: Configure Iroh with net feature
1 parent daab211 commit 344c5f1

8 files changed

Lines changed: 5366 additions & 388 deletions

File tree

Cargo.lock

Lines changed: 5276 additions & 299 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

Cargo.toml

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -13,13 +13,13 @@ rayon = "1"
1313
rustc-hash = "2"
1414
indexmap = { version = "2", features = ["rayon"] }
1515
tiny-keccak = { version = "2", features = ["keccak"] }
16-
17-
# bytes = "1.10.1"
18-
# [target.'cfg(not(all(target_os = "macos", target_arch = "aarch64")))'.dependencies]
19-
# iroh = "0.34.0"
20-
# tokio = "1.44.1"
21-
# iroh-base = "0.34.0"
22-
# iroh-blobs = { version = "0.34.0", features = ["rpc"] }
16+
# Iroh dependencies
17+
bytes = { version = "1.10.1", optional = true }
18+
tokio = { version = "1.44.1", optional = true }
19+
iroh = { version = "0.34.0", optional = true }
20+
iroh-base = { version = "0.34.0", optional = true }
21+
iroh-blobs = { version = "0.34.0", features = ["rpc"], optional = true }
2322

2423
[features]
2524
parallel = ["multi-stark/parallel"]
25+
net = ["bytes", "tokio", "iroh", "iroh-base", "iroh-blobs"]

Main.lean

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
import Ix.Cli.ProveCmd
22
import Ix.Cli.StoreCmd
3-
-- import Ix.Cli.SendCmd
4-
-- import Ix.Cli.RecvCmd
3+
import Ix.Cli.SendCmd
4+
import Ix.Cli.RecvCmd
55
import Ix
66

77
def VERSION : String :=
@@ -13,9 +13,9 @@ def ixCmd : Cli.Cmd := `[Cli|
1313

1414
SUBCOMMANDS:
1515
proveCmd;
16-
storeCmd
17-
-- sendCmd;
18-
-- recvCmd
16+
storeCmd;
17+
sendCmd;
18+
recvCmd
1919
]
2020

2121
def main (args : List String) : IO UInt32 := do

c/iroh.c

Lines changed: 35 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -1,35 +1,35 @@
1-
// #include "lean/lean.h"
2-
// #include "rust.h"
3-
4-
// extern lean_obj_res c_rs_iroh_send(b_lean_obj_arg bytes) {
5-
// c_result *result = rs_iroh_send(bytes);
6-
// lean_object *io_result;
7-
// if (result->is_ok) {
8-
// io_result = lean_io_result_mk_ok(lean_box(0));
9-
// }
10-
// else {
11-
// io_result = lean_mk_io_user_error(lean_mk_string(result->data));
12-
// }
13-
// rs__c_result_unit_string_free(result);
14-
15-
// return io_result;
16-
// }
17-
18-
// extern lean_obj_res c_rs_iroh_recv(b_lean_obj_arg ticket, size_t buffer_capacity) {
19-
// char const *ticket_str = lean_string_cstr(ticket);
20-
// // Buffer is allocated optimistically, but if the download fails it must be freed explicitly
21-
// lean_object *buffer = lean_alloc_sarray(1, 0, buffer_capacity);
22-
// c_result *result = rs_iroh_recv(ticket_str, buffer, buffer_capacity);
23-
24-
// lean_object *io_result;
25-
// if (result->is_ok) {
26-
// io_result = lean_io_result_mk_ok(buffer);
27-
// }
28-
// else {
29-
// io_result = lean_mk_io_user_error(lean_mk_string(result->data));
30-
// free(buffer);
31-
// }
32-
// rs__c_result_unit_string_free(result);
33-
34-
// return io_result;
35-
// }
1+
#include "lean/lean.h"
2+
#include "rust.h"
3+
4+
extern lean_obj_res c_rs_iroh_send(b_lean_obj_arg bytes) {
5+
c_result *result = rs_iroh_send(bytes);
6+
lean_object *io_result;
7+
if (result->is_ok) {
8+
io_result = lean_io_result_mk_ok(lean_box(0));
9+
}
10+
else {
11+
io_result = lean_mk_io_user_error(lean_mk_string(result->data));
12+
}
13+
rs__c_result_unit_string_free(result);
14+
15+
return io_result;
16+
}
17+
18+
extern lean_obj_res c_rs_iroh_recv(b_lean_obj_arg ticket, size_t buffer_capacity) {
19+
char const *ticket_str = lean_string_cstr(ticket);
20+
// Buffer is allocated optimistically, but if the download fails it must be freed explicitly
21+
lean_object *buffer = lean_alloc_sarray(1, 0, buffer_capacity);
22+
c_result *result = rs_iroh_recv(ticket_str, buffer, buffer_capacity);
23+
24+
lean_object *io_result;
25+
if (result->is_ok) {
26+
io_result = lean_io_result_mk_ok(buffer);
27+
}
28+
else {
29+
io_result = lean_mk_io_user_error(lean_mk_string(result->data));
30+
free(buffer);
31+
}
32+
rs__c_result_unit_string_free(result);
33+
34+
return io_result;
35+
}

lakefile.lean

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -55,11 +55,15 @@ section FFI
5555

5656
/-- Build the static lib for the Rust crate -/
5757
extern_lib ix_rs pkg := do
58+
-- Default to `--features parallel`, configured via env var
5859
let ixNoPar ← IO.getEnv "IX_NO_PAR"
60+
let ixNet ← IO.getEnv "IX_NET"
5961
let buildArgs := #["build", "--release"]
60-
let args := if ixNoPar == some "1"
61-
then buildArgs
62-
else buildArgs ++ #["--features", "parallel"]
62+
let args := match (ixNoPar, ixNet) with
63+
| (some "1", some "1") => buildArgs ++ ["--features", "net"]
64+
| (some "1", _) => buildArgs
65+
| (_, some "1") => buildArgs ++ ["--features", "parallel,net"]
66+
| _ => buildArgs ++ ["--features", "parallel"]
6367
proc { cmd := "cargo", args, cwd := pkg.dir } (quiet := true)
6468
let libName := nameToStaticLib "ix_rs"
6569
inputBinFile $ pkg.dir / "target" / "release" / libName

src/lean/ffi/_iroh.rs

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
use std::ffi::CString;
2+
3+
use crate::lean::{
4+
ffi::{CResult, c_char, to_raw},
5+
sarray::LeanSArrayObject,
6+
};
7+
8+
#[unsafe(no_mangle)]
9+
extern "C" fn rs_iroh_send(_bytes: &LeanSArrayObject) -> *const CResult {
10+
let msg = CString::new("Iroh functions not supported MacOS aarch64-darwin or when the Rust `net` feature is disabled")
11+
.expect("CString::new failure");
12+
let c_result = CResult {
13+
is_ok: true,
14+
data: msg.into_raw().cast(),
15+
};
16+
to_raw(c_result)
17+
}
18+
19+
#[unsafe(no_mangle)]
20+
extern "C" fn rs_iroh_recv(
21+
_ticket: *const c_char,
22+
_buffer: &mut LeanSArrayObject,
23+
_buffer_capacity: usize,
24+
) -> *const CResult {
25+
let msg = CString::new("Iroh functions not supported on MacOS aarch64-darwin or when the Rust `net` feature is disabled")
26+
.expect("CString::new failure");
27+
let c_result = CResult {
28+
is_ok: true,
29+
data: msg.into_raw().cast(),
30+
};
31+
to_raw(c_result)
32+
}

src/lean/ffi/iroh.rs

Lines changed: 0 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -1,23 +1,16 @@
1-
#[cfg(not(all(target_os = "macos", target_arch = "aarch64")))]
21
use anyhow::Result;
3-
#[cfg(not(all(target_os = "macos", target_arch = "aarch64")))]
42
use bytes::Bytes;
5-
#[cfg(not(all(target_os = "macos", target_arch = "aarch64")))]
63
use iroh::{Endpoint, protocol::Router};
7-
#[cfg(not(all(target_os = "macos", target_arch = "aarch64")))]
84
use iroh_blobs::{net_protocol::Blobs, ticket::BlobTicket};
9-
#[cfg(not(all(target_os = "macos", target_arch = "aarch64")))]
105
use std::error::Error;
116
use std::ffi::CString;
127

13-
#[cfg(not(all(target_os = "macos", target_arch = "aarch64")))]
148
use crate::lean::ffi::raw_to_str;
159
use crate::lean::{
1610
ffi::{CResult, c_char, to_raw},
1711
sarray::LeanSArrayObject,
1812
};
1913

20-
#[cfg(not(all(target_os = "macos", target_arch = "aarch64")))]
2114
#[unsafe(no_mangle)]
2215
extern "C" fn rs_iroh_send(bytes: &LeanSArrayObject) -> *const CResult {
2316
// Create a Tokio runtime to block on the async function
@@ -41,19 +34,6 @@ extern "C" fn rs_iroh_send(bytes: &LeanSArrayObject) -> *const CResult {
4134
to_raw(c_result)
4235
}
4336

44-
#[cfg(all(target_os = "macos", target_arch = "aarch64"))]
45-
#[unsafe(no_mangle)]
46-
extern "C" fn rs_iroh_send(_bytes: &LeanSArrayObject) -> *const CResult {
47-
let msg = CString::new("Iroh functions not supported on MacOS aarch64-darwin")
48-
.expect("CString::new failure");
49-
let c_result = CResult {
50-
is_ok: false,
51-
data: msg.into_raw().cast(),
52-
};
53-
to_raw(c_result)
54-
}
55-
56-
#[cfg(not(all(target_os = "macos", target_arch = "aarch64")))]
5737
async fn iroh_send(bytes: &[u8]) -> Result<(), Box<dyn Error>> {
5838
// Create an endpoint, it allows creating and accepting
5939
// connections in the iroh p2p world
@@ -91,7 +71,6 @@ async fn iroh_send(bytes: &[u8]) -> Result<(), Box<dyn Error>> {
9171
Ok(())
9272
}
9373

94-
#[cfg(not(all(target_os = "macos", target_arch = "aarch64")))]
9574
#[unsafe(no_mangle)]
9675
extern "C" fn rs_iroh_recv(
9776
ticket: *const c_char,
@@ -125,23 +104,6 @@ extern "C" fn rs_iroh_recv(
125104
to_raw(c_result)
126105
}
127106

128-
#[cfg(all(target_os = "macos", target_arch = "aarch64"))]
129-
#[unsafe(no_mangle)]
130-
extern "C" fn rs_iroh_recv(
131-
_ticket: *const c_char,
132-
_buffer: &mut LeanSArrayObject,
133-
_buffer_capacity: usize,
134-
) -> *const CResult {
135-
let msg = CString::new("Iroh functions not supported on MacOS aarch64-darwin")
136-
.expect("CString::new failure");
137-
let c_result = CResult {
138-
is_ok: false,
139-
data: msg.into_raw().cast(),
140-
};
141-
to_raw(c_result)
142-
}
143-
144-
#[cfg(not(all(target_os = "macos", target_arch = "aarch64")))]
145107
async fn iroh_recv(ticket: &str, buffer_capacity: usize) -> Result<Bytes, Box<dyn Error>> {
146108
// Create an endpoint, it allows creating and accepting
147109
// connections in the iroh p2p world

src/lean/ffi/mod.rs

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,9 @@
11
pub mod aiur;
22
pub mod byte_array;
3-
// pub mod iroh;
3+
#[cfg(all(feature = "net", not(all(target_os = "macos", target_arch = "aarch64"))))]
4+
pub mod iroh;
5+
#[cfg(not(feature = "net"))]
6+
pub mod _iroh;
47
pub mod keccak;
58

69
use std::ffi::{CStr, CString, c_char, c_void};

0 commit comments

Comments
 (0)