inductive Lake.InputVer : Type

A version targeted by a dependency (e.g., in a require).

• none : InputVer

  No version was specified.

• git (rev : GitRev) : InputVer

  A Git revision to resolve to a commit hash.

  This is specified by an @ git <rev> clause in Lean or rev = <rev> field in TOML.

• ver (ver : VerRange) : InputVer

  A semantic version range of acceptable versions.

  This is specified by an @ <ver> clause in Lean or version = <ver> field in TOML.

@[instance_reducible]

instance Lake.instInhabitedInputVer : Inhabited InputVer

def Lake.instReprInputVer.repr : InputVer → Nat → Std.Format

@[instance_reducible]

instance Lake.instReprInputVer : Repr InputVer

def Lake.InputVer.parse (ver : String) : Except String InputVer

def Lake.InputVer.toString? (self : InputVer) : Option String

inductive Lake.DependencySrc : Type

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

• path (dir : System.FilePath) : DependencySrc

  A package located at a fixed path relative to the dependent package's directory.

• git (url : String) (rev : Option GitRev) (subDir : Option System.FilePath) : DependencySrc

  A package cloned from a Git repository available at a fixed Git url.

@[instance_reducible]

instance Lake.instInhabitedDependencySrc : Inhabited DependencySrc

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

@[instance_reducible]

instance Lake.instReprDependencySrc : Repr 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 : InputVer

  The target version of the dependency.

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

@[instance_reducible]

instance Lake.instInhabitedDependency : Inhabited Dependency

@[instance_reducible]

instance Lake.instTypeNameDependency : TypeName Dependency

@[inline]

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

Returns the directory name used for storing the materialized dependency.

@[inline]

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

Returns the name of the dependency formatted for printing.

@[inline]

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

Returns the name of the dependency formatted for lookup on Reservoir.

@[inline]

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

Returns the full name of the dependency (i.e., <scope>/<name>) formatted for printing.

@[inline]

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

Returns a printable string which uniquely identifies this dependency for the resolver.