Documentation

Lake.DSL.Require

The require syntax #

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

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