structure Lake.LoadConfig : Type

Context for loading a Lake configuration.

• lakeEnv : Lake.Env

  The Lake environment of the load process.

• wsDir : Lake.FilePath

  The root directory of the Lake workspace.

• relPkgDir : Lake.FilePath

  The directory of the loaded package (relative to the root).

• relConfigFile : Lake.FilePath

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

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

• 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.pkgDir (cfg : Lake.LoadConfig) : Lake.FilePath

The full path to loaded package's directory.

Equations

• cfg.pkgDir = cfg.wsDir / cfg.relPkgDir

@[inline]

def Lake.LoadConfig.configFile (cfg : Lake.LoadConfig) : Lake.FilePath

The full path to loaded package's configuration file.

Equations

• cfg.configFile = cfg.pkgDir / cfg.relConfigFile

@[inline]

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

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

Equations

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