@[export lean_enable_initializer_execution]

unsafe def Lean.enableInitializersExecution : IO Unit

By default the initialize code is not executed when importing .olean files. When this flag is set to true, the initializers are executed. This method is meant to be used by the Lean frontend only. Remark: it is not safe to run initialize code when using multiple threads. Remark: Any loaded native Lean code must match its imported version. In particular, no two versions of the same module may be loaded when this flag is set. No native code may be loaded after its module has been imported. Remark: Compacted module regions must not be freed when using this flag as the cached initializer results may reference objects in them. Remark: The Lean frontend executes this method at startup time.

def Lean.isInitializerExecutionEnabled : IO Bool

Equations

• Lean.isInitializerExecutionEnabled = ST.Ref.get Lean.runInitializersRef✝

def Lean.initializing : IO Bool

We say Lean is "initializing" when it is executing builtin_initialize declarations or importing modules. Recall that Lean executes initialize declarations while importing modules.

def Lean.withImporting {α : Type} (x : IO α) : IO α

Execute x with "importing" flag turned on. When the "importing" flag is set to true, we allow user-extensions defined with with the initialize command to update global references. IMPORTANT: There is no semaphore controlling the access to these global references. We assume these global references are updated by a single execution thread. This is true in the Lean frontend where we process the import commands at the beginning of the execution only. Users must make sure that when importModules is used, there is only one execution thread accessing the global references.

Equations

• Lean.withImporting x = tryFinally (do ST.Ref.set Lean.importingRef✝ true x) do ST.Ref.set Lean.importingRef✝ false ST.Ref.set Lean.runInitializersRef✝ false