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

• build : ι → Lake.IndexBuildM (DataFam name)

  The facet's build (function).

• getJob? : Option (DataFam name → Lake.BuildJob Unit)

  Does this facet produce an associated asynchronous job?

A facet's declarative configuration.

instance Lake.instInhabitedFacetConfig : {a : Lake.Name → Type} → {a_1 : Type} → {a_2 : Lake.Name} → Inhabited (Lake.FacetConfig a a_1 a_2)

@[inline, reducible]

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

@[inline]

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

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

@[inline]

def Lake.mkFacetJobConfigSmall {ι : Type} {α : Type} {Fam : Lake.Name → Type} {facet : Lake.Name} (build : ι → Lake.IndexBuildM (Lake.BuildJob α)) [h : Lake.FamilyOut Fam facet (Lake.BuildJob α)] : Lake.FacetConfig Fam ι facet

A smart constructor for facet configurations that generate jobs for the CLI. This is for small jobs that do not the increase the progress counter.

@[inline]

def Lake.mkFacetJobConfig {ι : Type} {α : Type} {Fam : Lake.Name → Type} {facet : Lake.Name} (build : ι → Lake.IndexBuildM (Lake.BuildJob α)) [Lake.FamilyOut Fam facet (Lake.BuildJob α)] : Lake.FacetConfig Fam ι facet

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

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

• name : Lake.Name
• config : β s.name

A dependently typed configuration based on its registered name.

@[inline, reducible]

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

A module facet's declarative configuration.

@[inline, reducible]

abbrev Lake.ModuleFacetDecl : Type

A module facet declaration from a configuration file.

@[inline, reducible]

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

A package facet's declarative configuration.

@[inline, reducible]

abbrev Lake.PackageFacetDecl : Type

A package facet declaration from a configuration file.

@[inline, reducible]

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

A library facet's declarative configuration.

@[inline, reducible]

abbrev Lake.LibraryFacetDecl : Type

A library facet declaration from a configuration file.