structure Lake.FacetConfig (name : Lean.Name) : Type

A facet's declarative configuration.

• kind : Lean.Name

  The facet kind (i.e., the kind of targets that support this facet).

• fetchFn : DataType self.kind → FetchM (Job (FacetOut name))

  The facet's fetch function.

• outKind : OptDataKind (FacetOut name)

  The optional data kind of the facet's output.

• buildable : Bool

  Is this facet compatible with the lake build CLI?

• format : OutFormat → FacetOut name → String

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

• memoize : Bool

  Whether the fetch of this facet should be cached in the Lake build store.

instance Lake.instInhabitedFacetConfig {a✝ : Lean.Name} : Inhabited (FacetConfig a✝)

Equations

• Lake.instInhabitedFacetConfig = { default := { kind := default, fetchFn := default, outKind := default, buildable := default, format := default, memoize := default } }

@[reducible, inline]

abbrev Lake.FacetConfig.name {name : Lean.Name} : FacetConfig name → Lean.Name

Equations

• x✝.name = name

structure Lake.KFacetConfig (k name : Lean.Name) extends Lake.FacetConfig name : Type

• kind : Lean.Name
• fetchFn : DataType self.kind → FetchM (Job (FacetOut name))
• outKind : OptDataKind (FacetOut name)
• buildable : Bool
• format : OutFormat → FacetOut name → String
• memoize : Bool
• kind_eq : self.kind = k

@[reducible, inline]

abbrev Lake.FacetConfig.toKind {name kind : Lean.Name} (self : FacetConfig name) (h : self.kind = kind) : KFacetConfig kind name

Equations

• self.toKind h = { toFacetConfig := self, kind_eq := h }

def Lake.FacetConfig.toKind? {name : Lean.Name} (kind : Lean.Name) (self : FacetConfig name) : Option (KFacetConfig kind name)

Equations

• Lake.FacetConfig.toKind? kind self = if h : self.kind = kind then some (self.toKind h) else none

@[inline]

def Lake.KFacetConfig.run {kind : Lean.Name} {α : Type} {facet : Lean.Name} {β : Type} [FamilyOut DataType kind α] [FamilyOut FacetOut facet β] (self : KFacetConfig kind facet) (info : α) : FetchM (Job β)

Run the facet configuration's fetch function.

Equations

• self.run info = cast ⋯ (self.fetchFn (cast ⋯ info))

@[inline]

def Lake.mkFacetJobConfig {β : Type} {kind : Lean.Name} {α : Type} {facet : Lean.Name} [FormatQuery β] [outKind : OptDataKind β] [i : FamilyOut DataType kind α] [o : FamilyOut FacetOut facet β] (build : α → FetchM (Job β)) (buildable memoize : Bool := true) : KFacetConfig kind 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.KFacetConfig Lake.Module.facetKind

@[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.KFacetConfig Lake.Package.facetKind

@[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.KFacetConfig Lake.LeanLib.facetKind

@[reducible, inline]

abbrev Lake.LibraryFacetDecl : Type

A library facet declaration from a configuration file.

Equations

• Lake.LibraryFacetDecl = Lake.NamedConfigDecl Lake.LibraryFacetConfig

instance Lake.instTypeNameModuleFacetDecl : TypeName ModuleFacetDecl

Equations

• Lake.instTypeNameModuleFacetDecl = Lake.instTypeNameModuleFacetDecl.unsafe_impl_3

instance Lake.instTypeNamePackageFacetDecl : TypeName PackageFacetDecl

Equations

• Lake.instTypeNamePackageFacetDecl = Lake.instTypeNamePackageFacetDecl.unsafe_impl_3

instance Lake.instTypeNameLibraryFacetDecl : TypeName LibraryFacetDecl

Equations

• Lake.instTypeNameLibraryFacetDecl = Lake.instTypeNameLibraryFacetDecl.unsafe_impl_3

@[reducible, inline]

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

A library facet's declarative configuration.

Equations

• Lake.LeanLibFacetConfig = Lake.LibraryFacetConfig

@[reducible, inline]

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

A Lean executable facet's declarative configuration.

Equations

• Lake.LeanExeFacetConfig = Lake.KFacetConfig Lake.LeanExe.facetKind

@[reducible, inline]

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

An external library facet's declarative configuration.

Equations

• Lake.ExternLibFacetConfig = Lake.KFacetConfig Lake.ExternLib.facetKind