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.

Equations

• cfg.showProgress = decide (cfg.noBuild = true ∧ (cfg.verbosity == Lake.Verbosity.verbose) = true ∨ (cfg.verbosity != Lake.Verbosity.quiet) = true)

def Lake.JobQueue : Type

Mutable reference of registered build jobs.

Equations

• Lake.JobQueue = IO.Ref (Array Lake.OpaqueJob)

@[inline]

def Lake.mkJobQueue : BaseIO JobQueue

Returns a new empty job queue.

Equations

• Lake.mkJobQueue = IO.mkRef #[]

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.

Equations

• Lake.BuildT = ReaderT Lake.BuildContext

@[reducible, inline]

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

A monad equipped with a Lake build context.

Equations

• Lake.MonadBuild m = MonadReaderOf Lake.BuildContext m

@[implicit_reducible]

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

Equations

• Lake.instMonadLiftLakeMBuildTOfPure = { monadLift := fun {α : Type} (x : Lake.LakeM α) (ctx : Lake.BuildContext) => pure (Lake.LakeM.run ctx.toContext x) }

@[inline]

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

Equations

• Lake.getBuildContext = readThe Lake.BuildContext

@[inline]

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

Equations

• Lake.getLeanTrace = (fun (x : Lake.BuildContext) => x.leanTrace) <$> Lake.getBuildContext

@[inline]

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

Equations

• Lake.getBuildConfig = (fun (x : Lake.BuildContext) => x.toBuildConfig) <$> Lake.getBuildContext

@[inline]

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

Equations

• Lake.getIsOldMode = (fun (x : Lake.BuildConfig) => x.oldMode) <$> Lake.getBuildConfig

@[inline]

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

Equations

• Lake.getTrustHash = (fun (x : Lake.BuildConfig) => x.trustHash) <$> Lake.getBuildConfig

@[inline]

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

Equations

• Lake.getNoBuild = (fun (x : Lake.BuildConfig) => x.noBuild) <$> Lake.getBuildConfig

@[inline]

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

Equations

• Lake.getVerbosity = (fun (x : Lake.BuildConfig) => x.verbosity) <$> Lake.getBuildConfig

@[inline]

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

Equations

• Lake.getIsVerbose = (fun (x : Lake.Verbosity) => x == Lake.Verbosity.verbose) <$> Lake.getVerbosity

@[inline]

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

Equations

• Lake.getIsQuiet = (fun (x : Lake.Verbosity) => x == Lake.Verbosity.quiet) <$> Lake.getVerbosity

@[inline]

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

Equations

• Lake.getLeanOptOverrides = (fun (x : Lake.BuildConfig) => x.leanOptOverrides) <$> Lake.getBuildConfig