Make LeanDefinitionalEngine::new() thread safe

[khieta]

Before opening, please confirm:

• I have searched for duplicate or closed issues.
• I have read the guide for submitting bug reports.
• I have done my best to include a minimal, self-contained set of instructions for consistently reproducing the issue.

Bug Category

Other

Describe the bug

If I try to run multiple #[test]s that use the Lean engine (created via LeanDefinitionalEngine::new()), then I get a (signal: 11, SIGSEGV: invalid memory reference) failure. If I run with the --test-threads=1 option it looks like the first test succeeds, but the next one fails.

Expected behavior

No reponse

Reproduction steps

To observe this behavior, make a second copy of the integration_tests_on_def_impl() test and run cargo test.

Code Snippet

No response

Log output

No response

Additional configuration

No response

Operating System

AL2

Additional information and screenshots

No response

[andrewmwells-amazon]

Removing the "bug" label since this is expected behavior IIUC. integration_tests_on_def_impl() calls LeanDefinitionalEngine::new() which is implemented as:

pub fn new() -> Self {
        if env::var("RUST_LEAN_INTERFACE_INIT").is_err() {
            unsafe { lean_initialize_runtime_module() };
            unsafe { lean_initialize() };
            unsafe { initialize_DiffTest_Main(1, lean_io_mk_world()) };
            unsafe { lean_io_mark_end_initialization() };
            env::set_var("RUST_LEAN_INTERFACE_INIT", "1");
        }
        Self {}
    }

https://github.com/digama0/lean-sys/blob/main/src/init.rs#L6 notes that lean_initialize_runtime_module and lean_initialize are not thread safe.

Keeping the issue open as we should switch to the thread-safe calls if possible.