diff --git a/build.rs b/build.rs index 20dc76c..1ea6ddc 100644 --- a/build.rs +++ b/build.rs @@ -6,17 +6,10 @@ fn main() { let lean_root = env::var("LEAN_ROOT").expect("Lean root must exist"); let output_path = PathBuf::from(env::var("OUT_DIR").unwrap()); let input = format!("{lean_root}/include/lean/lean.h"); - println!("cargo:rerun-if-changed=build.rs"); - println!("cargo:rerun-if-changed={input}"); println!("cargo:rustc-link-search={callee_root}"); println!("cargo:rustc-link-search={lean_root}/lib/lean"); - // The bindgen::Builder is the main entry point - // to bindgen, and lets you build up options for - // the resulting bindings. let bindings = bindgen::Builder::default() - // The input header we would like to generate - // bindings for. .header(&input) // Tell cargo to invalidate the built crate whenever any of the // included header files changed. @@ -30,9 +23,7 @@ fn main() { .blocklist_function("lean_get_rc_mt_addr") .opaque_type("lean_thunk_object") .opaque_type("lean_task_object") - // Finish the builder and generate the bindings. .generate() - // Unwrap the Result and panic on failure. .expect("Unable to generate bindings"); bindings diff --git a/flake.nix b/flake.nix index e8946c4..2d2e05e 100644 --- a/flake.nix +++ b/flake.nix @@ -33,6 +33,8 @@ src = ./Callee; }; nativeBuildInputs = [ + pkgs.rustPlatform.bindgenHook + pkgs.llvmPackages.clang ]; buildInputs = [ leanPkgs.lean-all @@ -46,10 +48,6 @@ }) { inherit pkgs; defaultCrateOverrides = pkgs.defaultCrateOverrides // { - bindgen = attrs: { - inherit nativeBuildInputs; - buildInputs = nativeBuildInputs; - }; caller = attrs: { inherit nativeBuildInputs; inherit buildInputs; @@ -67,12 +65,9 @@ }; devShells.default = pkgs.mkShell { CALLEE_PATH = callee.sharedLib; - LIBCLANG_PATH = "${pkgs.llvmPackages.libclang.lib}/lib"; LEAN_ROOT = leanPkgs.lean-all; - nativeBuildInputs = [ - pkgs.rustPlatform.bindgenHook - ]; - buildInputs = buildInputs ++ nativeBuildInputs ++ [ + inherit nativeBuildInputs; + buildInputs = buildInputs ++ [ pkgs.rustc # This is not needed for compilation. It is here for diagnostic purposes pkgs.rust-bindgen diff --git a/src/main.rs b/src/main.rs index 7e29d83..e8ec002 100644 --- a/src/main.rs +++ b/src/main.rs @@ -2,8 +2,7 @@ #[allow(non_camel_case_types)] #[allow(non_snake_case)] #[allow(dead_code)] -mod lean -{ +mod lean { include!(concat!(env!("OUT_DIR"), "/lean.rs")); #[link(name = "leanshared")] @@ -18,8 +17,7 @@ mod lean pub fn my_function(s: lean_obj_arg) -> lean_obj_arg; } } -fn main() -{ +fn main() { unsafe { lean::lean_initialize_runtime_module(); lean::lean_initialize();