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.
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
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)
Whether the given module is considered local to the library.
Equations
- Lake.LeanLib.isLocalModule mod self = Lake.LeanLibConfig.isLocalModule mod self.config
Whether the given module is a buildable part of the library.
Equations
- Lake.LeanLib.isBuildableModule mod self = Lake.LeanLibConfig.isBuildableModule mod self.config
The file name of the library's static binary (i.e., its .a
)
Equations
- self.staticLibFileName = { toString := Lake.nameToStaticLib self.config.libName }
The path to the static library in the package's libDir
.
The path to the static library (with exported symbols) in the package's libDir
.
The library's extraDepTargets
configuration.
Equations
- self.extraDepTargets = self.config.extraDepTargets
Whether to precompile the library's modules.
Is true if either the package or the library have precompileModules
set.
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)
The library's defaultFacets
configuration.
Equations
- self.defaultFacets = self.config.defaultFacets
The library's nativeFacets
configuration.
Equations
- self.nativeFacets shouldExport = self.config.nativeFacets shouldExport
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
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
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
.
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
.
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
.
The arguments to pass to leanc
when linking the shared library.
That is, the package's moreLinkArgs
plus the library's moreLinkArgs
.
The arguments to weakly pass to leanc
when linking the shared library.
That is, the package's weakLinkArgs
plus the library's weakLinkArgs
.