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.

Instances For