def Lake.defaultLakeDir : System.FilePath

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

def Lake.defaultPackagesDir : System.FilePath

The default setting for a WorkspaceConfig's packagesDir option.

def Lake.defaultConfigFile : System.FilePath

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

def Lake.defaultLeanConfigFile : System.FilePath

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

def Lake.defaultTomlConfigFile : System.FilePath

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

def Lake.defaultManifestFile : System.FilePath

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

def Lake.defaultBuildDir : System.FilePath

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

def Lake.defaultLeanLibDir : System.FilePath

The default Lean library directory for packages.

def Lake.defaultNativeLibDir : System.FilePath

The default native library directory for packages.

def Lake.defaultBinDir : System.FilePath

The default binary directory for packages.

def Lake.defaultIrDir : System.FilePath

The default IR directory for packages.