structure Lake.LeanLibConfig (name : Lean.Name) extends Lake.LeanConfig : Type

A Lean library's declarative configuration.

• buildType : BuildType
• leanOptions : Array LeanOption
• moreLeanArgs : Array String
• weakLeanArgs : Array String
• moreLeancArgs : Array String
• moreServerOptions : Array LeanOption
• weakLeancArgs : Array String
• moreLinkObjs : TargetArray System.FilePath
• moreLinkLibs : TargetArray Dynlib
• moreLinkArgs : Array String
• weakLinkArgs : Array String
• backend : Backend
• platformIndependent : Option Bool
• dynlibs : TargetArray Dynlib
• plugins : TargetArray Dynlib
• srcDir : System.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 Lean.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 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 artifact. Used as a base for the file names of its static and dynamic binaries. Defaults to the mangled name of the target.

• libPrefixOnWindows : Bool

  Whether static and shared binaries of this library should be prefixed with lib on Windows.

  Unlike Unix, Windows does not require native libraries to start with lib and, by convention, they usually do not. However, for consistent naming across all platforms, users may wish to enable this.

  Defaults to false.

• needs : Array PartialBuildKey

  An Array of targets to build before the executable's modules.

• extraDepTargets : Array Lean.Name

  Deprecated. Use needs instead. 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 Lean.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 (shouldExport : Bool) : Array (ModuleFacet System.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.LeanLibConfig.extraDepTargets.instConfigField {name : Lean.Name} : ConfigField (LeanLibConfig name) `extraDepTargets (Array Lean.Name)

Equations

• Lake.LeanLibConfig.extraDepTargets.instConfigField = { toConfigProj := Lake.LeanLibConfig.extraDepTargets._proj }

instance Lake.LeanLibConfig.libName.instConfigField {name : Lean.Name} : ConfigField (LeanLibConfig name) `libName String

Equations

• Lake.LeanLibConfig.libName.instConfigField = { toConfigProj := Lake.LeanLibConfig.libName._proj }

instance Lake.LeanLibConfig.instConfigMeta : ConfigInfo `Lake.LeanLibConfig

Equations

• Lake.LeanLibConfig.instConfigMeta = { fields := Lake.LeanLibConfig._fields }

instance Lake.LeanLibConfig.toLeanConfig.instConfigParent {name : Lean.Name} : ConfigParent (LeanLibConfig name) LeanConfig

Equations

• Lake.LeanLibConfig.toLeanConfig.instConfigParent = { toConfigProj := Lake.LeanLibConfig.toLeanConfig._proj }

instance Lake.LeanLibConfig.nativeFacets.instConfigField {name : Lean.Name} : ConfigField (LeanLibConfig name) `nativeFacets (Bool → Array (ModuleFacet System.FilePath))

Equations

• Lake.LeanLibConfig.nativeFacets.instConfigField = { toConfigProj := Lake.LeanLibConfig.nativeFacets._proj }

instance Lake.LeanLibConfig.defaultFacets.instConfigField {name : Lean.Name} : ConfigField (LeanLibConfig name) `defaultFacets (Array Lean.Name)

Equations

• Lake.LeanLibConfig.defaultFacets.instConfigField = { toConfigProj := Lake.LeanLibConfig.defaultFacets._proj }

instance Lake.LeanLibConfig.precompileModules.instConfigField {name : Lean.Name} : ConfigField (LeanLibConfig name) `precompileModules Bool

Equations

• Lake.LeanLibConfig.precompileModules.instConfigField = { toConfigProj := Lake.LeanLibConfig.precompileModules._proj }

instance Lake.LeanLibConfig.instConfigFields {name : Lean.Name} : ConfigFields (LeanLibConfig name)

Equations

• Lake.LeanLibConfig.instConfigFields = { fields := Lake.LeanLibConfig._fields }

instance Lake.LeanLibConfig.needs.instConfigField {name : Lean.Name} : ConfigField (LeanLibConfig name) `needs (Array PartialBuildKey)

Equations

• Lake.LeanLibConfig.needs.instConfigField = { toConfigProj := Lake.LeanLibConfig.needs._proj }

instance Lake.LeanLibConfig.libPrefixOnWindows.instConfigField {name : Lean.Name} : ConfigField (LeanLibConfig name) `libPrefixOnWindows Bool

Equations

• Lake.LeanLibConfig.libPrefixOnWindows.instConfigField = { toConfigProj := Lake.LeanLibConfig.libPrefixOnWindows._proj }

instance Lake.LeanLibConfig.roots.instConfigField {name : Lean.Name} : ConfigField (LeanLibConfig name) `roots (Array Lean.Name)

Equations

• Lake.LeanLibConfig.roots.instConfigField = { toConfigProj := Lake.LeanLibConfig.roots._proj }

instance Lake.LeanLibConfig.globs.instConfigField {name : Lean.Name} : ConfigField (LeanLibConfig name) `globs (Array Glob)

Equations

• Lake.LeanLibConfig.globs.instConfigField = { toConfigProj := Lake.LeanLibConfig.globs._proj }

instance Lake.LeanLibConfig.srcDir.instConfigField {name : Lean.Name} : ConfigField (LeanLibConfig name) `srcDir System.FilePath

Equations

• Lake.LeanLibConfig.srcDir.instConfigField = { toConfigProj := Lake.LeanLibConfig.srcDir._proj }

instance Lake.instInhabitedLeanLibConfig {a✝ : Lean.Name} : Inhabited (LeanLibConfig a✝)

Equations

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

instance Lake.instEmptyCollectionLeanLibConfig {n : Lean.Name} : EmptyCollection (LeanLibConfig n)

Equations

• Lake.instEmptyCollectionLeanLibConfig = { emptyCollection := { } }

@[reducible, inline]

abbrev Lake.LeanLibConfig.name {n : Lean.Name} : LeanLibConfig n → Lean.Name

The library's name.

Equations

• x✝.name = n

def Lake.LeanLibConfig.isLocalModule {n : Lean.Name} (mod : Lean.Name) (self : LeanLibConfig n) : Bool

Whether the given module is considered local to the library.

Equations

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

def Lake.LeanLibConfig.isBuildableModule {n : Lean.Name} (mod : Lean.Name) (self : LeanLibConfig n) : 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.