- buildType : Lake.BuildType
- name : Lake.Name
The name of the target.
- srcDir : Lake.FilePath
The subdirectory of the package's source directory containing the library's Lean source files. Defaults simply to said
(This will be passed to
The root module(s) of the library.
Submodules of these roots (e.g.,
Lib) are considered part of the package.
Defaults to a single root of the library's upper camel case name.
- libName : String
The name of the library. Used as a base for the file names of its static and dynamic binaries. Defaults to the upper camel case name of the target.
Arrayof target names to build before the library's modules.
- precompileModules : Bool
Whether to compile each of the library's modules into a native shared library that is loaded whenever the module is imported. This speeds up evaluation of metaprograms and enables the interpreter to run functions marked
Arrayof library facets to build on a bare
lake buildof the library. For example,
#[LeanLib.sharedLib]will build the shared library facet.
Arrayof module facets to build and combine into the library's static and shared libraries. Defaults to
#[Module.oFacet](i.e., the object file compiled from the Lean source).
A Lean library's declarative configuration.