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.nameConst :
Lean.ParserDescr

A macro that expands to the assigned name of package during the Lakefile's elaboration.

Equations

- Lake.DSL.nameConst = Lean.ParserDescr.node `Lake.DSL.nameConst 1024 (Lean.ParserDescr.symbol "__name__")

Instances For

source
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__")

Instances For

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

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

Instances For

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

Instances For

source
@[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

Instances For

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

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

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.

Instances For

# The `require` syntax #

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

source
def Lake.DSL.fromPath :
Lean.ParserDescr
Equations

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

Instances For

source
def Lake.DSL.fromGit :
Lean.ParserDescr
Equations

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

Instances For

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

Instances For

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

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

Instances For

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

Instances For

source
def Lake.DSL.verSpec :
Lean.ParserDescr
Equations

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

Instances For

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

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

Instances For

source
def Lake.DSL.depName :
Lean.ParserDescr
Equations

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

Instances For

source
def Lake.DSL.depSpec :
Lean.ParserDescr
Equations

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

Instances For

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.

Instances For

source
@[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

Instances For

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

source
def Lake.DSL.buildDeclSig :
Lean.ParserDescr
Equations

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

Instances For

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

Instances For

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.

Instances For

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.

Instances For

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

Instances For

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

Instances For

source
@[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

Instances For

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

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

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.

Instances For

source
@[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

Instances For

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

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

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.

Instances For

source
@[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

Instances For

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

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

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.

Instances For

source
@[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

Instances For

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

source
def Lake.DSL.externLibDeclSpec :
Lean.ParserDescr
Equations

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

Instances For

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.

Instances For

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

Instances For

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.

Instances For

# Version Literals #

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

source
def Lake.DSL.verLit :
Lean.ParserDescr

A Lake version literal.

Equations

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

Instances For

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

Instances For

source
def Lake.DSL.packageTargetLit :
Lean.ParserDescr
Equations

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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.

Instances For

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

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

Instances For