DSL for Targets & Facets #
Macros for declaring Lake targets and facets.
Facet Declarations #
@[reducible, inline]
abbrev
Lake.DSL.mkModuleFacetDecl
(α : Type)
(facet : Lean.Name)
[OptDataKind α]
[FormatQuery α]
[FamilyDef ModuleData facet α]
(f : Module → FetchM (Job α))
:
Equations
Instances For
@[reducible, inline]
abbrev
Lake.DSL.mkPackageFacetDecl
(α : Type)
(facet : Lean.Name)
[OptDataKind α]
[FormatQuery α]
[FamilyDef PackageData facet α]
(f : Package → FetchM (Job α))
:
Equations
Instances For
@[reducible, inline]
abbrev
Lake.DSL.mkLibraryFacetDecl
(α : Type)
(facet : Lean.Name)
[OptDataKind α]
[FormatQuery α]
[FamilyDef LibraryData facet α]
(f : LeanLib → FetchM (Job α))
:
Equations
Instances For
Custom Target Declaration #
@[reducible, inline]
abbrev
Lake.DSL.mkTargetDecl
(α : Type)
(pkgName target : Lean.Name)
[OptDataKind α]
[FormatQuery α]
[FamilyDef (CustomData pkgName) target α]
(f : NPackage pkgName → FetchM (Job α))
:
Equations
Instances For
Lean Library & Executable Target Declarations #
@[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
Instances For
External Library Target Declaration #
@[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)]
: