Lake.Config.LeanLibConfig

source

structure Lake.LeanLibConfigextends Lake.LeanConfig :

Type

A Lean library's declarative configuration.

buildType : Lake.BuildType
leanOptions : Array Lake.LeanOption
moreLeanArgs : Array String
weakLeanArgs : Array String
moreLeancArgs : Array String
moreServerOptions : Array Lake.LeanOption
weakLeancArgs : Array String
moreLinkArgs : Array String
weakLinkArgs : Array String
backend : Lake.Backend
platformIndependent : Option Bool
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 srcDir.
(This will be passed to lean as the -R option.)
roots : Array Lake.Name
The root module(s) of the library. Submodules of these roots (e.g., Lib.Foo of Lib) are considered part of the library. Defaults to a single root of the target's name.
globs : Array Lake.Glob
An Array of module Globs to build for the library. Defaults to a Glob.one of each of the library's roots.
Submodule globs build every source file within their directory. Local imports of glob'ed files (i.e., fellow modules of the workspace) are also recursively built.
libName : String
The name of the library. Used as a base for the file names of its static and dynamic binaries. Defaults to the name of the target.
extraDepTargets : Array Lake.Name
An Array of 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 @[extern].
Defaults to false.
defaultFacets : Array Lake.Name
An Array of library facets to build on a bare lake build of the library. For example, #[LeanLib.sharedLib] will build the shared library facet.
nativeFacets : Array (Lake.ModuleFacet (Lake.BuildJob Lake.FilePath))
An Array of 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).