diff --git a/build.rs b/build.rs index 1ea6ddc..5c9234e 100644 --- a/build.rs +++ b/build.rs @@ -9,6 +9,9 @@ fn main() { println!("cargo:rustc-link-search={callee_root}"); 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() .header(&input) // 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 // function .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, // so they are blocklisted. The types which use `_Atomic` are treated as // opaque. @@ -30,11 +35,7 @@ fn main() { .write_to_file(output_path.join("lean.rs")) .expect("Couldn't write bindings!"); - let extern_src_path = env::temp_dir().join("bindgen").join("extern.c"); - 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"); + let extern_obj_path = bindgen_dir.join("leanextern.o"); // Compile the generated wrappers into an object file. 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"))] let lib_output = std::process::Command::new("ar") .arg("rcs") - .arg(output_path.join(&lib_path)) + .arg(bindgen_dir.join("libleanextern.a")) .arg(&extern_obj_path) - .output() - .unwrap(); + .output().unwrap(); #[cfg(target_os = "windows")] let lib_output = std::process::Command::new("LIB") - .arg(obj_path) + .arg(&extern_obj_path) .arg(format!( "/OUT:{}", - output_path.join("libextern.lib").display() + bindgen_dir.join("libleanextern.lib").display() )) - .output() - .unwrap(); + .output().unwrap(); if !lib_output.status.success() { panic!( "Could not emit library file:\n{}", @@ -81,6 +79,6 @@ fn main() { } // Statically link against the generated lib - println!("cargo:rustc-link-search={}", output_path.display()); - println!("cargo:rustc-link-lib=static=extern"); + println!("cargo:rustc-link-search={}", bindgen_dir.display()); + println!("cargo:rustc-link-lib=static=leanextern"); } diff --git a/src/main.rs b/src/main.rs index 5beb1d1..a8e1f39 100644 --- a/src/main.rs +++ b/src/main.rs @@ -18,9 +18,9 @@ mod callee { #[link(name = "Callee")] extern "C" { - #[allow(non_snake_case)] - pub fn initialize_Callee(builtin: u8, world: *mut lean_object) -> *mut lean_object; - pub fn my_function(s: lean_obj_arg) -> lean_obj_arg; + #[link_name = "initialize_Callee"] + pub fn initialize(builtin: u8, world: lean_obj_arg) -> lean_obj_res; + pub fn my_function(s: lean_obj_arg) -> lean_obj_res; } } fn main() { @@ -28,7 +28,7 @@ fn main() { lean::lean_initialize_runtime_module(); lean::lean_initialize(); 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) { lean::lean_dec_ref(res); } else {