structure Lake.LeanLib : Type

• pkg : Lake.Package

  The package the library belongs to.

• config : Lake.LeanLibConfig

  The library's user-defined configuration.

A Lean library -- its package plus its configuration.

@[inline]

def Lake.Package.leanLibs (self : Lake.Package) : Array Lake.LeanLib

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

@[inline]

def Lake.Package.findLeanLib? (name : Lake.Name) (self : Lake.Package) : Option Lake.LeanLib

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

@[inline]

def Lake.LeanLib.name (self : Lake.LeanLib) : Lake.Name

The library's well-formed name.

@[inline]

def Lake.LeanLib.srcDir (self : Lake.LeanLib) : Lake.FilePath

The package's srcDir joined with the library's srcDir.

@[inline]

def Lake.LeanLib.rootDir (self : Lake.LeanLib) : Lake.FilePath

The library's root directory for lean (i.e., srcDir).

@[inline]

def Lake.LeanLib.roots (self : Lake.LeanLib) : Array Lake.Name

The names of the library's root modules (i.e., the library's roots configuration).

@[inline]

def Lake.LeanLib.isLocalModule (mod : Lake.Name) (self : Lake.LeanLib) : Bool

Whether the given module is considered local to the library.

@[inline]

def Lake.LeanLib.isBuildableModule (mod : Lake.Name) (self : Lake.LeanLib) : Bool

Whether the given module is a buildable part of the library.

@[inline]

def Lake.LeanLib.staticLibFileName (self : Lake.LeanLib) : Lake.FilePath

The file name of the library's static binary (i.e., its .a)

@[inline]

def Lake.LeanLib.staticLibFile (self : Lake.LeanLib) : Lake.FilePath

The path to the static library in the package's libDir.

@[inline]

def Lake.LeanLib.sharedLibFileName (self : Lake.LeanLib) : Lake.FilePath

The file name of the library's shared binary (i.e., its dll, dylib, or so) .

@[inline]

def Lake.LeanLib.sharedLibFile (self : Lake.LeanLib) : Lake.FilePath

The path to the shared library in the package's libDir.

@[inline]

def Lake.LeanLib.extraDepTargets (self : Lake.LeanLib) : Array Lake.Name

The library's extraDepTargets configuration.

@[inline]

def Lake.LeanLib.precompileModules (self : Lake.LeanLib) : Bool

Whether to precompile the library's modules. Is true if either the package or the library have precompileModules set.

@[inline]

def Lake.LeanLib.defaultFacets (self : Lake.LeanLib) : Array Lake.Name

The library's defaultFacets configuration.

@[inline]

def Lake.LeanLib.nativeFacets (self : Lake.LeanLib) : Array (Lake.ModuleFacet (Lake.BuildJob Lake.FilePath))

The library's nativeFacets configuration.

@[inline]

def Lake.LeanLib.buildType (self : Lake.LeanLib) : Lake.BuildType

The build type for modules of this library. That is, the minimum of package's buildType and the library's buildType.

@[inline]

def Lake.LeanLib.leanArgs (self : Lake.LeanLib) : Array String

The arguments to pass to lean when compiling the library's Lean files. That is, the package's moreLeanArgs plus the library's moreLeanArgs.

@[inline]

def Lake.LeanLib.weakLeanArgs (self : Lake.LeanLib) : Array String

The arguments to weakly pass to lean when compiling the library's Lean files. That is, the package's weakLeanArgs plus the library's weakLeanArgs.

@[inline]

def Lake.LeanLib.leancArgs (self : Lake.LeanLib) : Array String

The arguments to pass to leanc when compiling the library's C files. That is, the build type's leancArgs, the package's moreLeancArgs, and then the library's moreLeancArgs.

@[inline]

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

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