Compare commits

..

No commits in common. "main" and "data-structures" have entirely different histories.

3 changed files with 18 additions and 38 deletions

View File

@ -17,7 +17,3 @@ def think (s: String): Think :=
Think.Success (s.drop 1)
else
Think.Failure s.length
@[export print_in_upper]
def print_in_upper (s: String): IO Unit := do
IO.println s.toUpper

View File

@ -9,9 +9,6 @@ fn main() {
println!("cargo:rustc-link-search={callee_root}");
println!("cargo:rustc-link-search={lean_root}/lib/lean");
let bindgen_dir = env::temp_dir().join("bindgen");
let extern_src_path = bindgen_dir.join("leanextern.c");
let bindings = bindgen::Builder::default()
.header(&input)
// Tell cargo to invalidate the built crate whenever any of the
@ -20,8 +17,6 @@ fn main() {
// The following is specific to `lean.h`: There are a lot of static
// function
.wrap_static_fns(true)
.wrap_static_fns_suffix("__leanextern")
.wrap_static_fns_path(&extern_src_path)
// but some functions use `_Atomic(int)` types that bindgen cannot handle,
// so they are blocklisted. The types which use `_Atomic` are treated as
// opaque.
@ -35,7 +30,11 @@ fn main() {
.write_to_file(output_path.join("lean.rs"))
.expect("Couldn't write bindings!");
let extern_obj_path = bindgen_dir.join("leanextern.o");
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");
// Compile the generated wrappers into an object file.
let clang_output = std::process::Command::new("clang")
@ -57,20 +56,23 @@ fn main() {
);
}
// Turn the object file into a static library
#[cfg(not(target_os = "windows"))]
let lib_output = std::process::Command::new("ar")
.arg("rcs")
.arg(bindgen_dir.join("libleanextern.a"))
.arg(output_path.join(&lib_path))
.arg(&extern_obj_path)
.output().unwrap();
.output()
.unwrap();
#[cfg(target_os = "windows")]
let lib_output = std::process::Command::new("LIB")
.arg(&extern_obj_path)
.arg(obj_path)
.arg(format!(
"/OUT:{}",
bindgen_dir.join("libleanextern.lib").display()
output_path.join("libextern.lib").display()
))
.output().unwrap();
.output()
.unwrap();
if !lib_output.status.success() {
panic!(
"Could not emit library file:\n{}",
@ -79,6 +81,6 @@ fn main() {
}
// Statically link against the generated lib
println!("cargo:rustc-link-search={}", bindgen_dir.display());
println!("cargo:rustc-link-lib=static=leanextern");
println!("cargo:rustc-link-search={}", output_path.display());
println!("cargo:rustc-link-lib=static=extern");
}

View File

@ -18,12 +18,11 @@ mod callee {
#[link(name = "Callee")]
extern "C" {
#[link_name = "initialize_Callee"]
pub fn initialize(builtin: u8, world: lean_obj_arg) -> lean_obj_res;
#[allow(non_snake_case)]
pub fn initialize_Callee(builtin: u8, world: lean_obj_arg) -> lean_obj_res;
pub fn my_function(s: lean_obj_arg) -> lean_obj_res;
pub fn stylize(s: lean_obj_arg) -> lean_obj_res;
pub fn think(s: lean_obj_arg) -> lean_obj_res;
pub fn print_in_upper(s: lean_obj_arg, world: lean_obj_arg) -> lean_obj_res;
}
}
@ -32,7 +31,7 @@ fn initialize() {
lean::lean_initialize_runtime_module();
lean::lean_initialize();
let builtin: u8 = 1;
let res = callee::initialize(builtin, lean::lean_io_mk_world());
let res = callee::initialize_Callee(builtin, lean::lean_io_mk_world());
if lean::lean_io_result_is_ok(res) {
lean::lean_dec_ref(res);
} else {
@ -119,22 +118,6 @@ fn call_think(s: &str) -> Result<String, usize> {
}
}
fn call_print_in_upper()
{
let c_str = std::ffi::CString::new("caller").unwrap();
unsafe {
let native_str = lean::lean_mk_string(c_str.as_ptr());
let res = callee::print_in_upper(native_str, lean::lean_io_mk_world());
if lean::lean_io_result_is_ok(res) {
lean::lean_dec_ref(res);
} else {
lean::lean_io_result_show_error(res);
lean::lean_dec(res);
panic!("IO Monad execution failed");
}
};
}
fn main() {
initialize();
println!("Lean initialization complete!");
@ -144,5 +127,4 @@ fn main() {
assert_eq!(call_think("Stanford"), Ok("tanford".to_string()));
assert_eq!(call_think("Else"), Err(4));
call_print_in_upper();
}