inductive Lake.DependencySrc : Type

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

• path: System.FilePath → Lake.DependencySrc
• git: String → Option String → Option System.FilePath → Lake.DependencySrc

instance Lake.instInhabitedDependencySrc : Inhabited Lake.DependencySrc

instance Lake.instReprDependencySrc : Repr Lake.DependencySrc

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 Lake.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.

instance Lake.instInhabitedDependency : Inhabited Lake.Dependency

Equations

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

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

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

Equations

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