Documentation

Lake.Config.FacetConfig

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

A facet's declarative configuration.

  • build : ιFetchM (DataFam name)

    The facet's build (function).

  • getJob? : Option (DataFam nameOpaqueJob)

    Does this facet produce an associated asynchronous job?

Instances For
instance Lake.instInhabitedFacetConfig {a✝ : Lean.NameType} {a✝¹ : Type} {a✝² : Lean.Name} :
Inhabited (FacetConfig a✝ a✝¹ a✝²)
Equations
@[reducible, inline]
abbrev Lake.FacetConfig.name {DataFam : Lean.NameType} {ι : Type} {name : Lean.Name} :
FacetConfig DataFam ι nameLean.Name
Equations
  • x✝.name = name
@[inline]
def Lake.mkFacetConfig {ι α : Type} {Fam : Lean.NameType} {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
@[inline]
def Lake.mkFacetJobConfig {ι α : Type} {Fam : Lean.NameType} {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
structure Lake.NamedConfigDecl (β : Lean.NameType u) :

A dependently typed configuration based on its registered name.

@[reducible, inline]

A module facet's declarative configuration.

Equations
@[reducible, inline]

A module facet declaration from a configuration file.

Equations
@[reducible, inline]

A package facet's declarative configuration.

Equations
@[reducible, inline]

A package facet declaration from a configuration file.

Equations
@[reducible, inline]

A library facet's declarative configuration.

Equations
@[reducible, inline]

A library facet declaration from a configuration file.

Equations