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

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

@[inline]

def Lake.Package.findLeanLib? (name : Lean.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) : Lean.Name

The library's well-formed name.

Equations

• self.name = self.config.name

@[inline]

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

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

Equations

• self.srcDir = self.pkg.srcDir / self.config.srcDir

@[inline]

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

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

Equations

• self.rootDir = self.srcDir

@[inline]

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

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

Equations

• self.roots = self.config.roots

@[inline]

def Lake.LeanLib.isLocalModule (mod : Lean.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 : Lean.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) : System.FilePath

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

Equations

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

@[inline]

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

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

Equations

• self.staticLibFile = self.pkg.nativeLibDir / self.staticLibFileName

@[inline]

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

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

Equations

• self.staticExportLibFile = self.pkg.nativeLibDir / self.staticLibFileName.addExtension "export"

@[inline]

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

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

Equations

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

@[inline]

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

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

Equations

• self.sharedLibFile = self.pkg.nativeLibDir / self.sharedLibFileName

@[inline]

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

The library's extraDepTargets configuration.

Equations

• self.extraDepTargets = 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

• self.precompileModules = (self.pkg.precompileModules || 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

• self.platformIndependent = (self.config.platformIndependent <|> self.pkg.platformIndependent)

@[inline]

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

The library's defaultFacets configuration.

Equations

• self.defaultFacets = self.config.defaultFacets

@[inline]

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

The library's nativeFacets configuration.

Equations

• self.nativeFacets shouldExport = self.config.nativeFacets shouldExport

@[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 accumulation of:

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

Equations

• self.serverOptions = self.pkg.moreServerOptions ++ self.config.leanOptions ++ self.config.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

• self.buildType = min self.pkg.buildType self.config.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

• self.backend = self.config.backend.orPreferLeft self.pkg.backend

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

• self.leanArgs = self.pkg.moreLeanArgs ++ Array.map (fun (x : Lake.LeanOption) => x.asCliArg) self.config.leanOptions ++ self.config.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.

Equations

• self.weakLeanArgs = self.pkg.weakLeanArgs ++ self.config.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

• self.leancArgs = self.buildType.leancArgs ++ self.pkg.moreLeancArgs ++ self.config.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

• self.weakLeancArgs = self.pkg.weakLeancArgs ++ self.config.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

• self.linkArgs = self.pkg.moreLinkArgs ++ self.config.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

• self.weakLinkArgs = self.pkg.weakLinkArgs ++ self.config.weakLinkArgs