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

A facet's declarative configuration.

• fetchFn : ι → FetchM (Job (DataFam name))

  The facet's fetch function.

• buildable : Bool

  Is this facet compatible with the lake build CLI?

• format : OutFormat → DataFam name → String

  Format this facet's output (e.g., for lake query).

Instances For

• Lake.instInhabitedFacetConfig

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

Equations

• Lake.instInhabitedFacetConfig = { default := { fetchFn := default, buildable := default, format := 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.mkFacetJobConfig {α : Type} {Fam : Lean.Name → Type} {facet : Lean.Name} {ι : Type} [FormatQuery α] [h : FamilyOut Fam facet α] (build : ι → FetchM (Job α)) (buildable : Bool := true) : FacetConfig Fam ι facet

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

Equations

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

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