Remove locked routines

Cargo.toml

@@ -20,7 +20,6 @@ default = ["small_allocator", "static"]
 libc = { version = "0.2", default-features = false }
 memoffset = "0.7"
 static_assertions = "1.1.0"
-parking_lot = "0.12"
 
 [dev-dependencies]
 rand = "0.8"

src/alloc.rs

@@ -1,4 +1,3 @@
-use crate::lean_get_slot_idx;
 use crate::lean_inc_heartbeat;
 use crate::LEAN_OBJECT_SIZE_DELTA;
 use core::alloc::GlobalAlloc;
@@ -27,7 +26,7 @@ unsafe impl GlobalAlloc for LeanAlloc {
         #[cfg(feature = "small_allocator")]
         if alignment == LEAN_OBJECT_SIZE_DELTA && size <= crate::LEAN_MAX_SMALL_OBJECT_SIZE as usize
         {
-            let slot_idx = lean_get_slot_idx(size as _);
+            let slot_idx = crate::lean_get_slot_idx(size as _);
             return crate::lean_alloc_small(size as _, slot_idx).cast();
         }
 
@@ -55,14 +54,12 @@ unsafe impl GlobalAlloc for LeanAlloc {
 
 #[cfg(test)]
 mod test {
-    use crate::lean_initialize_locked;
+    use crate::test::initialize_runtime_module_for_tests;
     extern crate std;
 
     #[test]
     fn various_sized_allocations() {
-        unsafe {
-            lean_initialize_locked();
-        }
+        initialize_runtime_module_for_tests();
         use core::alloc::GlobalAlloc;
         let alloc = super::LeanAlloc;
         for size in [

src/init.rs

@@ -1,58 +1,26 @@
 /*!
 Utilities for initializing Lean's runtime
 */
-use parking_lot::Mutex;
-
-/// A convenience mutex, since [`lean_initialize_runtime_module`] and [`lean_initialize`] are *not* thread-safe.
-///
-/// It is convention to hold this when initializing Lean's runtime, or Lean modules, to make sure only one thread at a time is doing so.
-/// This is used in this library to safely implement tests, but it is the user's responsibility to uphold thread-safety when using this API.
-///
-/// # Examples
-/// ```rust
-/// # use lean_sys::*;
-/// unsafe {
-///     let guard = LEAN_INIT_MUTEX.lock();
-///     lean_initialize_runtime_module();
-///     // LEAN_INIT_MUTEX is unlocked here when `guard` goes out of scope
-/// }
-/// let big_nat = unsafe { lean_uint64_to_nat(u64::MAX) };
-/// assert!(!lean_is_scalar(big_nat));
-/// ```
-pub static LEAN_INIT_MUTEX: Mutex<()> = Mutex::new(());
-
-/// A helper function to call [`lean_initialize_runtime_module`] while holding the [`LEAN_INIT_MUTEX`].
-///
-/// This is equivalent to writing
-/// ```rust
-/// # use lean_sys::*;
-/// unsafe {
-///     let guard = LEAN_INIT_MUTEX.lock();
-///     lean_initialize_runtime_module();
-/// }
-/// ```
-//TODO: is this safe?
-pub unsafe fn lean_initialize_runtime_module_locked() {
-    let _guard = LEAN_INIT_MUTEX.lock();
-    lean_initialize_runtime_module();
-}
-
-/// A helper function to call [`lean_initialize`] while holding the [`LEAN_INIT_MUTEX`].///
-/// This is equivalent to writing
-/// ```rust
-/// # use lean_sys::*;
-/// unsafe {
-///     let guard = LEAN_INIT_MUTEX.lock();
-///     lean_initialize();
-/// }
-/// ```
-//TODO: is this safe?
-pub unsafe fn lean_initialize_locked() {
-    let _guard = LEAN_INIT_MUTEX.lock();
-    lean_initialize();
-}
 
 extern "C" {
     pub fn lean_initialize_runtime_module();
     pub fn lean_initialize();
 }
+
+#[cfg(test)]
+pub(crate) mod test {
+    use crate::lean_initialize_runtime_module;
+    extern crate std;
+
+    static INITIALIZED: std::sync::Mutex<bool> = std::sync::Mutex::new(false);
+
+    pub(crate) fn initialize_runtime_module_for_tests() {
+        let mut guard = INITIALIZED.lock().unwrap();
+        if !*guard {
+            unsafe {
+                lean_initialize_runtime_module();
+            }
+            *guard = true;
+        }
+    }
+}

src/nat.rs

@@ -213,8 +213,8 @@ mod test {
     #[test]
     fn big_nat_multiplication_commutes_test() {
         let mut rng = rand_xoshiro::Xoshiro256PlusPlus::seed_from_u64(0x568478687);
+        crate::test::initialize_runtime_module_for_tests();
         unsafe {
-            lean_initialize_runtime_module_locked();
             let mut vec = std::vec::Vec::with_capacity(100);
             for _ in 0..10 {
                 for _ in 0..100 {