The require syntax

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

def Lake.DSL.fromPath : Lean.ParserDescr

Equations

• Lake.DSL.fromPath = Lean.ParserDescr.nodeWithAntiquot "fromPath" `Lake.DSL.fromPath (Lean.ParserDescr.cat `term 0)

def Lake.DSL.fromGit : Lean.ParserDescr

Equations

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

def Lake.DSL.fromSource : Lean.ParserDescr

Equations

• Lake.DSL.fromSource = Lean.ParserDescr.nodeWithAntiquot "fromSource" `Lake.DSL.fromSource (Lean.ParserDescr.binary `orelse Lake.DSL.fromGit Lake.DSL.fromPath)

def Lake.DSL.fromClause : Lean.ParserDescr

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

• Lake.DSL.fromClause = Lean.ParserDescr.nodeWithAntiquot "fromClause" `Lake.DSL.fromClause (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " from ") Lake.DSL.fromSource)

def Lake.DSL.withClause : Lean.ParserDescr

Equations

• Lake.DSL.withClause = Lean.ParserDescr.nodeWithAntiquot "withClause" `Lake.DSL.withClause (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " with ") (Lean.ParserDescr.cat `term 0))

def Lake.DSL.verSpec : Lean.ParserDescr

Equations

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

def Lake.DSL.verClause : Lean.ParserDescr

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

Equations

• Lake.DSL.verClause = Lean.ParserDescr.nodeWithAntiquot "verClause" `Lake.DSL.verClause (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " @ ") Lake.DSL.verSpec)

def Lake.DSL.depName : Lean.ParserDescr

Equations

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

def Lake.DSL.depSpec : Lean.ParserDescr

Equations

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

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

def Lake.DSL.requireDecl : Lean.ParserDescr

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.

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 } }