# Library Facet Builds #

Build function definitions for a library's builtin facets.

## Build Lean & Static Lib #

source
def Lake.LeanLib.leanArtsFacetConfig :
LibraryFacetConfig leanArtsFacet

The `LibraryFacetConfig` for the builtin `leanArtsFacet`.

Equations

- Lake.LeanLib.leanArtsFacetConfig = Lake.mkFacetJobConfig Lake.LeanLib.recBuildLean✝

Instances For

source
def Lake.LeanLib.staticFacetConfig :
LibraryFacetConfig staticFacet

The `LibraryFacetConfig` for the builtin `staticFacet`.

Equations

- Lake.LeanLib.staticFacetConfig = Lake.mkFacetJobConfig fun (x : Lake.LeanLib) => Lake.LeanLib.recBuildStatic✝ x false

Instances For

source
def Lake.LeanLib.staticExportFacetConfig :
LibraryFacetConfig staticExportFacet

The `LibraryFacetConfig` for the builtin `staticExportFacet`.

Equations

- Lake.LeanLib.staticExportFacetConfig = Lake.mkFacetJobConfig fun (x : Lake.LeanLib) => Lake.LeanLib.recBuildStatic✝ x true

Instances For

## Build Shared Lib #

source
def Lake.LeanLib.sharedFacetConfig :
LibraryFacetConfig sharedFacet

The `LibraryFacetConfig` for the builtin `sharedFacet`.

Equations

- Lake.LeanLib.sharedFacetConfig = Lake.mkFacetJobConfig Lake.LeanLib.recBuildShared✝

Instances For

## Other #

source
def Lake.LeanLib.extraDepFacetConfig :
LibraryFacetConfig extraDepFacet

The `LibraryFacetConfig` for the builtin `extraDepFacet`.

Equations

- Lake.LeanLib.extraDepFacetConfig = Lake.mkFacetJobConfig Lake.LeanLib.recBuildExtraDepTargets✝

Instances For

source
def Lake.LeanLib.defaultFacetConfig :
LibraryFacetConfig defaultFacet

The `LibraryFacetConfig` for the builtin `defaultFacet`.

Equations

- Lake.LeanLib.defaultFacetConfig = Lake.mkFacetJobConfig Lake.LeanLib.recBuildDefaultFacets✝

Instances For

source
def Lake.LeanLib.initFacetConfigs :
DNameMap LeanLibFacetConfig

A name-configuration map for the initial set of Lean library facets (e.g., `lean`, `static`, `shared`).

Equations

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

Instances For

source
@[reducible, inline]
abbrev Lake.initLibraryFacetConfigs :
DNameMap LibraryFacetConfig

A name-configuration map for the initial set of Lean library facets (e.g., `lean`, `static`, `shared`).

Equations

- Lake.initLibraryFacetConfigs = Lake.LeanLib.initFacetConfigs

Instances For