@[reducible, inline]

abbrev Lake.ExternLib : Type

An external library -- its package plus its configuration.

Equations

• Lake.ExternLib = Lake.ConfigTarget Lake.ExternLib.configKind

Instances For

• Lake.instDataKindExternLib
• Lake.instFamilyDefNameDataTypeMkStr1ExternLib

@[inline]

def Lake.Package.externLibs (self : Package) : Array ExternLib

The external libraries of the package (as an Array).

Equations

• self.externLibs = Lake.Package.configTargets Lake.ExternLib.configKind self

@[inline]

def Lake.Package.findExternLib? (name : Lean.Name) (self : Package) : Option ExternLib

Try to find a external library in the package with the given name.

Equations

• Lake.Package.findExternLib? name self = Lake.Package.findConfigTarget? Lake.ExternLib.configKind name self

@[inline]

def Lake.ExternLib.config (self : ExternLib) : ExternLibConfig self.pkg.name self.name

The library's user-defined configuration.

Equations

• self.config = self.config

@[inline]

def Lake.ExternLib.linkArgs (self : ExternLib) : Array String

The arguments to pass to leanc when linking the external library. That is, the package's moreLinkArgs.

Equations

• self.linkArgs = self.pkg.moreLinkArgs

@[inline]

def Lake.ExternLib.staticTargetName (self : ExternLib) : Lean.Name

The name of the package target used to build the external library's static binary.

Equations

• self.staticTargetName = self.name.str "static"