Add bindgen hook; code cleanup
This commit is contained in:
parent
c0f00af744
commit
4acebb508f
|
@ -1,3 +1,8 @@
|
||||||
.*
|
.*
|
||||||
*.olean
|
*.olean
|
||||||
!.gitignore
|
!.gitignore
|
||||||
|
|
||||||
|
# rust output
|
||||||
|
/target
|
||||||
|
# nix output
|
||||||
|
/result
|
||||||
|
|
|
@ -51,6 +51,13 @@ version = "2.4.2"
|
||||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
checksum = "ed570934406eb16438a4e976b1b4500774099c13b8cb96eec99f620f05090ddf"
|
checksum = "ed570934406eb16438a4e976b1b4500774099c13b8cb96eec99f620f05090ddf"
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "caller"
|
||||||
|
version = "0.1.0"
|
||||||
|
dependencies = [
|
||||||
|
"bindgen",
|
||||||
|
]
|
||||||
|
|
||||||
[[package]]
|
[[package]]
|
||||||
name = "cexpr"
|
name = "cexpr"
|
||||||
version = "0.6.0"
|
version = "0.6.0"
|
||||||
|
@ -137,9 +144,9 @@ checksum = "9c198f91728a82281a64e1f4f9eeb25d82cb32a5de251c6bd1b5154d63a8e7bd"
|
||||||
|
|
||||||
[[package]]
|
[[package]]
|
||||||
name = "libloading"
|
name = "libloading"
|
||||||
version = "0.8.2"
|
version = "0.8.3"
|
||||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
checksum = "2caa5afb8bf9f3a2652760ce7d4f62d21c4d5a423e68466fca30df82f2330164"
|
checksum = "0c2a198fb6b0eada2a8df47933734e6d35d350665a33a3593d7164fa52c75c19"
|
||||||
dependencies = [
|
dependencies = [
|
||||||
"cfg-if",
|
"cfg-if",
|
||||||
"windows-targets",
|
"windows-targets",
|
||||||
|
@ -248,13 +255,6 @@ version = "1.1.0"
|
||||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
checksum = "08d43f7aa6b08d49f382cde6a7982047c3426db949b1424bc4b7ec9ae12c6ce2"
|
checksum = "08d43f7aa6b08d49f382cde6a7982047c3426db949b1424bc4b7ec9ae12c6ce2"
|
||||||
|
|
||||||
[[package]]
|
|
||||||
name = "rustcalllean"
|
|
||||||
version = "0.1.0"
|
|
||||||
dependencies = [
|
|
||||||
"bindgen",
|
|
||||||
]
|
|
||||||
|
|
||||||
[[package]]
|
[[package]]
|
||||||
name = "rustix"
|
name = "rustix"
|
||||||
version = "0.38.31"
|
version = "0.38.31"
|
||||||
|
|
|
@ -1,5 +1,5 @@
|
||||||
[package]
|
[package]
|
||||||
name = "rustcalllean"
|
name = "caller"
|
||||||
description = "Rust calls Lean"
|
description = "Rust calls Lean"
|
||||||
authors = ["Leni Aniva"]
|
authors = ["Leni Aniva"]
|
||||||
publish = false
|
publish = false
|
||||||
|
|
21
build.rs
21
build.rs
|
@ -3,15 +3,16 @@ use std::path::PathBuf;
|
||||||
|
|
||||||
const CALLEE_NAME: &str = "Callee";
|
const CALLEE_NAME: &str = "Callee";
|
||||||
|
|
||||||
fn main()
|
fn main() {
|
||||||
{
|
|
||||||
let callee_root = env::var("CALLEE_PATH").expect("Callee path variable must be available");
|
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 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");
|
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");
|
||||||
println!("cargo:rustc-link-lib={CALLEE_NAME}");
|
println!("cargo:rustc-link-lib={CALLEE_NAME}");
|
||||||
//println!("cargo:rustc-link-lib=Init_shared");
|
|
||||||
println!("cargo:rustc-link-lib=leanshared");
|
println!("cargo:rustc-link-lib=leanshared");
|
||||||
|
|
||||||
// The bindgen::Builder is the main entry point
|
// The bindgen::Builder is the main entry point
|
||||||
|
@ -38,15 +39,13 @@ fn main()
|
||||||
// Unwrap the Result and panic on failure.
|
// Unwrap the Result and panic on failure.
|
||||||
.expect("Unable to generate bindings");
|
.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
|
bindings
|
||||||
.write_to_file(out_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 = env::temp_dir().join("bindgen").join("extern.o");
|
||||||
|
|
||||||
// This is the path to the static library file.
|
// This is the path to the static library file.
|
||||||
let lib_path = output_path.join("libextern.a");
|
let lib_path = output_path.join("libextern.a");
|
||||||
|
|
||||||
|
@ -59,6 +58,8 @@ fn main()
|
||||||
.arg(&extern_src_path)
|
.arg(&extern_src_path)
|
||||||
.arg("-include")
|
.arg("-include")
|
||||||
.arg(&input)
|
.arg(&input)
|
||||||
|
.arg("-I")
|
||||||
|
.arg(format!("{lean_root}/include"))
|
||||||
.output()
|
.output()
|
||||||
.unwrap();
|
.unwrap();
|
||||||
if !clang_output.status.success() {
|
if !clang_output.status.success() {
|
||||||
|
@ -81,7 +82,7 @@ fn main()
|
||||||
.arg(obj_path)
|
.arg(obj_path)
|
||||||
.arg(format!(
|
.arg(format!(
|
||||||
"/OUT:{}",
|
"/OUT:{}",
|
||||||
out_dir_path.join("libextern.lib").display()
|
output_path.join("libextern.lib").display()
|
||||||
))
|
))
|
||||||
.output()
|
.output()
|
||||||
.unwrap();
|
.unwrap();
|
||||||
|
|
19
flake.lock
19
flake.lock
|
@ -193,7 +193,24 @@
|
||||||
"inputs": {
|
"inputs": {
|
||||||
"flake-parts": "flake-parts",
|
"flake-parts": "flake-parts",
|
||||||
"lean": "lean",
|
"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"
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
},
|
},
|
||||||
|
|
37
flake.nix
37
flake.nix
|
@ -5,6 +5,10 @@
|
||||||
nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
|
nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
|
||||||
flake-parts.url = "github:hercules-ci/flake-parts";
|
flake-parts.url = "github:hercules-ci/flake-parts";
|
||||||
lean.url = "github:leanprover/lean4?ref=v4.1.0";
|
lean.url = "github:leanprover/lean4?ref=v4.1.0";
|
||||||
|
rust-crate2nix = {
|
||||||
|
url = "github:kolloch/crate2nix";
|
||||||
|
flake = false;
|
||||||
|
};
|
||||||
};
|
};
|
||||||
|
|
||||||
outputs = inputs @ {
|
outputs = inputs @ {
|
||||||
|
@ -12,6 +16,7 @@
|
||||||
nixpkgs,
|
nixpkgs,
|
||||||
flake-parts,
|
flake-parts,
|
||||||
lean,
|
lean,
|
||||||
|
rust-crate2nix,
|
||||||
...
|
...
|
||||||
} : flake-parts.lib.mkFlake { inherit inputs; } {
|
} : flake-parts.lib.mkFlake { inherit inputs; } {
|
||||||
flake = {
|
flake = {
|
||||||
|
@ -27,19 +32,47 @@
|
||||||
roots = [ "Callee" ];
|
roots = [ "Callee" ];
|
||||||
src = ./Callee;
|
src = ./Callee;
|
||||||
};
|
};
|
||||||
common = [
|
nativeBuildInputs = [
|
||||||
|
];
|
||||||
|
buildInputs = [
|
||||||
leanPkgs.lean-all
|
leanPkgs.lean-all
|
||||||
pkgs.libiconv
|
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 {
|
in rec {
|
||||||
packages = {
|
packages = {
|
||||||
inherit (leanPkgs) lean iTree stage1 lean-all;
|
inherit (leanPkgs) lean iTree stage1 lean-all;
|
||||||
callee = callee.sharedLib;
|
callee = callee.sharedLib;
|
||||||
|
caller = caller.rootCrate.build;
|
||||||
|
bindgen = pkgs.rustPlatform.bindgenHook;
|
||||||
};
|
};
|
||||||
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;
|
||||||
buildInputs = common ++ [
|
nativeBuildInputs = [
|
||||||
|
pkgs.rustPlatform.bindgenHook
|
||||||
|
];
|
||||||
|
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
|
||||||
|
|
Loading…
Reference in New Issue