This module defines the syntax of the Lake DSL. The syntax is defined separately from the elaborator and/or macro definitions to allow clients to import it without crashing Lean. In particular, this allows the reference manual to document the DSL syntax.

def Lake.DSL.dirConst : Lean.ParserDescr

A macro that expands to the path of package's directory during the Lakefile's elaboration.

Equations

• Lake.DSL.dirConst = Lean.ParserDescr.node `Lake.DSL.dirConst 1024 (Lean.ParserDescr.symbol "__dir__")

def Lake.DSL.getConfig : Lean.ParserDescr

A macro that expands to the specified configuration option (or none, if the option has not been set) during the Lakefile's elaboration.

Configuration arguments are set either via the Lake CLI (by the -K option) or via the with clause in a require statement.

Equations

• Lake.DSL.getConfig = Lean.ParserDescr.node `Lake.DSL.getConfig 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "get_config? ") (Lean.ParserDescr.const `ident))

Package Declarations

DSL syntax definitions for packages and hooks.

def Lake.DSL.packageCommand : Lean.ParserDescr

Defines the configuration of a Lake package. Has many forms:

package «pkg-name»
package «pkg-name» { /- config opts -/ }
package «pkg-name» where /- config opts -/

There can only be one package declaration per Lake configuration file. The defined package configuration will be available for reference as _package.

Equations

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

@[reducible, inline]

abbrev Lake.DSL.PackageCommand : Type

Defines the configuration of a Lake package. Has many forms:

package «pkg-name»
package «pkg-name» { /- config opts -/ }
package «pkg-name» where /- config opts -/

There can only be one package declaration per Lake configuration file. The defined package configuration will be available for reference as _package.

Equations

• Lake.DSL.PackageCommand = Lean.TSyntax `Lake.DSL.packageCommand

instance Lake.DSL.instCoePackageCommandCommand : Coe PackageCommand Lean.Command

Equations

• Lake.DSL.instCoePackageCommandCommand = { coe := fun (x : Lake.DSL.PackageCommand) => { raw := x.raw } }

def Lake.DSL.postUpdateDecl : Lean.ParserDescr

Declare a post-lake update hook for the package. Runs the monadic action is after a successful lake update execution in this package or one of its downstream dependents.

Example

This feature enables Mathlib to synchronize the Lean toolchain and run cache get after a lake update:

lean_exe cache
post_update pkg do
  let wsToolchainFile := (← getRootPackage).dir / "lean-toolchain"
  let mathlibToolchain ← IO.FS.readFile <| pkg.dir / "lean-toolchain"
  IO.FS.writeFile wsToolchainFile mathlibToolchain
  let exeFile ← runBuild cache.fetch
  let exitCode ← env exeFile.toString #["get"]
  if exitCode ≠ 0 then
    error s!"{pkg.name}: failed to fetch cache"

Equations

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

The require syntax

This is the require DSL syntax used to specify package dependencies.

def Lake.DSL.fromPath : Lean.ParserDescr

Equations

• Lake.DSL.fromPath = Lean.ParserDescr.nodeWithAntiquot "fromPath" `Lake.DSL.fromPath (Lean.ParserDescr.cat `term 0)

def Lake.DSL.fromGit : Lean.ParserDescr

Equations

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

def Lake.DSL.fromSource : Lean.ParserDescr

Equations

• Lake.DSL.fromSource = Lean.ParserDescr.nodeWithAntiquot "fromSource" `Lake.DSL.fromSource (Lean.ParserDescr.binary `orelse Lake.DSL.fromGit Lake.DSL.fromPath)

def Lake.DSL.fromClause : Lean.ParserDescr

Specifies a specific source from which to draw the package dependency. Dependencies that are downloaded from a remote source will be placed into the workspace's packagesDir.

Path Dependencies

from <path>

Lake loads the package located a fixed path relative to the requiring package's directory.

Git Dependencies

from git <url> [@ <rev>] [/ <subDir>]

Lake clones the Git repository available at the specified fixed Git url, and checks out the specified revision rev. The revision can be a commit hash, branch, or tag. If none is provided, Lake defaults to master. After checkout, Lake loads the package located in subDir (or the repository root if no subdirectory is specified).

Equations

• Lake.DSL.fromClause = Lean.ParserDescr.nodeWithAntiquot "fromClause" `Lake.DSL.fromClause (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " from ") Lake.DSL.fromSource)

def Lake.DSL.withClause : Lean.ParserDescr

Equations

• Lake.DSL.withClause = Lean.ParserDescr.nodeWithAntiquot "withClause" `Lake.DSL.withClause (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " with ") (Lean.ParserDescr.cat `term 0))

def Lake.DSL.verSpec : Lean.ParserDescr

Equations

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

def Lake.DSL.verClause : Lean.ParserDescr

The version of the package to require. To specify a Git revision, use the syntax @ git <rev>.

Equations

• Lake.DSL.verClause = Lean.ParserDescr.nodeWithAntiquot "verClause" `Lake.DSL.verClause (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " @ ") Lake.DSL.verSpec)

def Lake.DSL.depName : Lean.ParserDescr

Equations

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

def Lake.DSL.depSpec : Lean.ParserDescr

Equations

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

def Lake.DSL.requireDecl : Lean.ParserDescr

Adds a new package dependency to the workspace. The general syntax is:

require ["<scope>" /] <pkg-name> [@ <version>]
  [from <source>] [with <options>]

The from clause tells Lake where to locate the dependency. See the fromClause syntax documentation (e.g., hover over it) to see the different forms this clause can take.

Without a from clause, Lake will lookup the package in the default registry (i.e., Reservoir) and use the information there to download the package at the requested version. The scope is used to disambiguate between packages in the registry with the same pkg-name. In Reservoir, this scope is the package owner (e.g., leanprover of @leanprover/doc-gen4).

The with clause specifies a NameMap String of Lake options used to configure the dependency. This is equivalent to passing -K options to the dependency on the command line.

Equations

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

@[reducible, inline]

abbrev Lake.DSL.RequireDecl : Type

Adds a new package dependency to the workspace. The general syntax is:

require ["<scope>" /] <pkg-name> [@ <version>]
  [from <source>] [with <options>]

The from clause tells Lake where to locate the dependency. See the fromClause syntax documentation (e.g., hover over it) to see the different forms this clause can take.

Without a from clause, Lake will lookup the package in the default registry (i.e., Reservoir) and use the information there to download the package at the requested version. The scope is used to disambiguate between packages in the registry with the same pkg-name. In Reservoir, this scope is the package owner (e.g., leanprover of @leanprover/doc-gen4).

The with clause specifies a NameMap String of Lake options used to configure the dependency. This is equivalent to passing -K options to the dependency on the command line.

Equations

• Lake.DSL.RequireDecl = Lean.TSyntax `Lake.DSL.requireDecl

instance Lake.DSL.instCoeRequireDeclCommand : Coe RequireDecl Lean.Command

Equations

• Lake.DSL.instCoeRequireDeclCommand = { coe := fun (x : Lake.DSL.RequireDecl) => { raw := x.raw } }

DSL for Targets & Facets

Syntax for declaring Lake targets and facets.

def Lake.DSL.buildDeclSig : Lean.ParserDescr

Equations

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

Facet Declarations

def Lake.DSL.moduleFacetDecl : Lean.ParserDescr

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.

def Lake.DSL.packageFacetDecl : Lean.ParserDescr

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.

def Lake.DSL.libraryFacetDecl : Lean.ParserDescr

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

def Lake.DSL.targetCommand : Lean.ParserDescr

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

def Lake.DSL.leanLibCommand : Lean.ParserDescr

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]

abbrev Lake.DSL.LeanLibCommand : Type

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

• Lake.DSL.LeanLibCommand = Lean.TSyntax `Lake.DSL.leanLibCommand

instance Lake.DSL.instCoeLeanLibCommandCommand : Coe LeanLibCommand Lean.Command

Equations

• Lake.DSL.instCoeLeanLibCommandCommand = { coe := fun (x : Lake.DSL.LeanLibCommand) => { raw := x.raw } }

def Lake.DSL.leanExeCommand : Lean.ParserDescr

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]

abbrev Lake.DSL.LeanExeCommand : Type

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

• Lake.DSL.LeanExeCommand = Lean.TSyntax `Lake.DSL.leanExeCommand

instance Lake.DSL.instCoeLeanExeCommandCommand : Coe LeanExeCommand Lean.Command

Equations

• Lake.DSL.instCoeLeanExeCommandCommand = { coe := fun (x : Lake.DSL.LeanExeCommand) => { raw := x.raw } }

def Lake.DSL.inputFileCommand : Lean.ParserDescr

Define a new input file target for the package. Can optionally be provided with a configuration of type InputFileConfig.

Equations

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

@[reducible, inline]

abbrev Lake.DSL.InputFileCommand : Type

Define a new input file target for the package. Can optionally be provided with a configuration of type InputFileConfig.

Equations

• Lake.DSL.InputFileCommand = Lean.TSyntax `Lake.DSL.inputFileCommand

instance Lake.DSL.instCoeInputFileCommandCommand : Coe InputFileCommand Lean.Command

Equations

• Lake.DSL.instCoeInputFileCommandCommand = { coe := fun (x : Lake.DSL.InputFileCommand) => { raw := x.raw } }

def Lake.DSL.inputDirCommand : Lean.ParserDescr

Define a new input directory target for the package. Can optionally be provided with a configuration of type InputDirConfig.

Equations

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

@[reducible, inline]

abbrev Lake.DSL.InputDirCommand : Type

Define a new input directory target for the package. Can optionally be provided with a configuration of type InputDirConfig.

Equations

• Lake.DSL.InputDirCommand = Lean.TSyntax `Lake.DSL.inputDirCommand

instance Lake.DSL.instCoeInputDirCommandCommand : Coe InputDirCommand Lean.Command

Equations

• Lake.DSL.instCoeInputDirCommandCommand = { coe := fun (x : Lake.DSL.InputDirCommand) => { raw := x.raw } }

External Library Target Declaration

def Lake.DSL.externLibDeclSpec : Lean.ParserDescr

Equations

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

def Lake.DSL.externLibCommand : Lean.ParserDescr

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.

Script Declarations

DSL definitions to define a Lake script for a package.

def Lake.DSL.scriptDeclSpec : Lean.ParserDescr

Equations

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

def Lake.DSL.scriptDecl : Lean.ParserDescr

Define a new Lake script for the package.

Example

/-- Display a greeting -/
script «script-name» (args) do
  if h : 0 < args.length then
    IO.println s!"Hello, {args[0]'h}!"
  else
    IO.println "Hello, world!"
  return 0

Equations

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

Version Literals

Defines the v!"<ver>" syntax for version literals.

def Lake.DSL.verLit : Lean.ParserDescr

A Lake version literal.

Equations

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

DSL for Build Key

Notation for specifying build keys in a package.

def Lake.DSL.facetSuffix : Lean.ParserDescr

Equations

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

def Lake.DSL.packageTargetLit : Lean.ParserDescr

Equations

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

def Lake.DSL.moduleTargetKeyLit : Lean.ParserDescr

A module target key literal (with optional facet).

Equations

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

def Lake.DSL.packageTargetKeyLit : Lean.ParserDescr

A package target key literal (with optional facet).

Equations

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

Elaboration-Time Control Flow

Syntax for elaboration time control flow.

def Lake.DSL.cmdDo : Lean.ParserDescr

The do command syntax groups multiple similarly indented commands together. The group can then be passed to another command that usually only accepts a single command (e.g., meta if).

Equations

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

def Lake.DSL.metaIf : Lean.ParserDescr

The meta if command has two forms:

meta if <c:term> then <a:command>
meta if <c:term> then <a:command> else <b:command>

It expands to the command a if the term c evaluates to true (at elaboration time). Otherwise, it expands to command b (if an else clause is provided).

One can use this command to specify, for example, external library targets only available on specific platforms:

meta if System.Platform.isWindows then
extern_lib winOnlyLib := ...
else meta if System.Platform.isOSX then
extern_lib macOnlyLib := ...
else
extern_lib linuxOnlyLib := ...

Equations

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

def Lake.DSL.runIO : Lean.ParserDescr

Executes a term of type IO α at elaboration-time and produces an expression corresponding to the result via ToExpr α.

Equations

• Lake.DSL.runIO = Lean.ParserDescr.node `Lake.DSL.runIO 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "run_io ") (Lean.ParserDescr.const `doSeq))