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.

@[implicit_reducible]

instance Lake.instInhabitedInputVer : Inhabited InputVer

Equations

• Lake.instInhabitedInputVer = { default := Lake.instInhabitedInputVer.default }

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

Equations

• One or more equations did not get rendered due to their size.
• Lake.instReprInputVer.repr Lake.InputVer.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lake.InputVer.none")).group prec✝

@[implicit_reducible]

instance Lake.instReprInputVer : Repr InputVer

Equations

• Lake.instReprInputVer = { reprPrec := Lake.instReprInputVer.repr }

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

Equations

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

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

Equations

• Lake.InputVer.none.toString? = none
• (Lake.InputVer.git a).toString? = some (toString "git#" ++ toString a)
• (Lake.InputVer.ver a).toString? = some a.toString

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 GitRev) (subDir : Option System.FilePath) : DependencySrc

@[implicit_reducible]

instance Lake.instInhabitedDependencySrc : Inhabited DependencySrc

Equations

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

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

Equations

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

@[implicit_reducible]

instance Lake.instReprDependencySrc : Repr DependencySrc

Equations

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

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.

@[implicit_reducible]

instance Lake.instInhabitedDependency : Inhabited Dependency

Equations

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

@[implicit_reducible]

instance Lake.instTypeNameDependency : TypeName Dependency

Equations

• Lake.instTypeNameDependency = Lake.inst✝

@[inline]

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

Returns the directory name used for storing the materialized dependency.

Equations

• dep.dirName = dep.name.toString false

@[inline]

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

Returns the name of the dependency formatted for printing.

Equations

• dep.prettyName = dep.name.toString false

@[inline]

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

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

Equations

• dep.reservoirName = dep.name.toString false

@[inline]

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

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

Equations

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

@[inline]

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

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

Equations

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