structure Lake.LeanLib : Type

A Lean library -- its package plus its configuration.

• pkg : Lake.Package

  The package the library belongs to.

• config : Lake.LeanLibConfig

  The library's user-defined configuration.

@[inline]

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

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

Equations

• Lake.Package.leanLibs self = Lake.RBArray.foldl (fun (a : Array Lake.LeanLib) (v : Lake.LeanLibConfig) => Array.push a { pkg := self, config := v }) #[] self.leanLibConfigs

@[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.

Equations

• Lake.Package.findLeanLib? name self = Option.map (fun (x : Lake.LeanLibConfig) => { pkg := self, config := x }) (Lake.RBArray.find? self.leanLibConfigs name)

@[inline]

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

The library's well-formed name.

Equations

• Lake.LeanLib.name self = self.config.name

@[inline]

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

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

Equations

• Lake.LeanLib.srcDir self = Lake.Package.srcDir self.pkg / self.config.srcDir

@[inline]

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

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

Equations

• Lake.LeanLib.rootDir self = Lake.LeanLib.srcDir self

@[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).

Equations

• Lake.LeanLib.roots self = self.config.roots

@[inline]

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

Whether the given module is considered local to the library.

Equations

• Lake.LeanLib.isLocalModule mod self = Lake.LeanLibConfig.isLocalModule mod self.config

@[inline]

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

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

Equations

• Lake.LeanLib.isBuildableModule mod self = Lake.LeanLibConfig.isBuildableModule mod self.config

@[inline]

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

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

Equations

• Lake.LeanLib.staticLibFileName self = { toString := Lake.nameToStaticLib self.config.libName }

@[inline]

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

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

Equations

• Lake.LeanLib.staticLibFile self = Lake.Package.nativeLibDir self.pkg / Lake.LeanLib.staticLibFileName self

@[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) .

Equations

• Lake.LeanLib.sharedLibFileName self = { toString := Lake.nameToSharedLib self.config.libName }

@[inline]

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

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

Equations

• Lake.LeanLib.sharedLibFile self = Lake.Package.nativeLibDir self.pkg / Lake.LeanLib.sharedLibFileName self

@[inline]

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

The library's extraDepTargets configuration.

Equations

• Lake.LeanLib.extraDepTargets self = self.config.extraDepTargets

@[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.

Equations

• Lake.LeanLib.precompileModules self = (Lake.Package.precompileModules self.pkg || self.config.precompileModules)

@[inline]

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

Equations

• Lake.LeanLib.platformIndependent self = HOrElse.hOrElse self.config.toLeanConfig.platformIndependent fun (x : Unit) => Lake.Package.platformIndependent self.pkg

@[inline]

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

The library's defaultFacets configuration.

Equations

• Lake.LeanLib.defaultFacets self = self.config.defaultFacets

@[inline]

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

The library's nativeFacets configuration.

Equations

• Lake.LeanLib.nativeFacets self = self.config.nativeFacets

@[inline]

def Lake.LeanLib.serverOptions (self : Lake.LeanLib) : Array Lake.LeanOption

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

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

Equations

• Lake.LeanLib.serverOptions self = Lake.Package.moreServerOptions self.pkg ++ self.config.toLeanConfig.leanOptions ++ self.config.toLeanConfig.moreServerOptions

@[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.

Equations

• Lake.LeanLib.buildType self = min (Lake.Package.buildType self.pkg) self.config.toLeanConfig.buildType

@[inline]

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

Equations

• Lake.LeanLib.backend self = Lake.Backend.orPreferLeft self.config.toLeanConfig.backend (Lake.Package.backend self.pkg)

@[inline]

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

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

• the package's leanOptions
• the package's moreLeanArgs
• the library's leanOptions
• the library's moreLeanArgs

Equations

• One or more equations did not get rendered due to their size.

@[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.

Equations

• Lake.LeanLib.weakLeanArgs self = Lake.Package.weakLeanArgs self.pkg ++ self.config.toLeanConfig.weakLeanArgs

@[inline]

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

Equations

• Lake.LeanLib.leancArgs self = Lake.BuildType.leancArgs (Lake.LeanLib.buildType self) ++ Lake.Package.moreLeancArgs self.pkg ++ self.config.toLeanConfig.moreLeancArgs

@[inline]

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

Equations

• Lake.LeanLib.weakLeancArgs self = Lake.Package.weakLeancArgs self.pkg ++ self.config.toLeanConfig.weakLeancArgs

@[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.

Equations

• Lake.LeanLib.linkArgs self = Lake.Package.moreLinkArgs self.pkg ++ self.config.toLeanConfig.moreLinkArgs

@[inline]

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

Equations

• Lake.LeanLib.weakLinkArgs self = Lake.Package.weakLinkArgs self.pkg ++ self.config.toLeanConfig.weakLinkArgs