- 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.
Instances For
The Lean libraries of the package (as an Array).
Instances For
Try to find a Lean library in the package with the given name.
Instances For
The library's well-formed name.
Instances For
The names of the library's root modules
(i.e., the library's roots
configuration).
Instances For
Whether the given module is considered local to the library.
Instances For
Whether the given module is a buildable part of the library.
Instances For
The file name of the library's static binary (i.e., its .a
)
Instances For
The path to the static library in the package's libDir
.
Instances For
Whether to precompile the library's modules.
Is true if either the package or the library have precompileModules
set.
Instances For
The library's nativeFacets
configuration.
Instances For
The arguments to pass to lean
when compiling the library's Lean files.
That is, the package's moreLeanArgs
plus the library's moreLeanArgs
.
Instances For
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
.
Instances For
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
.
Instances For
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
.
Instances For
The arguments to pass to leanc
when linking the shared library.
That is, the package's moreLinkArgs
plus the library's moreLinkArgs
.
Instances For
The arguments to weakly pass to leanc
when linking the shared library.
That is, the package's weakLinkArgs
plus the library's weakLinkArgs
.