structure Lake.BuildConfigextends Lake.LogConfig : Type

Configuration options for a Lake build.

• failLv : LogLevel
• outLv : LogLevel
• ansiMode : AnsiMode
• out : OutStream
• oldMode : Bool

  Use modification times for trace checking.

• trustHash : Bool

  Whether to trust .hash files.

• noBuild : Bool

  Early exit if a target has to be rebuilt.

• verbosity : Verbosity

  Verbosity level (-q, -v, or neither).

• showSuccess : Bool

  Whether to print a message when the build finishes successfully (if not quiet).

• outputsFile? : Option System.FilePath

  File to save input-to-output mappings from the build of the workspace's root

• leanOptOverrides : Lean.NameMap Lean.LeanOptions

  Per-package Lean option overrides, applied to every module whose owning package's baseName appears as a key. When recFetchSetup builds module M, the LeanOptions associated with M.pkg.baseName (if any) are appended to M.leanOptions, overriding clashing entries.

  Used by lake lint to inject linter.extra/linter.all into every module of a target package (so transitively-imported first-party modules capture linter-tagged warnings), without touching dependencies.

def Lake.BuildConfig.showProgress (cfg : BuildConfig) : Bool

Whether the build should show progress information.

Verbosity.quiet hides progress and, for a noBuild, Verbosity.verbose shows progress.

def Lake.JobQueue : Type

Mutable reference of registered build jobs.

@[inline]

def Lake.mkJobQueue : BaseIO JobQueue

Returns a new empty job queue.

structure Lake.BuildContextextends Lake.BuildConfig, Lake.Context : Type

A Lake context with a build configuration and additional build data.

• failLv : LogLevel
• outLv : LogLevel
• ansiMode : AnsiMode
• out : OutStream
• oldMode : Bool
• trustHash : Bool
• noBuild : Bool
• verbosity : Verbosity
• showSuccess : Bool
• outputsFile? : Option System.FilePath
• leanOptOverrides : Lean.NameMap Lean.LeanOptions
• opaqueWs : OpaqueWorkspace
• leanTrace : BuildTrace
• registeredJobs : JobQueue
• outputsRef? : Option CacheRef

  Input-to-output(s) map for hashes of the root package's artifacts. If none, tracking outputs is disabled for this build.

@[reducible, inline]

abbrev Lake.BuildT (m : Type → Type u_1) (α : Type) : Type u_1

A transformer to equip a monad with a BuildContext.

@[reducible, inline]

abbrev Lake.MonadBuild (m : Type → Type u) : Type u

A monad equipped with a Lake build context.

@[implicit_reducible]

instance Lake.instMonadLiftLakeMBuildTOfPure {m : Type → Type u_1} [Pure m] : MonadLift LakeM (BuildT m)

@[inline]

def Lake.getBuildContext {m : Type → Type u_1} [MonadBuild m] : m BuildContext

@[inline]

def Lake.getLeanTrace {m : Type → Type u_1} [Functor m] [MonadBuild m] : m BuildTrace

@[inline]

def Lake.getBuildConfig {m : Type → Type u_1} [Functor m] [MonadBuild m] : m BuildConfig

@[inline]

def Lake.getIsOldMode {m : Type → Type u_1} [Functor m] [MonadBuild m] : m Bool

@[inline]

def Lake.getTrustHash {m : Type → Type u_1} [Functor m] [MonadBuild m] : m Bool

@[inline]

def Lake.getNoBuild {m : Type → Type u_1} [Functor m] [MonadBuild m] : m Bool

@[inline]

def Lake.getVerbosity {m : Type → Type u_1} [Functor m] [MonadBuild m] : m Verbosity

@[inline]

def Lake.getIsVerbose {m : Type → Type u_1} [Functor m] [MonadBuild m] : m Bool

@[inline]

def Lake.getIsQuiet {m : Type → Type u_1} [Functor m] [MonadBuild m] : m Bool

@[inline]

def Lake.getLeanOptOverrides {m : Type → Type u_1} [Functor m] [MonadBuild m] : m (Lean.NameMap Lean.LeanOptions)