structure Lake.LeanLibConfigextends Lake.LeanConfig : Type

• buildType : Lake.BuildType
• moreLeanArgs : Array String
• weakLeanArgs : Array String
• moreLeancArgs : Array String
• moreLinkArgs : Array String
• 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 package.

  Defaults to a single root of the library's upper camel case 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 upper camel case 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).

A Lean library's declarative configuration.

instance Lake.instInhabitedLeanLibConfig : Inhabited Lake.LeanLibConfig

def Lake.LeanLibConfig.isLocalModule (mod : Lake.Name) (self : Lake.LeanLibConfig) : Bool

Whether the given module is considered local to the library.

def Lake.LeanLibConfig.isBuildableModule (mod : Lake.Name) (self : Lake.LeanLibConfig) : Bool

Whether the given module is a buildable part of the library.