def Lake.DSL.fromPath : Lean.ParserDescr

def Lake.DSL.fromGit : Lean.ParserDescr

def Lake.DSL.depSpec : Lean.ParserDescr

def Lake.DSL.expandDepSpec : Lean.TSyntax `Lake.DSL.depSpec → Lean.MacroM Lean.Command

def Lake.DSL.requireDecl : Lean.ParserDescr

Adds a new package dependency to the workspace. Has two forms:

require foo from "path"/"to"/"local"/"package" with NameMap.empty
require bar from git "url.git"@"rev"/"optional"/"path-to"/"dir-with-pkg"

Either form supports the optional with clause. The @"rev" and /"path"/"dir" parts of the git form of require are optional.

The elements of both the from and with clauses are proper terms so normal computation is supported within them (though parentheses made be required to disambiguate the syntax).