Documentation

Lake.DSL.Require

The require syntax #

This module contains the macro definition of the require DSL syntax used to specify package dependencies.

Equations
  • One or more equations did not get rendered due to their size.
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
      • One or more equations did not get rendered due to their size.
      Instances For

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

        Equations
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            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
              • One or more equations did not get rendered due to their size.
              Instances For
                @[reducible, inline]

                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