aniva
/
RustCallLean
1
0
Fork 0
Code Issues Pull Requests 1 Packages Projects Releases Wiki Activity

Tidying up the code

main
Leni Aniva 2024-03-09 15:59:00 -08:00
parent 1f8807a809
commit 6e1af2794d
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
2 changed files with 17 additions and 19 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
build.rs
View File

@ -9,6 +9,9 @@ fn main() {
println!("cargo:rustc-link-search={callee_root}"); println!("cargo:rustc-link-search={callee_root}");
println!("cargo:rustc-link-search={lean_root}/lib/lean"); println!("cargo:rustc-link-search={lean_root}/lib/lean");
let bindgen_dir = env::temp_dir().join("bindgen");
let extern_src_path = bindgen_dir.join("leanextern.c");
let bindings = bindgen::Builder::default() let bindings = bindgen::Builder::default()
.header(&input) .header(&input)
// Tell cargo to invalidate the built crate whenever any of the // Tell cargo to invalidate the built crate whenever any of the
@ -17,6 +20,8 @@ fn main() {
// The following is specific to `lean.h`: There are a lot of static // The following is specific to `lean.h`: There are a lot of static
// function // function
.wrap_static_fns(true) .wrap_static_fns(true)
.wrap_static_fns_suffix("__leanextern")
.wrap_static_fns_path(&extern_src_path)
// but some functions use `_Atomic(int)` types that bindgen cannot handle, // but some functions use `_Atomic(int)` types that bindgen cannot handle,
// so they are blocklisted. The types which use `_Atomic` are treated as // so they are blocklisted. The types which use `_Atomic` are treated as
// opaque. // opaque.
@ -30,11 +35,7 @@ fn main() {
.write_to_file(output_path.join("lean.rs")) .write_to_file(output_path.join("lean.rs"))
.expect("Couldn't write bindings!"); .expect("Couldn't write bindings!");
let extern_src_path = env::temp_dir().join("bindgen").join("extern.c"); let extern_obj_path = bindgen_dir.join("leanextern.o");
let extern_obj_path = env::temp_dir().join("bindgen").join("extern.o");
// This is the path to the static library file.
let lib_path = output_path.join("libextern.a");
// Compile the generated wrappers into an object file. // Compile the generated wrappers into an object file.
let clang_output = std::process::Command::new("clang") let clang_output = std::process::Command::new("clang")
@ -56,23 +57,20 @@ fn main() {
); );
} }
// Turn the object file into a static library
#[cfg(not(target_os = "windows"))] #[cfg(not(target_os = "windows"))]
let lib_output = std::process::Command::new("ar") let lib_output = std::process::Command::new("ar")
.arg("rcs") .arg("rcs")
.arg(output_path.join(&lib_path)) .arg(bindgen_dir.join("libleanextern.a"))
.arg(&extern_obj_path) .arg(&extern_obj_path)
.output() .output().unwrap();
.unwrap();
#[cfg(target_os = "windows")] #[cfg(target_os = "windows")]
let lib_output = std::process::Command::new("LIB") let lib_output = std::process::Command::new("LIB")
.arg(obj_path) .arg(&extern_obj_path)
.arg(format!( .arg(format!(
"/OUT:{}", "/OUT:{}",
output_path.join("libextern.lib").display() bindgen_dir.join("libleanextern.lib").display()
)) ))
.output() .output().unwrap();
.unwrap();
if !lib_output.status.success() { if !lib_output.status.success() {
panic!( panic!(
"Could not emit library file:\n{}", "Could not emit library file:\n{}",
@ -81,6 +79,6 @@ fn main() {
} }
// Statically link against the generated lib // Statically link against the generated lib
println!("cargo:rustc-link-search={}", output_path.display()); println!("cargo:rustc-link-search={}", bindgen_dir.display());
println!("cargo:rustc-link-lib=static=extern"); println!("cargo:rustc-link-lib=static=leanextern");
} }

8
src/main.rs
View File

@ -18,9 +18,9 @@ mod callee {
#[link(name = "Callee")] #[link(name = "Callee")]
extern "C" { extern "C" {
#[allow(non_snake_case)] #[link_name = "initialize_Callee"]
pub fn initialize_Callee(builtin: u8, world: *mut lean_object) -> *mut lean_object; pub fn initialize(builtin: u8, world: lean_obj_arg) -> lean_obj_res;
pub fn my_function(s: lean_obj_arg) -> lean_obj_arg; pub fn my_function(s: lean_obj_arg) -> lean_obj_res;
} }
} }
fn main() { fn main() {
@ -28,7 +28,7 @@ fn main() {
lean::lean_initialize_runtime_module(); lean::lean_initialize_runtime_module();
lean::lean_initialize(); lean::lean_initialize();
let builtin: u8 = 1; let builtin: u8 = 1;
let res = callee::initialize_Callee(builtin, lean::lean_io_mk_world()); let res = callee::initialize(builtin, lean::lean_io_mk_world());
if lean::lean_io_result_is_ok(res) { if lean::lean_io_result_is_ok(res) {
lean::lean_dec_ref(res); lean::lean_dec_ref(res);
} else { } else {