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" }

def Lake.defaultConfigFile : Lake.FilePath

The default name of the Lake configuration file (i.e., lakefile.lean).

Equations

• Lake.defaultConfigFile = { toString := "lakefile.lean" }

def Lake.defaultManifestFile : Lake.FilePath

The default name of the Lake manifest file (i.e., lake-manifest.json).

Equations

• Lake.defaultManifestFile = { toString := "lake-manifest.json" }

def Lake.defaultBuildDir : Lake.FilePath

The default build directory for packages (i.e., .lake/build).

Equations

• Lake.defaultBuildDir = Lake.defaultLakeDir / { toString := "build" }

def Lake.defaultLeanLibDir : Lake.FilePath

The default Lean library directory for packages.

Equations

• Lake.defaultLeanLibDir = { toString := "lib" }

def Lake.defaultNativeLibDir : Lake.FilePath

The default native library directory for packages.

Equations

• Lake.defaultNativeLibDir = { toString := "lib" }

def Lake.defaultBinDir : Lake.FilePath

The default binary directory for packages.

Equations

• Lake.defaultBinDir = { toString := "bin" }

def Lake.defaultIrDir : Lake.FilePath

The default IR directory for packages.

Equations

• Lake.defaultIrDir = { toString := "ir" }