def Lake.defaultPackagesDir : Lake.FilePath

The default setting for a WorkspaceConfig's packagesDir option.

structure Lake.WorkspaceConfig : Type

• packagesDir : Option 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

instance Lake.instReprWorkspaceConfig : Repr Lake.WorkspaceConfig