From 4acebb508f7df4f97e73ac50058d2afb5b499618 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 6 Mar 2024 13:03:40 -0800 Subject: [PATCH] Add bindgen hook; code cleanup --- .gitignore | 5 +++++ Cargo.lock | 18 +++++++++--------- Cargo.toml | 2 +- build.rs | 21 +++++++++++---------- flake.lock | 19 ++++++++++++++++++- flake.nix | 37 +++++++++++++++++++++++++++++++++++-- 6 files changed, 79 insertions(+), 23 deletions(-) diff --git a/.gitignore b/.gitignore index 01fc188..966e031 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,8 @@ .* *.olean !.gitignore + +# rust output +/target +# nix output +/result diff --git a/Cargo.lock b/Cargo.lock index 56b409a..ffb71c6 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -51,6 +51,13 @@ version = "2.4.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ed570934406eb16438a4e976b1b4500774099c13b8cb96eec99f620f05090ddf" +[[package]] +name = "caller" +version = "0.1.0" +dependencies = [ + "bindgen", +] + [[package]] name = "cexpr" version = "0.6.0" @@ -137,9 +144,9 @@ checksum = "9c198f91728a82281a64e1f4f9eeb25d82cb32a5de251c6bd1b5154d63a8e7bd" [[package]] name = "libloading" -version = "0.8.2" +version = "0.8.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2caa5afb8bf9f3a2652760ce7d4f62d21c4d5a423e68466fca30df82f2330164" +checksum = "0c2a198fb6b0eada2a8df47933734e6d35d350665a33a3593d7164fa52c75c19" dependencies = [ "cfg-if", "windows-targets", @@ -248,13 +255,6 @@ version = "1.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "08d43f7aa6b08d49f382cde6a7982047c3426db949b1424bc4b7ec9ae12c6ce2" -[[package]] -name = "rustcalllean" -version = "0.1.0" -dependencies = [ - "bindgen", -] - [[package]] name = "rustix" version = "0.38.31" diff --git a/Cargo.toml b/Cargo.toml index e46ce78..4ff856f 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,5 +1,5 @@ [package] -name = "rustcalllean" +name = "caller" description = "Rust calls Lean" authors = ["Leni Aniva"] publish = false diff --git a/build.rs b/build.rs index 0af6f66..fb6cc0d 100644 --- a/build.rs +++ b/build.rs @@ -3,15 +3,16 @@ use std::path::PathBuf; const CALLEE_NAME: &str = "Callee"; -fn main() -{ +fn main() { let callee_root = env::var("CALLEE_PATH").expect("Callee path variable must be available"); 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"); println!("cargo:rustc-link-lib={CALLEE_NAME}"); - //println!("cargo:rustc-link-lib=Init_shared"); println!("cargo:rustc-link-lib=leanshared"); // The bindgen::Builder is the main entry point @@ -38,15 +39,13 @@ fn main() // Unwrap the Result and panic on failure. .expect("Unable to generate bindings"); - let extern_src_path = std::env::temp_dir().join("bindgen").join("extern.c"); - let extern_obj_path = std::env::temp_dir().join("bindgen").join("extern.o"); - let output_path = PathBuf::from(std::env::var("OUT_DIR").unwrap()); - // Write the bindings to the $OUT_DIR/bindings.rs file. - let out_path = PathBuf::from(env::var("OUT_DIR").unwrap()); bindings - .write_to_file(out_path.join("lean.rs")) + .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"); @@ -59,6 +58,8 @@ fn main() .arg(&extern_src_path) .arg("-include") .arg(&input) + .arg("-I") + .arg(format!("{lean_root}/include")) .output() .unwrap(); if !clang_output.status.success() { @@ -81,7 +82,7 @@ fn main() .arg(obj_path) .arg(format!( "/OUT:{}", - out_dir_path.join("libextern.lib").display() + output_path.join("libextern.lib").display() )) .output() .unwrap(); diff --git a/flake.lock b/flake.lock index 0475ae7..26504e0 100644 --- a/flake.lock +++ b/flake.lock @@ -193,7 +193,24 @@ "inputs": { "flake-parts": "flake-parts", "lean": "lean", - "nixpkgs": "nixpkgs_3" + "nixpkgs": "nixpkgs_3", + "rust-crate2nix": "rust-crate2nix" + } + }, + "rust-crate2nix": { + "flake": false, + "locked": { + "lastModified": 1708135620, + "narHash": "sha256-O8FgwfMR8LgJjIX1RjEmme67sLscMUlmkJLlkb83RyY=", + "owner": "kolloch", + "repo": "crate2nix", + "rev": "7eb26c517fa5b4b2056cc5e2e288e0117306e600", + "type": "github" + }, + "original": { + "owner": "kolloch", + "repo": "crate2nix", + "type": "github" } } }, diff --git a/flake.nix b/flake.nix index bc67e74..e8946c4 100644 --- a/flake.nix +++ b/flake.nix @@ -5,6 +5,10 @@ nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable"; flake-parts.url = "github:hercules-ci/flake-parts"; lean.url = "github:leanprover/lean4?ref=v4.1.0"; + rust-crate2nix = { + url = "github:kolloch/crate2nix"; + flake = false; + }; }; outputs = inputs @ { @@ -12,6 +16,7 @@ nixpkgs, flake-parts, lean, + rust-crate2nix, ... } : flake-parts.lib.mkFlake { inherit inputs; } { flake = { @@ -27,19 +32,47 @@ roots = [ "Callee" ]; src = ./Callee; }; - common = [ + nativeBuildInputs = [ + ]; + buildInputs = [ leanPkgs.lean-all pkgs.libiconv ]; + caller = let + crateTools = pkgs.callPackage "${rust-crate2nix}/tools.nix" { inherit pkgs; }; + in import (crateTools.generatedCargoNix { + name = "caller"; + src = ./.; + }) { + inherit pkgs; + defaultCrateOverrides = pkgs.defaultCrateOverrides // { + bindgen = attrs: { + inherit nativeBuildInputs; + buildInputs = nativeBuildInputs; + }; + caller = attrs: { + inherit nativeBuildInputs; + inherit buildInputs; + CALLEE_PATH = callee.sharedLib; + LEAN_ROOT = leanPkgs.lean-all; + }; + }; + }; in rec { packages = { inherit (leanPkgs) lean iTree stage1 lean-all; callee = callee.sharedLib; + caller = caller.rootCrate.build; + bindgen = pkgs.rustPlatform.bindgenHook; }; devShells.default = pkgs.mkShell { CALLEE_PATH = callee.sharedLib; + LIBCLANG_PATH = "${pkgs.llvmPackages.libclang.lib}/lib"; LEAN_ROOT = leanPkgs.lean-all; - buildInputs = common ++ [ + nativeBuildInputs = [ + pkgs.rustPlatform.bindgenHook + ]; + buildInputs = buildInputs ++ nativeBuildInputs ++ [ pkgs.rustc # This is not needed for compilation. It is here for diagnostic purposes pkgs.rust-bindgen