structure Lake.Dynlib : Type

A dynamic/shared library artifact for linking.

• path : System.FilePath

  Library file path.

• name : String

  Library name without any platform-specific prefix/suffix (for -l).

• plugin : Bool

  Whether this library can be loaded as a plugin.

• deps : Array Dynlib

  Transitive dependencies of this library for situations that need them (e.g., linking on Windows, loading via lean).

• runtimeOnlyDeps : Array Dynlib

  Non-link transitive dependencies of this library that are only required at runtime (e.g., libraries loaded dynamically via dlopen). Used by Lake to preload such dependencies for lean elaboration when precompiling.

@[instance_reducible]

instance Lake.instInhabitedDynlib : Inhabited Dynlib

Equations

• Lake.instInhabitedDynlib = { default := Lake.instInhabitedDynlib.default }

@[instance_reducible]

instance Lake.instReprDynlib : Repr Dynlib

Equations

• Lake.instReprDynlib = { reprPrec := Lake.instReprDynlib.repr }

partial def Lake.instReprDynlib.repr : Dynlib → Nat → Std.Format

def Lake.Dynlib.dir? (self : Dynlib) : Option System.FilePath

Optional library directory (for -L).

Equations

• self.dir? = self.path.parent

@[instance_reducible]

instance Lake.Dynlib.instToJson : Lean.ToJson Dynlib

Equations

• Lake.Dynlib.instToJson = { toJson := fun (x : Lake.Dynlib) => Lean.Json.str x.path.toString }

@[instance_reducible]

instance Lake.Dynlib.instToString : ToString Dynlib

Equations

• Lake.Dynlib.instToString = { toString := fun (x : Lake.Dynlib) => x.path.toString }

@[instance_reducible]

instance Lake.Dynlib.instCoeFilePath : Coe Dynlib System.FilePath

Equations

• Lake.Dynlib.instCoeFilePath = { coe := fun (x : Lake.Dynlib) => x.path }