digama0 / lean-sys

Rust bindings for the Lean 4 proof assistant
Apache License 2.0
17 stars 5 forks source link

Remove locked routines #6

Open SchrodingerZhu opened 1 year ago

SchrodingerZhu commented 1 year ago

@digama0 So, parking_lot still requires std, which is annoying. This PR provides a potential fix.

However, I suggest we should completely remove the *_locked things. It is hardly useful to provide such locked routines. Users cannot call it multiple times, even if it is locked. Users still struggle to maintain the status to check if Lean is already initialized. Also, the user may initialize their own pieces between lean_initialize and io_mark_end_initialization, where exclusivity is required during the whole time, but these *_locked things simply release the lock after the first function call.

// Why not just mark `lean_initialize_runtime_module` as `MT-unsafe` and let users use their own lock?
pub(crate) fn initialize_runtime_module_for_tests() {
        let _guard = LEAN_INIT_MUTEX.lock();
        if !INITIALIZED.load(std::sync::atomic::Ordering::SeqCst) {
            unsafe {
                lean_initialize_runtime_module();
            }
            INITIALIZED.store(true, std::sync::atomic::Ordering::SeqCst);
        }
    }

As in this low-level lean-sys, I think just providing the unsafe initialization routine is fine.

SchrodingerZhu commented 1 year ago

@digama0 I change this PR to remove *_locked initializations. I also found a problem in previous tests where initialization can be called multiple times. At least for small_allocator, such repeated initialization means that previously allocated pages are leaked.