def Lean.Dynlib : Type

A dynamic library handle.

Equations

• Lean.Dynlib = Lean.DynlibImpl✝.type

instance Lean.instNonemptyDynlib : Nonempty Dynlib

def Lean.Dynlib.Symbol (dynlib : Dynlib) : Type

A reference to a symbol within a dynamic library.

Equations

• dynlib.Symbol = (Lean.Dynlib.SymbolImpl✝ dynlib).type

instance Lean.instNonemptySymbol {dynlib : Dynlib} : Nonempty dynlib.Symbol

@[extern lean_dynlib_load]

opaque Lean.Dynlib.load (path : System.FilePath) : IO Dynlib

Dynamically loads a shared library.

The path may also be used perform a system-dependent search for library. To avoid this, use an absolute path (e.g., from IO.FS.realPath).

@[extern lean_dynlib_get]

opaque Lean.Dynlib.get? (dynlib : Dynlib) (sym : String) : Option dynlib.Symbol

Returns the symbol of the dynamic library with the specified name (if any).

@[extern lean_dynlib_symbol_run_as_init]

unsafe opaque Lean.Dynlib.Symbol.runAsInit {dynlib : Dynlib} (sym : dynlib.Symbol) : IO Unit

Runs a module initializer function. The symbol should have the signature (builtin : Bool) → IO Unit (e.g., initialize_Foo(uint8_t builtin, obj_arg)).

This function is unsafe because there is no guarantee the symbol has the expected signature. An invalid symbol can thus produce undefined behavior. Furthermore, if the initializer introduces pointers (e.g., function closures) from the dynamic library into the global state, future garbage collection of the library will produce undefined behavior. In such cases, garbage collection of the dynamic library can be prevented via Runtime.markPersistent or Runtime.forget.

@[export lean_load_dynlib]

def Lean.loadDynlib (path : System.FilePath) : IO Unit

Dynamically loads a shared library so that its symbols can be used by the Lean interpreter (e.g., for interpreting @[extern] declarations). Equivalent to passing --load-dynlib=path to lean.

Lean never unloads libraries. Attempting to load a library that defines symbols shared with a previously loaded library (including itself) will error. If multiple libraries share common symbols, those symbols should be linked and loaded as separate libraries.

Equations

• Lean.loadDynlib path = do let dynlib ← Lean.Dynlib.load path let __discr ← liftM (Lean.loadDynlib.unsafe_impl_1 dynlib) let x : Lean.Dynlib := __discr pure PUnit.unit

@[export lean_load_plugin]

def Lean.loadPlugin (path : System.FilePath) : IO Unit

Loads a Lean plugin and runs its initializers.

A Lean plugin is a shared library built from a Lean module. This means it has an initialize_<module-name> symbol that runs the module's initializers (including its imports' initializers). Initializers are declared with the initialize or builtin_initialize commands.

This is similar to passing --plugin=path to lean. Lean environment initializers, such as definitions calling registerEnvExtension, also require Lean.initializing to be true. To enable them, use loadPlugin within a withImporting block. This will set Lean.initializing (but not IO.initializing).

Lean never unloads plugins. Attempting to load a plugin that defines symbols shared with a previously loaded plugin (including itself) will error. If multiple plugins share common symbols (e.g., imports), those symbols should be linked and loaded separately.

Equations

• One or more equations did not get rendered due to their size.