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 : Bool → Array (Lake.ModuleFacet (Lake.BuildJob Lake.FilePath))

  The module facets to build and combine into the library's static and shared libraries. If shouldExport is true, the module facets should export any symbols a user may expect to lookup in the library. For example, the Lean interpreter will use exported symbols in linked libraries.

  Defaults to a singleton of Module.oExportFacet (if shouldExport) or Module.oFacet. That is, the object files compiled from the Lean sources, potentially with exported Lean symbols.

instance Lake.instInhabitedLeanLibConfig : Inhabited Lake.LeanLibConfig

Equations

• One or more equations did not get rendered due to their size.

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

Whether the given module is considered local to the library.

Equations

• Lake.LeanLibConfig.isLocalModule mod self = ((self.roots.any fun (root : Lake.Name) => root.isPrefixOf mod) || self.globs.any fun (glob : Lake.Glob) => Lake.Glob.matches mod glob)

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

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

Equations

• One or more equations did not get rendered due to their size.