source
inductive Lake.DependencySrc :
Type

The source of a `Dependency`. That is, where Lake should look to materialize the dependency.

- path (dir : System.FilePath) : DependencySrc
- git (url : String) (rev : Option String) (subDir : Option System.FilePath) : DependencySrc

Instances For

source
def Lake.instInhabitedDependencySrc.default :
DependencySrc
Equations

- Lake.instInhabitedDependencySrc.default = Lake.DependencySrc.path default

Instances For

source
instance Lake.instInhabitedDependencySrc :
Inhabited DependencySrc
Equations

- Lake.instInhabitedDependencySrc = { default := Lake.instInhabitedDependencySrc.default }

source
def Lake.instReprDependencySrc.repr :
DependencySrc → Nat → Std.Format
Equations

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

Instances For

source
instance Lake.instReprDependencySrc :
Repr DependencySrc
Equations

- Lake.instReprDependencySrc = { reprPrec := Lake.instReprDependencySrc.repr }

source
structure Lake.Dependency :
Type

A `Dependency` of a package. It specifies a package which another package depends on. This encodes the information contained in the `require` DSL syntax.

- name : Lean.Name

  The package name of the dependency. This name must match the one declared in its configuration file, as that name is used to index its target data types. For this reason, the package name must also be unique across packages in the dependency graph.

- scope : String

  An additional qualifier used to distinguish packages of the same name in a Lake registry. On Reservoir, this is the package owner.

- version? : Option String

  The target version of the dependency. A Git revision can be specified with the syntax `git#<rev>`.

- src? : Option DependencySrc

  The source of a dependency. If none, looks up the dependency in the default registry (e.g., Reservoir). See the documentation of `DependencySrc` for supported sources.

- opts : Lean.NameMap String

  Arguments to pass to the dependency's package configuration.

Instances For

source
def Lake.instInhabitedDependency.default :
Dependency
Equations

- Lake.instInhabitedDependency.default = { name := default, scope := default, version? := default, src? := default, opts := default }

Instances For

source
instance Lake.instInhabitedDependency :
Inhabited Dependency
Equations

- Lake.instInhabitedDependency = { default := Lake.instInhabitedDependency.default }

source
instance Lake.instTypeNameDependency :
TypeName Dependency
Equations

- Lake.instTypeNameDependency = Lake.inst✝

source
def Lake.Dependency.fullName (dep : Dependency) :
String

The full name of a dependency (i.e., `<scope>/<name>`)

Equations

- dep.fullName = toString dep.scope ++ toString "/" ++ toString dep.name.toString

Instances For