inductive Lake.Source : Type

The src of a Dependency.

In Lake, dependency sources currently come into flavors:

• Local paths relative to the package's directory.
• Remote git repositories that are download from a given url into the workspace's packagesDir.

• path: Lake.FilePath → Lake.Source
• git: String → Option String → Option Lake.FilePath → Lake.Source

instance Lake.instInhabitedSource : Inhabited Lake.Source

Equations

• Lake.instInhabitedSource = { default := Lake.Source.path default }

instance Lake.instReprSource : Repr Lake.Source

Equations

• Lake.instReprSource = { reprPrec := Lake.reprSource✝ }

structure Lake.Dependency : Type

A Dependency of a package.

• name : Lake.Name

  A Name for the dependency. The names of a package's dependencies cannot clash.

• src : Lake.Source

  The source of a dependency. See the documentation of Source for more information.

• opts : Lake.NameMap String

  Arguments to pass to the dependency's package configuration.

instance Lake.instInhabitedDependency : Inhabited Lake.Dependency

Equations

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