Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
23 changes: 19 additions & 4 deletions lakefile.lean
Original file line number Diff line number Diff line change
Expand Up @@ -29,12 +29,27 @@ end Tests

section FFI

/- Build the static lib for the Rust crate -/
/-- Build the static lib for the Rust crate -/
extern_lib ix_rs pkg := do
proc { cmd := "cargo", args := #["build", "--release"], cwd := pkg.dir }
let name := nameToStaticLib "ix_rs"
let srcPath := pkg.dir / "target" / "release" / name
return pure srcPath
let libName := nameToStaticLib "ix_rs"
let libPath := pkg.dir / "target" / "release" / libName

-- If the static lib has changed, remove cached binaries for recompilation
let libBytes ← IO.FS.readBinFile libPath
let libHash := toString $ hash libBytes
let libHashPath := pkg.nativeLibDir / (libName ++ ".hash")
let shouldCleanBinaries ←
if ← pkg.binDir.pathExists then
if ← libHashPath.pathExists then
let cachedHash ← IO.FS.readFile libHashPath
pure $ libHash != cachedHash -- Clean up in case of hash mismatch
else pure true -- No hash file
else pure false -- No files to remove
if shouldCleanBinaries then IO.FS.removeDirAll pkg.binDir
IO.FS.writeFile libHashPath libHash

return pure libPath

end FFI

Expand Down
7 changes: 2 additions & 5 deletions src/lean/ffi.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,10 +9,7 @@ extern "C" fn add_u32s(a: u32, b: u32) -> u32 {
/// `@& ByteArray → UInt8`
#[no_mangle]
extern "C" fn byte_array_sum(o: &LeanSArrayObject) -> u8 {
o.m_data
.slice(o.m_size)
.iter()
.fold(0, |acc, x| x.overflowing_add(acc).0)
o.data().iter().fold(0, |acc, x| x.overflowing_add(acc).0)
}

/// `USize → ByteArray`
Expand All @@ -24,5 +21,5 @@ extern "C" fn byte_array_zeros(len: usize) -> *const LeanSArrayObject {
/// `@& ByteArray → @& ByteArray → Bool`
#[no_mangle]
extern "C" fn byte_array_beq(a: &LeanSArrayObject, b: &LeanSArrayObject) -> bool {
a.slice() == b.slice()
a.data() == b.data()
}
5 changes: 3 additions & 2 deletions src/lean/sarray.rs
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,8 @@ pub struct LeanSArrayObject {
}

impl LeanSArrayObject {
pub fn slice(&self) -> &[u8] {
#[inline]
pub fn data(&self) -> &[u8] {
self.m_data.slice(self.m_size)
}

Expand All @@ -34,7 +35,7 @@ impl LeanSArrayObject {
size_of::<LeanSArrayObject>() + len,
align_of::<LeanSArrayObject>(),
)
.unwrap();
.expect("Couldn't compute the memory layout");

let ptr = unsafe { alloc(layout) as *mut LeanSArrayObject };
if ptr.is_null() {
Expand Down