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.

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

Equations
    Instances For

      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
        Instances For

          Package Declarations #

          DSL syntax definitions for packages and hooks.

          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
            Instances For

              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
                Instances For

                  The require syntax #

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

                  Equations
                    Instances For
                      Equations
                        Instances For
                          Equations
                            Instances For

                              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
                                Instances For
                                  Equations
                                    Instances For
                                      Equations
                                        Instances For

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

                                          Equations
                                            Instances For
                                              Equations
                                                Instances For
                                                  Equations
                                                    Instances For

                                                      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
                                                        Instances For

                                                          DSL for Targets & Facets #

                                                          Syntax for declaring Lake targets and facets.

                                                          Facet Declarations #

                                                          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
                                                            Instances For

                                                              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
                                                                Instances For

                                                                  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
                                                                    Instances For

                                                                      Custom Target Declaration #

                                                                      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
                                                                        Instances For

                                                                          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
                                                                            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
                                                                                Instances For

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

                                                                                  Equations
                                                                                    Instances For

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

                                                                                      Equations
                                                                                        Instances For

                                                                                          External Library Target Declaration #

                                                                                          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
                                                                                            Instances For

                                                                                              Script Declarations #

                                                                                              DSL definitions to define a Lake script for a package.

                                                                                              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
                                                                                                Instances For

                                                                                                  Version Literals #

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

                                                                                                  A Lake version literal.

                                                                                                  Equations
                                                                                                    Instances For

                                                                                                      DSL for Build Key #

                                                                                                      Notation for specifying build keys in a package.

                                                                                                      Equations
                                                                                                        Instances For

                                                                                                          A module target key literal (with optional facet).

                                                                                                          Equations
                                                                                                            Instances For

                                                                                                              A package target key literal (with optional facet).

                                                                                                              Equations
                                                                                                                Instances For

                                                                                                                  Elaboration-Time Control Flow #

                                                                                                                  Syntax for elaboration time control flow.

                                                                                                                  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
                                                                                                                    Instances For

                                                                                                                      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
                                                                                                                        Instances For

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

                                                                                                                          Equations
                                                                                                                            Instances For