structure Lake.TargetConfig (pkgName : Lake.Name) (name : Lake.Name) : Type

A custom target's declarative configuration.

• build : Lake.NPackage pkgName → Lake.IndexBuildM (Lake.CustomData (pkgName, name))

  The target's build function.

• getJob : Lake.CustomData (pkgName, name) → Lake.BuildJob Unit

  The target's resulting build job.

instance Lake.instInhabitedTargetConfig : {a a_1 : Lake.Name} → Inhabited (Lake.TargetConfig a a_1)

Equations

• Lake.instInhabitedTargetConfig = { default := { build := default, getJob := default } }

@[inline]

def Lake.mkTargetJobConfig {pkgName : Lake.Name} {α : Type} {name : Lake.Name} (build : Lake.NPackage pkgName → Lake.IndexBuildM (Lake.BuildJob α)) [h : Lake.FamilyOut Lake.CustomData (pkgName, name) (Lake.BuildJob α)] : Lake.TargetConfig pkgName name

A smart constructor for target configurations that generate CLI targets.

Equations

• Lake.mkTargetJobConfig build = { build := cast ⋯ build, getJob := fun (data : Lake.CustomData (pkgName, name)) => discard (Lake.ofFamily data) }

structure Lake.TargetDecl : Type

A dependently typed configuration based on its registered package and name.

• pkg : Lake.Name
• name : Lake.Name
• config : Lake.TargetConfig self.pkg self.name

instance Lake.OpaqueTargetConfig.instCoeTargetConfigOpaqueTargetConfig {pkgName : Lake.Name} {name : Lake.Name} : Coe (Lake.TargetConfig pkgName name) (Lake.OpaqueTargetConfig pkgName name)

Equations

• Lake.OpaqueTargetConfig.instCoeTargetConfigOpaqueTargetConfig = { coe := Lake.OpaqueTargetConfig.mk }

unsafe def Lake.OpaqueTargetConfig.unsafeMk {pkgName : Lake.Name} {name : Lake.Name} : Lake.TargetConfig pkgName name → Lake.OpaqueTargetConfig pkgName name

Equations

• Lake.OpaqueTargetConfig.unsafeMk = unsafeCast

instance Lake.OpaqueTargetConfig.instInhabitedOpaqueTargetConfig {pkgName : Lake.Name} {name : Lake.Name} [Inhabited (Lake.TargetConfig pkgName name)] : Inhabited (Lake.OpaqueTargetConfig pkgName name)

Equations

• Lake.OpaqueTargetConfig.instInhabitedOpaqueTargetConfig = { default := Lake.OpaqueTargetConfig.mk default }

@[implemented_by Lake.OpaqueTargetConfig.unsafeGet]

opaque Lake.OpaqueTargetConfig.get {pkgName : Lake.Name} {name : Lake.Name} : Lake.OpaqueTargetConfig pkgName name → Lake.TargetConfig pkgName name

instance Lake.OpaqueTargetConfig.instCoeOpaqueTargetConfigTargetConfig {pkgName : Lake.Name} {name : Lake.Name} : Coe (Lake.OpaqueTargetConfig pkgName name) (Lake.TargetConfig pkgName name)

Equations

• Lake.OpaqueTargetConfig.instCoeOpaqueTargetConfigTargetConfig = { coe := Lake.OpaqueTargetConfig.get }

@[simp]

axiom Lake.OpaqueTargetConfig.get_mk {pkgName : Lake.Name} {name : Lake.Name} : ∀ {x : Lake.TargetConfig pkgName name}, Lake.OpaqueTargetConfig.get (Lake.OpaqueTargetConfig.mk x) = x

@[implemented_by Lake.OpaqueTargetConfig.unsafeMk]

opaque Lake.OpaqueTargetConfig.mk {pkgName : Lake.Name} {name : Lake.Name} : Lake.TargetConfig pkgName name → Lake.OpaqueTargetConfig pkgName name

unsafe def Lake.OpaqueTargetConfig.unsafeGet {pkgName : Lake.Name} {name : Lake.Name} : Lake.OpaqueTargetConfig pkgName name → Lake.TargetConfig pkgName name

Equations

• Lake.OpaqueTargetConfig.unsafeGet = unsafeCast

def Lake.Package.findTargetConfig? (name : Lake.Name) (self : Lake.Package) : Option (Lake.TargetConfig (Lake.Package.name self) name)

Try to find a target configuration in the package with the given name .

Equations

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