structure Lake.FacetConfig (DataFam : Lean.Name → Type) (ι : Type) (name : Lean.Name) : Type

A facet's declarative configuration.

• build : ι → FetchM (DataFam name)

  The facet's build (function).

• getJob? : Option (DataFam name → OpaqueJob)

  Does this facet produce an associated asynchronous job?

instance Lake.instInhabitedFacetConfig {a✝ : Lean.Name → Type} {a✝¹ : Type} {a✝² : Lean.Name} : Inhabited (FacetConfig a✝ a✝¹ a✝²)

Equations

• Lake.instInhabitedFacetConfig = { default := { build := default, getJob? := default } }

@[reducible, inline]

abbrev Lake.FacetConfig.name {DataFam : Lean.Name → Type} {ι : Type} {name : Lean.Name} : FacetConfig DataFam ι name → Lean.Name

Equations

• x✝.name = name

@[inline]

def Lake.mkFacetConfig {ι α : Type} {Fam : Lean.Name → Type} {facet : Lean.Name} (build : ι → FetchM α) [h : FamilyOut Fam facet α] : FacetConfig Fam ι facet

A smart constructor for facet configurations that are not known to generate targets.

Equations

• Lake.mkFacetConfig build = { build := cast ⋯ build, getJob? := none }

@[inline]

def Lake.mkFacetJobConfig {ι α : Type} {Fam : Lean.Name → Type} {facet : Lean.Name} (build : ι → FetchM (Job α)) [h : FamilyOut Fam facet (Job α)] : FacetConfig Fam ι facet

A smart constructor for facet configurations that generate jobs for the CLI.

Equations

• Lake.mkFacetJobConfig build = { build := cast ⋯ build, getJob? := some fun (data : Fam facet) => (Lake.ofFamily data).toOpaque }

structure Lake.NamedConfigDecl (β : Lean.Name → Type u) : Type u

A dependently typed configuration based on its registered name.

• name : Lean.Name
• config : β self.name

@[reducible, inline]

abbrev Lake.ModuleFacetConfig (name : Lean.Name) : Type

A module facet's declarative configuration.

Equations

• Lake.ModuleFacetConfig = Lake.FacetConfig Lake.ModuleData Lake.Module

@[reducible, inline]

abbrev Lake.ModuleFacetDecl : Type

A module facet declaration from a configuration file.

Equations

• Lake.ModuleFacetDecl = Lake.NamedConfigDecl Lake.ModuleFacetConfig

@[reducible, inline]

abbrev Lake.PackageFacetConfig (name : Lean.Name) : Type

A package facet's declarative configuration.

Equations

• Lake.PackageFacetConfig = Lake.FacetConfig Lake.PackageData Lake.Package

@[reducible, inline]

abbrev Lake.PackageFacetDecl : Type

A package facet declaration from a configuration file.

Equations

• Lake.PackageFacetDecl = Lake.NamedConfigDecl Lake.PackageFacetConfig

@[reducible, inline]

abbrev Lake.LibraryFacetConfig (name : Lean.Name) : Type

A library facet's declarative configuration.

Equations

• Lake.LibraryFacetConfig = Lake.FacetConfig Lake.LibraryData Lake.LeanLib

@[reducible, inline]

abbrev Lake.LibraryFacetDecl : Type

A library facet declaration from a configuration file.

Equations

• Lake.LibraryFacetDecl = Lake.NamedConfigDecl Lake.LibraryFacetConfig