def Lake.defaultLakeDir : Lake.FilePath

The default directory to output Lake-related files (e.g., build artifacts, packages, caches, etc.). Currently not configurable.

Equations

• Lake.defaultLakeDir = { toString := ".lake" }

def Lake.defaultPackagesDir : Lake.FilePath

The default setting for a WorkspaceConfig's packagesDir option.

Equations

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

structure Lake.WorkspaceConfig : Type

A Workspace's declarative configuration.

• packagesDir : Lake.FilePath

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

instance Lake.instInhabitedWorkspaceConfig : Inhabited Lake.WorkspaceConfig

Equations

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

instance Lake.instReprWorkspaceConfig : Repr Lake.WorkspaceConfig

Equations

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