src/Lean/LoadDynlib.lean

/-
Copyright (c) 2021 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
module

prelude
public import Init.System.IO
import Init.Data.String.TakeDrop
import Init.Data.ToString.Macro

public section

namespace Lean

private opaque DynlibImpl : NonemptyType.{0}
/-- A dynamic library handle. -/
def Dynlib := DynlibImpl.type
instance : Nonempty Dynlib := by exact DynlibImpl.property

private opaque Dynlib.SymbolImpl (dynlib : Dynlib) : NonemptyType.{0}
/-- A reference to a symbol within a dynamic library. -/
def Dynlib.Symbol (dynlib : Dynlib) := SymbolImpl dynlib |>.type
instance : Nonempty (Dynlib.Symbol dynlib) := by exact Dynlib.SymbolImpl dynlib |>.property

/--
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_load"]
opaque Dynlib.load (path : @& System.FilePath) : IO Dynlib

/-- Returns the symbol of the dynamic library with the specified name (if any).  -/
@[extern "lean_dynlib_get"]
opaque Dynlib.get? (dynlib : @& Dynlib) (sym : @& String) : Option dynlib.Symbol

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

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`.
-/
@[extern "lean_dynlib_symbol_run_as_init"]
unsafe opaque Dynlib.Symbol.runAsInit {dynlib : @& Dynlib} (sym : @& dynlib.Symbol) : 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.
-/
@[export lean_load_dynlib]
def loadDynlib (path : System.FilePath) : IO Unit := do
  let dynlib ← Dynlib.load path
  -- Lean never unloads libraries.
  -- Safety: There are no concurrent accesses to `dynlib` at this point.
  let _ ← unsafe Runtime.markPersistent dynlib

/--
Loads a Lean plugin and runs its initializers.

A Lean plugin is a shared library with an initialization function. If
no `initFn?` is explicitly provided, the initalization function will be
derived from the library's name (as `initialize_<lib-name>`).

Plugins built from a Lean module will have an initialization function 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` (or `--plugin=path:initFn`) 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.
-/
@[export lean_load_plugin]
def loadPlugin (path : System.FilePath) (initFn? : Option String := none) : IO Unit := do
  -- We never want to look up plugins using the system library search
  let path ← IO.FS.realPath path
  let name ← initFn?.getDM do
    let some name := path.fileStem
    | throw <| IO.userError s!"error, plugin has invalid file name '{path}'"
    -- Lean libraries can be prefixed with `lib` or suffixed with `_shared`
    -- under some configurations. We strip these from the default initializer symbol.
    let name := name.dropPrefix "lib" |>.dropSuffix "_shared"
    return s!"initialize_{name}"
  let dynlib ← Dynlib.load path
  let some sym := dynlib.get? name
    | throw <| IO.userError s!"error loading plugin, initializer not found '{name}'"
  -- Lean never unloads plugins (once initialized).
  -- Safety: There are no concurrent accesses to `dynlib` at this point.
  let _ ← unsafe Runtime.markPersistent dynlib
  /-
  Safety:
  * As `dynlib` is marked persistent, there is no danger of garbage collection.
  * There is still no guarantee that `sym` has the proper signature, but this
    is about as safe as it can be. The default initializer naming convention helps
    avoid accidentally mistaking non-plugins as plugins.
  -/
  unsafe sym.runAsInit