Documentation

Lake.Load.Config

source
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).

Instances For
    source
    @[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
    Instances For
      source
      @[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
      Instances For
        source
        @[inline]
        def Lake.LoadConfig.lakeDir (cfg : Lake.LoadConfig) :
        Lake.FilePath

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

        Equations
        Instances For