Make LeanDefinitionalEngine thread safe (#227)

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"

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,

cedar-drt/tests/benchmark.rs

@@ -163,10 +163,7 @@ fn print_summary(auth_times: HashMap<&str, Vec<f64>>, 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();