diff --git a/cedar-drt/Cargo.toml b/cedar-drt/Cargo.toml index b6a08f827..b6f20e9ab 100644 --- a/cedar-drt/Cargo.toml +++ b/cedar-drt/Cargo.toml @@ -13,7 +13,7 @@ cedar-policy-core = { path = "../cedar/cedar-policy-core", version = "4.*", feat cedar-policy-validator = { path = "../cedar/cedar-policy-validator", version = "4.*", features = ["arbitrary"] } cedar-policy-formatter = { path = "../cedar/cedar-policy-formatter", version = "4.*" } cedar-testing = { path = "../cedar/cedar-testing", version = "4.*" } -lean-sys = { version = "0.0.5", features = ["small_allocator"], default-features = false } +lean-sys = { version = "0.0.7", features = ["small_allocator"], default-features = false } miette = "7.1.0" serde = { version = "1.0", features = ["derive"] } serde_json = "1.0" diff --git a/cedar-drt/src/lean_impl.rs b/cedar-drt/src/lean_impl.rs index dbea58ee9..b53b1aced 100644 --- a/cedar-drt/src/lean_impl.rs +++ b/cedar-drt/src/lean_impl.rs @@ -34,10 +34,10 @@ use cedar_testing::cedar_test_impl::*; pub use lean_sys::init::lean_initialize; pub use lean_sys::lean_object; pub use lean_sys::string::lean_mk_string; -use lean_sys::{lean_dec, lean_dec_ref, lean_io_result_is_ok, lean_io_result_show_error}; use lean_sys::{ - lean_initialize_runtime_module_locked, lean_io_mark_end_initialization, lean_io_mk_world, - lean_string_cstr, + lean_dec, lean_dec_ref, lean_finalize_thread, lean_initialize_runtime_module_locked, + lean_initialize_thread, lean_io_mark_end_initialization, lean_io_mk_world, + lean_io_result_is_ok, lean_io_result_show_error, lean_string_cstr, }; use log::info; use miette::miette; @@ -150,6 +150,7 @@ impl LeanDefinitionalEngine { lean_io_mark_end_initialization(); }; }); + unsafe { lean_initialize_thread() }; Self {} } @@ -374,6 +375,12 @@ impl LeanDefinitionalEngine { } } +impl Drop for LeanDefinitionalEngine { + fn drop(&mut self) { + unsafe { lean_finalize_thread() } + } +} + impl CedarTestImplementation for LeanDefinitionalEngine { fn is_authorized( &self, diff --git a/cedar-drt/tests/benchmark.rs b/cedar-drt/tests/benchmark.rs index 5cc6444d0..2bb2bd1d9 100644 --- a/cedar-drt/tests/benchmark.rs +++ b/cedar-drt/tests/benchmark.rs @@ -163,10 +163,7 @@ fn print_summary(auth_times: HashMap<&str, Vec>, val_times: HashMap<&str, V } } -// Currently, running this in conjunction with existing tests will cause an error (#227). -// In order see the printed output from this test, run `cargo test -- --ignored --nocapture`. #[test] -#[ignore = "Can only run one Lean FFI thread currently."] fn run_all_tests() { let rust_impl = RustEngine::new(); let lean_impl = LeanDefinitionalEngine::new();