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