# DSL for Targets & Facets #

Macros for declaring Lake targets and facets.

## Facet Declarations #

source
@[reducible, inline]
abbrev Lake.DSL.mkModuleFacetDecl (α : Type) (facet : Lean.Name) [OptDataKind α] [FormatQuery α] [FamilyDef ModuleData facet α] (f : Module → FetchM (Job α)) :
ModuleFacetDecl
Equations

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

Instances For

source
@[reducible, inline]
abbrev Lake.DSL.mkPackageFacetDecl (α : Type) (facet : Lean.Name) [OptDataKind α] [FormatQuery α] [FamilyDef PackageData facet α] (f : Package → FetchM (Job α)) :
PackageFacetDecl
Equations

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

Instances For

source
@[reducible, inline]
abbrev Lake.DSL.mkLibraryFacetDecl (α : Type) (facet : Lean.Name) [OptDataKind α] [FormatQuery α] [FamilyDef LibraryData facet α] (f : LeanLib → FetchM (Job α)) :
LibraryFacetDecl
Equations

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

Instances For

## Custom Target Declaration #

source
@[reducible, inline]
abbrev Lake.DSL.mkTargetDecl (α : Type) (pkgName target : Lean.Name) [OptDataKind α] [FormatQuery α] [FamilyDef (CustomData pkgName) target α] (f : NPackage pkgName → FetchM (Job α)) :
TargetDecl
Equations

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

Instances For

## Lean Library & Executable Target Declarations #

source
@[reducible, inline]
abbrev Lake.DSL.mkConfigDecl (pkg name kind : Lean.Name) (config : ConfigType kind pkg name) [FamilyDef (CustomData pkg) name (ConfigTarget kind)] [FamilyDef DataType kind (ConfigTarget kind)] :
KConfigDecl kind
Equations

- Lake.DSL.mkConfigDecl pkg name kind config = { pkg := pkg, name := name, kind := kind, config := config, wf_data := ⋯, kind_eq := ⋯ }

Instances For

## External Library Target Declaration #

source
@[reducible, inline]
abbrev Lake.DSL.mkExternLibDecl (pkgName name : Lean.Name) [FamilyDef (CustomData pkgName) (name.str "static") System.FilePath] [FamilyDef (CustomData pkgName) name (ConfigTarget ExternLib.configKind)] :
ExternLibDecl
Equations

- Lake.DSL.mkExternLibDecl pkgName name = Lake.DSL.mkConfigDecl pkgName name Lake.ExternLib.configKind { getPath := cast ⋯ }

Instances For