Documentation

Lake.DSL.Targets

DSL for Targets & Facets #

Macros for declaring Lake targets and facets.

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

Facet Declarations #

@[reducible, inline]
Equations
  • One or more equations did not get rendered due to their size.

Define a new module facet. Has one form:

module_facet «facet-name» (mod : Module) : α :=
  /- build term of type `FetchM (Job α)` -/

The mod parameter (and its type specifier) is optional.

Equations
  • One or more equations did not get rendered due to their size.
@[reducible, inline]
Equations
  • One or more equations did not get rendered due to their size.

Define a new package facet. Has one form:

package_facet «facet-name» (pkg : Package) : α :=
  /- build term of type `FetchM (Job α)` -/

The pkg parameter (and its type specifier) is optional.

Equations
  • One or more equations did not get rendered due to their size.
@[reducible, inline]
Equations
  • One or more equations did not get rendered due to their size.

Define a new library facet. Has one form:

library_facet «facet-name» (lib : LeanLib) : α :=
  /- build term of type `FetchM (Job α)` -/

The lib parameter (and its type specifier) is optional.

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

Custom Target Declaration #

@[reducible, inline]
abbrev Lake.DSL.mkTargetDecl (α : Type) (pkgName target : Lean.Name) [FormatQuery α] [FamilyDef CustomData (pkgName, target) α] (f : NPackage pkgNameFetchM (Job α)) :
Equations
  • One or more equations did not get rendered due to their size.

Define a new custom target for the package. Has one form:

target «target-name» (pkg : NPackage _package.name) : α :=
  /- build term of type `FetchM (Job α)` -/

The pkg parameter (and its type specifier) is optional. It is of type NPackage _package.name to provably demonstrate the package provided is the package in which the target is defined.

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

Lean Library & Executable Target Declarations #

Define a new Lean library target for the package. Can optionally be provided with a configuration of type LeanLibConfig. Has many forms:

lean_lib «target-name»
lean_lib «target-name» { /- config opts -/ }
lean_lib «target-name» where /- config opts -/
Equations
  • One or more equations did not get rendered due to their size.
@[reducible, inline]

Define a new Lean library target for the package. Can optionally be provided with a configuration of type LeanLibConfig. Has many forms:

lean_lib «target-name»
lean_lib «target-name» { /- config opts -/ }
lean_lib «target-name» where /- config opts -/
Equations
Instances For

Define a new Lean binary executable target for the package. Can optionally be provided with a configuration of type LeanExeConfig. Has many forms:

lean_exe «target-name»
lean_exe «target-name» { /- config opts -/ }
lean_exe «target-name» where /- config opts -/
Equations
  • One or more equations did not get rendered due to their size.
@[reducible, inline]

Define a new Lean binary executable target for the package. Can optionally be provided with a configuration of type LeanExeConfig. Has many forms:

lean_exe «target-name»
lean_exe «target-name» { /- config opts -/ }
lean_exe «target-name» where /- config opts -/
Equations
Instances For

External Library Target Declaration #

@[reducible, inline]
Equations
Equations
  • One or more equations did not get rendered due to their size.

Define a new external library target for the package. Has one form:

extern_lib «target-name» (pkg : NPackage _package.name) :=
  /- build term of type `FetchM (Job FilePath)` -/

The pkg parameter (and its type specifier) is optional. It is of type NPackage _package.name to provably demonstrate the package provided is the package in which the target is defined.

The term should build the external library's static library.

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