The require syntax

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

def Lake.DSL.expandDepSpec (stx : Lean.TSyntax `Lake.DSL.depSpec) (doc? : Option DocComment) : Lean.MacroM Lean.Command

def Lake.DSL.expandRequireDecl : Lean.Macro

Equations

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

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

instance Lake.DSL.instCoeRequireDeclCommand : Coe RequireDecl Lean.Command

Equations

• Lake.DSL.instCoeRequireDeclCommand = { coe := fun (x : Lake.DSL.RequireDecl) => { raw := x.raw } }