@[reducible, inline]

abbrev Lake.LeanLib : Type

A Lean library -- its package plus its configuration.

@[inline]

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

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

@[inline]

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

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

@[inline]

def Lake.LeanLib.config (self : LeanLib) : LeanLibConfig self.name

The library's user-defined configuration.

@[inline]

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

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

@[inline]

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

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

@[inline]

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

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

@[inline]

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

Whether the given module is considered local to the library.

@[inline]

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

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

@[inline]

def Lake.LeanLib.libName (self : LeanLib) : String

The name of the library artifact.

@[inline]

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

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

@[inline]

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

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

@[inline]

def Lake.LeanLib.staticExportLibFile (self : LeanLib) : System.FilePath

The path to the static library (with exported symbols) in the package's libDir.

@[inline]

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

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

@[inline]

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

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

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

Whether the shared binary of this library is a valid plugin.

@[inline]

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

The library's extraDepTargets configuration.

@[inline]

def Lake.LeanLib.precompileModules (self : 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.platformIndependent (self : LeanLib) : Option Bool

Whether to the library's Lean code is platform-independent. Returns the library's platformIndependent configuration if non-none. Otherwise, falls back to the package's.

@[inline]

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

The library's defaultFacets configuration.

@[inline]

def Lake.LeanLib.nativeFacets (self : LeanLib) (shouldExport : Bool) : Array (ModuleFacet System.FilePath)

The library's nativeFacets configuration.

@[inline]

def Lake.LeanLib.buildType (self : LeanLib) : 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.serverOptions (self : LeanLib) : Array LeanOption

The arguments to pass to lean --server when running the Lean language server. serverOptions is the accumulation of:

• the build type's leanOptions
• the package's leanOptions
• the package's moreServerOptions
• the library's leanOptions
• the library's moreServerOptions

@[inline]

def Lake.LeanLib.backend (self : LeanLib) : Backend

The backend type for modules of this library. Prefer the library's backend configuration, then the package's, then the default (which is C for now).

@[inline]

def Lake.LeanLib.dynlibs (self : LeanLib) : TargetArray Dynlib

The dynamic libraries to load for modules of this library. The targets of the package plus the targets of the library (in that order).

@[inline]

def Lake.LeanLib.plugins (self : LeanLib) : TargetArray Dynlib

The Lean plugins for modules of this library. The targets of the package plus the targets of the library (in that order).

@[inline]

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

The arguments to pass to lean when compiling the library's Lean files. leanArgs is the accumulation of:

• the build type's leanArgs
• the package's leanOptions
• the package's moreLeanArgs
• the library's leanOptions
• the library's moreLeanArgs

@[inline]

def Lake.LeanLib.weakLeanArgs (self : 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 : LeanLib) : Array String

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

@[inline]

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

The arguments to weakly pass to leanc when compiling the library's Lean-produced C files. That is, the package's weakLeancArgs plus the library's weakLeancArgs.

@[inline]

def Lake.LeanLib.moreLinkObjs (self : LeanLib) : TargetArray System.FilePath

Additionl target objects to pass to ar when linking the static library. That is, the package's moreLinkObjs plus the library's moreLinkObjs.

@[inline]

def Lake.LeanLib.moreLinkLibs (self : LeanLib) : TargetArray Dynlib

@[inline]

def Lake.LeanLib.linkArgs (self : 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.

@[inline]

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

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