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).

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

@[reducible, inline]

abbrev Lake.FacetConfig.name {name : Lean.Name} : FacetConfig name → Lean.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
• 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

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

@[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.

@[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 : Bool := true) : KFacetConfig kind facet

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

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.

@[reducible, inline]

abbrev Lake.ModuleFacetDecl : Type

A module facet declaration from a configuration file.

@[reducible, inline]

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

A package facet's declarative configuration.

@[reducible, inline]

abbrev Lake.PackageFacetDecl : Type

A package facet declaration from a configuration file.

@[reducible, inline]

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

A library facet's declarative configuration.

@[reducible, inline]

abbrev Lake.LibraryFacetDecl : Type

A library facet declaration from a configuration file.

instance Lake.instTypeNameLibraryFacetDecl : TypeName LibraryFacetDecl

instance Lake.instTypeNameModuleFacetDecl : TypeName ModuleFacetDecl

instance Lake.instTypeNamePackageFacetDecl : TypeName PackageFacetDecl

@[reducible, inline]

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

A library facet's declarative configuration.

@[reducible, inline]

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

A Lean executable facet's declarative configuration.

@[reducible, inline]

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

An external library facet's declarative configuration.