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

      The version of the package to lookup in Lake's package index. A Git revision can be specified via "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
            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 specified version. The optional scope is used to disambiguate which package with pkg-name to lookup. 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 specified version. The optional scope is used to disambiguate which package with pkg-name to lookup. 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