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

Code cleanup

This commit is contained in:
Leni Aniva 2024-03-06 14:37:56 -08:00
parent a7aa5ba22e
commit e0e293efc9
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
3 changed files with 6 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
build.rs
View File

@ -6,17 +6,10 @@ fn main() {
let lean_root = env::var("LEAN_ROOT").expect("Lean root must exist"); let lean_root = env::var("LEAN_ROOT").expect("Lean root must exist");
let output_path = PathBuf::from(env::var("OUT_DIR").unwrap()); let output_path = PathBuf::from(env::var("OUT_DIR").unwrap());
let input = format!("{lean_root}/include/lean/lean.h"); 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={callee_root}");
println!("cargo:rustc-link-search={lean_root}/lib/lean"); 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() let bindings = bindgen::Builder::default()
// The input header we would like to generate
// bindings for.
.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
// included header files changed. // included header files changed.
@ -30,9 +23,7 @@ fn main() {
.blocklist_function("lean_get_rc_mt_addr") .blocklist_function("lean_get_rc_mt_addr")
.opaque_type("lean_thunk_object") .opaque_type("lean_thunk_object")
.opaque_type("lean_task_object") .opaque_type("lean_task_object")
// Finish the builder and generate the bindings.
.generate() .generate()
// Unwrap the Result and panic on failure.
.expect("Unable to generate bindings"); .expect("Unable to generate bindings");
bindings bindings

13
flake.nix
View File

@ -33,6 +33,8 @@
src = ./Callee; src = ./Callee;
}; };
nativeBuildInputs = [ nativeBuildInputs = [
pkgs.rustPlatform.bindgenHook
pkgs.llvmPackages.clang
]; ];
buildInputs = [ buildInputs = [
leanPkgs.lean-all leanPkgs.lean-all
@ -46,10 +48,6 @@
}) { }) {
inherit pkgs; inherit pkgs;
defaultCrateOverrides = pkgs.defaultCrateOverrides // { defaultCrateOverrides = pkgs.defaultCrateOverrides // {
bindgen = attrs: {
inherit nativeBuildInputs;
buildInputs = nativeBuildInputs;
};
caller = attrs: { caller = attrs: {
inherit nativeBuildInputs; inherit nativeBuildInputs;
inherit buildInputs; inherit buildInputs;
@ -67,12 +65,9 @@
}; };
devShells.default = pkgs.mkShell { devShells.default = pkgs.mkShell {
CALLEE_PATH = callee.sharedLib; CALLEE_PATH = callee.sharedLib;
LIBCLANG_PATH = "${pkgs.llvmPackages.libclang.lib}/lib";
LEAN_ROOT = leanPkgs.lean-all; LEAN_ROOT = leanPkgs.lean-all;
nativeBuildInputs = [ inherit nativeBuildInputs;
pkgs.rustPlatform.bindgenHook buildInputs = buildInputs ++ [
];
buildInputs = buildInputs ++ nativeBuildInputs ++ [
pkgs.rustc pkgs.rustc
# This is not needed for compilation. It is here for diagnostic purposes # This is not needed for compilation. It is here for diagnostic purposes
pkgs.rust-bindgen pkgs.rust-bindgen

6
src/main.rs
View File

@ -2,8 +2,7 @@
#[allow(non_camel_case_types)] #[allow(non_camel_case_types)]
#[allow(non_snake_case)] #[allow(non_snake_case)]
#[allow(dead_code)] #[allow(dead_code)]
mod lean mod lean {
{
include!(concat!(env!("OUT_DIR"), "/lean.rs")); include!(concat!(env!("OUT_DIR"), "/lean.rs"));
#[link(name = "leanshared")] #[link(name = "leanshared")]
@ -18,8 +17,7 @@ mod lean
pub fn my_function(s: lean_obj_arg) -> lean_obj_arg; pub fn my_function(s: lean_obj_arg) -> lean_obj_arg;
} }
} }
fn main() fn main() {
{
unsafe { unsafe {
lean::lean_initialize_runtime_module(); lean::lean_initialize_runtime_module();
lean::lean_initialize(); lean::lean_initialize();