Module lean_sys::init

Utilities for initializing Lean’s runtime

Statics

LEAN_INIT_MUTEX

A convenience mutex, since lean_initialize_runtime_module and lean_initialize are not thread-safe.

Functions

lean_initialize^⚠

lean_initialize_locked^⚠

A helper function to call lean_initialize while holding the LEAN_INIT_MUTEX./// This is equivalent to writing

lean_initialize_runtime_module^⚠

lean_initialize_runtime_module_locked^⚠

A helper function to call lean_initialize_runtime_module while holding the LEAN_INIT_MUTEX.