Lake.Config.Defaults

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

Instances For

source

def Lake.defaultPackagesDir :

System.FilePath

The default setting for a WorkspaceConfig's packagesDir option.

Instances For

source

def Lake.defaultConfigFile :

System.FilePath

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

Instances For

source

def Lake.defaultLeanConfigFile :

System.FilePath

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

Equations

Lake.defaultLeanConfigFile = Lake.defaultConfigFile.addExtension "lean"

Instances For

source

def Lake.defaultTomlConfigFile :

System.FilePath

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

Equations

Lake.defaultTomlConfigFile = Lake.defaultConfigFile.addExtension "toml"

Instances For

source

def Lake.defaultManifestFile :

System.FilePath

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

Equations

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

Instances For

source

def Lake.defaultBuildDir :

System.FilePath

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

Instances For

source

def Lake.defaultLeanLibDir :

System.FilePath

The default Lean library directory for packages.

Equations

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

Instances For

source

def Lake.defaultNativeLibDir :

System.FilePath

The default native library directory for packages.

Instances For

source

def Lake.defaultBinDir :

System.FilePath

The default binary directory for packages.

Instances For

source

def Lake.defaultIrDir :

System.FilePath

The default IR directory for packages.

Instances For