def Lake.toolchainFileName : Lake.FilePath

elan toolchain file name

Equations

• Lake.toolchainFileName = { toString := "lean-toolchain" }

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 : String

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

Equations

• Lake.defaultManifestFile = "lake-manifest.json"

structure Lake.LoadConfig : Type

Context for loading a Lake configuration.

• env : Lake.Env

  The Lake environment of the load process.

• rootDir : Lake.FilePath

  The root directory of the loaded package (and its workspace).

• configFile : Lake.FilePath

  The Lean file with the package's Lake configuration (e.g., lakefile.lean)

• configOpts : Lake.NameMap String

  A set of key-value Lake configuration options (i.e., -K settings).

• leanOpts : Lean.Options

  The Lean options with which to elaborate the configuration file.

• reconfigure : Bool

  If true, Lake will elaborate configuration files instead of using OLeans.