lean_sys/
init.rs

1/*!
2Utilities for initializing Lean's runtime
3*/
4use parking_lot::Mutex;
5
6/// A convenience mutex, since [`lean_initialize_runtime_module`] and [`lean_initialize`] are *not* thread-safe.
7///
8/// 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.
9/// 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.
10///
11/// # Examples
12/// ```rust
13/// # use lean_sys::*;
14/// unsafe {
15///     let guard = LEAN_INIT_MUTEX.lock();
16///     lean_initialize_runtime_module();
17///     // LEAN_INIT_MUTEX is unlocked here when `guard` goes out of scope
18/// }
19/// let big_nat = unsafe { lean_uint64_to_nat(u64::MAX) };
20/// assert!(!lean_is_scalar(big_nat));
21/// ```
22pub static LEAN_INIT_MUTEX: Mutex<()> = Mutex::new(());
23
24/// A helper function to call [`lean_initialize_runtime_module`] while holding the [`LEAN_INIT_MUTEX`].
25///
26/// This is equivalent to writing
27/// ```rust
28/// # use lean_sys::*;
29/// unsafe {
30///     let guard = LEAN_INIT_MUTEX.lock();
31///     lean_initialize_runtime_module();
32/// }
33/// ```
34//TODO: is this safe?
35pub unsafe fn lean_initialize_runtime_module_locked() {
36    let _guard = LEAN_INIT_MUTEX.lock();
37    lean_initialize_runtime_module();
38}
39
40/// A helper function to call [`lean_initialize`] while holding the [`LEAN_INIT_MUTEX`].///
41/// This is equivalent to writing
42/// ```rust
43/// # use lean_sys::*;
44/// unsafe {
45///     let guard = LEAN_INIT_MUTEX.lock();
46///     lean_initialize();
47/// }
48/// ```
49//TODO: is this safe?
50pub unsafe fn lean_initialize_locked() {
51    let _guard = LEAN_INIT_MUTEX.lock();
52    lean_initialize();
53}
54
55extern "C" {
56    pub fn lean_initialize_runtime_module();
57    pub fn lean_initialize();
58}
lean_sys/init.rs

lean_sys/
init.rs
