structure Lake.LoadConfig : Type

Context for loading a Lake configuration.

• lakeEnv : Env

  The Lake environment of the load process.

• lakeArgs? : Option (Array String)

  The CLI arguments Lake was run with. Used to perform a restart of Lake on a toolchain update. A value of none means that Lake is not restartable via the CLI.

• wsDir : System.FilePath

  The absolute path to the root directory of the Lake workspace.

• relPkgDir : System.FilePath

  The loaded package's directory (relative to the workspace directory).

• pkgDir : System.FilePath

  The absolute path to the loaded package's directory.

• relConfigFile : System.FilePath

  The package's Lake configuration file (relative to its directory).

• configFile : System.FilePath

  The full path to the loaded package's Lake configuration file.

• packageOverrides : Array PackageEntry

  Additional package overrides for this workspace load.

• lakeOpts : Lean.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

  Whether Lake should re-elaborate configuration files instead of using cached OLeans.

• updateDeps : Bool

  Whether to update dependencies when loading the workspace.

• updateToolchain : Bool

  Whether to update the workspace's lean-toolchain when dependencies are updated. If true and a toolchain update occurs, Lake will need to be restarted.

• scope : String

  The package's scope (e.g., in Reservoir).

• remoteUrl : String

  The URL to this package's Git remote (if any).

@[inline]

def Lake.LoadConfig.lakeDir (cfg : LoadConfig) : System.FilePath

The package's Lake directory (for Lake temporary files).

Equations

• cfg.lakeDir = cfg.pkgDir / Lake.defaultLakeDir