Fix linker error on linux
This commit is contained in:
parent
4acebb508f
commit
a7aa5ba22e
4
build.rs
4
build.rs
|
@ -1,8 +1,6 @@
|
||||||
use std::env;
|
use std::env;
|
||||||
use std::path::PathBuf;
|
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 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");
|
||||||
|
@ -12,8 +10,6 @@ fn main() {
|
||||||
println!("cargo:rerun-if-changed={input}");
|
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=leanshared");
|
|
||||||
|
|
||||||
// The bindgen::Builder is the main entry point
|
// The bindgen::Builder is the main entry point
|
||||||
// to bindgen, and lets you build up options for
|
// to bindgen, and lets you build up options for
|
||||||
|
|
|
@ -6,7 +6,7 @@ mod lean
|
||||||
{
|
{
|
||||||
include!(concat!(env!("OUT_DIR"), "/lean.rs"));
|
include!(concat!(env!("OUT_DIR"), "/lean.rs"));
|
||||||
|
|
||||||
#[link(name = "lean")]
|
#[link(name = "leanshared")]
|
||||||
extern "C" {
|
extern "C" {
|
||||||
pub fn lean_initialize_runtime_module();
|
pub fn lean_initialize_runtime_module();
|
||||||
pub fn lean_initialize();
|
pub fn lean_initialize();
|
||||||
|
|
Loading…
Reference in New Issue