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

A facet's declarative configuration.

• 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?

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

Equations

• Lake.instInhabitedFacetConfig = { default := { build := default, getJob? := default } }

@[inline, reducible]

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

Equations

• Lake.FacetConfig.name x = 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.

Equations

• Lake.mkFacetConfig build = { build := cast (_ : (ι → Lake.IndexBuildM α) = (ι → Lake.IndexBuildM (Fam facet))) build, getJob? := none }

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

Equations

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

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

Equations

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

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

A dependently typed configuration based on its registered name.

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

@[inline, reducible]

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

A module facet's declarative configuration.

Equations

• Lake.ModuleFacetConfig = Lake.FacetConfig Lake.ModuleData Lake.Module

@[inline, reducible]

abbrev Lake.ModuleFacetDecl : Type

A module facet declaration from a configuration file.

Equations

• Lake.ModuleFacetDecl = Lake.NamedConfigDecl Lake.ModuleFacetConfig

@[inline, reducible]

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

A package facet's declarative configuration.

Equations

• Lake.PackageFacetConfig = Lake.FacetConfig Lake.PackageData Lake.Package

@[inline, reducible]

abbrev Lake.PackageFacetDecl : Type

A package facet declaration from a configuration file.

Equations

• Lake.PackageFacetDecl = Lake.NamedConfigDecl Lake.PackageFacetConfig

@[inline, reducible]

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

A library facet's declarative configuration.

Equations

• Lake.LibraryFacetConfig = Lake.FacetConfig Lake.LibraryData Lake.LeanLib

@[inline, reducible]

abbrev Lake.LibraryFacetDecl : Type

A library facet declaration from a configuration file.

Equations

• Lake.LibraryFacetDecl = Lake.NamedConfigDecl Lake.LibraryFacetConfig