Documentation

Lake.DSL.Syntax

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.

source
def Lake.DSL.dirConst :
Lean.ParserDescr

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

Equations
source
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

Package Declarations #

DSL syntax definitions for packages and hooks.

source
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.
source
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.

source
def Lake.DSL.fromPath :
Lean.ParserDescr
Equations
source
def Lake.DSL.fromGit :
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lake.DSL.fromSource :
Lean.ParserDescr
Equations
source
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
source
def Lake.DSL.withClause :
Lean.ParserDescr
Equations
source
def Lake.DSL.verSpec :
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lake.DSL.verClause :
Lean.ParserDescr

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

Equations
source
def Lake.DSL.depName :
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lake.DSL.depSpec :
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
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.

DSL for Targets & Facets #

Syntax for declaring Lake targets and facets.

source
def Lake.DSL.buildDeclSig :
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.

Facet Declarations #

source
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.
source
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.
source
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 #

source
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 #

source
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.
source
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.
source
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.
source
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.

External Library Target Declaration #

source
def Lake.DSL.externLibDeclSpec :
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
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.

source
def Lake.DSL.scriptDeclSpec :
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
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.

source
def Lake.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.

source
def Lake.DSL.facetSuffix :
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lake.DSL.packageTargetLit :
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lake.DSL.«term`+___» :
Lean.ParserDescr

A module target key literal (with optional facet).

Equations
  • One or more equations did not get rendered due to their size.
source
def Lake.DSL.«term`@___/____» :
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.

source
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.
source
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.
source
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