def Lake.defaultPackagesDir : Lake.FilePath

The default setting for a WorkspaceConfig's packagesDir option.

Equations

• Lake.defaultPackagesDir = { toString := "lake-packages" }

structure Lake.WorkspaceConfig : Type

• packagesDir : Lake.FilePath

  The directory to which Lake should download remote dependencies. Defaults to defaultPackagesDir (i.e., lake-packages).

A Workspace's declarative configuration.

instance Lake.instInhabitedWorkspaceConfig : Inhabited Lake.WorkspaceConfig

Equations

• Lake.instInhabitedWorkspaceConfig = { default := { packagesDir := default } }

instance Lake.instReprWorkspaceConfig : Repr Lake.WorkspaceConfig

Equations

• Lake.instReprWorkspaceConfig = { reprPrec := Lake.reprWorkspaceConfig✝ }