structure Lake.ExternLib : Type

• pkg : Lake.Package

  The package the library belongs to.

• name : Lake.Name

  The external library's name.

• config : Lake.ExternLibConfig (Lake.Package.name s.pkg) s.name

  The library's user-defined configuration.

An external library -- its package plus its configuration.

@[inline]

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

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

Equations

• Lake.Package.externLibs self = Lake.DRBMap.fold (fun a x v => Array.push a { pkg := self, name := x, config := v }) #[] self.externLibConfigs

@[inline]

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

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

Equations

• Lake.Package.findExternLib? name self = Option.map (fun x => { pkg := self, name := name, config := x }) (Lake.DRBMap.find? self.externLibConfigs name)

@[inline]

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

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

Equations

• Lake.ExternLib.linkArgs self = Lake.Package.moreLinkArgs self.pkg

@[inline]

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

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

Equations

• Lake.ExternLib.staticTargetName self = Lean.Name.str self.name "static"