def Lake.noBuildCode : Lake.ExitCode

Exit code to return if --no-build is set and a build is required.

Equations

• Lake.noBuildCode = 3

structure Lake.BuildConfig : Type

Configuration options for a Lake build.

• 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 : Lake.Verbosity

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

• failLv : Lake.LogLevel

  Fail the top-level build if entries of at least this level have been logged.

  Unlike some build systems, this does NOT convert such log entries to errors, and it does not abort jobs when warnings are logged (i.e., dependent jobs will still continue unimpeded).

• outLv : Lake.LogLevel

  The minimum log level for an log entry to be reported.

• out : Lake.OutStream

  The stream to which Lake reports build progress. By default, Lake uses stderr.

• ansiMode : Lake.AnsiMode

  Whether to use ANSI escape codes in build output.

def Lake.BuildConfig.showProgress (cfg : Lake.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)

inductive Lake.JobAction : Type

Information on what this job did.

• unknown : Lake.JobAction

  No information about this job's action is available.

• replay : Lake.JobAction

  Tried to replay a cached build action (set by buildFileUnlessUpToDate)

• fetch : Lake.JobAction

  Tried to fetch a build from a store (can be set by buildUnlessUpToDate?)

• build : Lake.JobAction

  Tried to perform a build action (set by buildUnlessUpToDate?)

instance Lake.instInhabitedJobAction : Inhabited Lake.JobAction

Equations

• Lake.instInhabitedJobAction = { default := Lake.JobAction.unknown }

instance Lake.instReprJobAction : Repr Lake.JobAction

Equations

• Lake.instReprJobAction = { reprPrec := Lake.reprJobAction✝ }

instance Lake.instDecidableEqJobAction : DecidableEq Lake.JobAction

Equations

• Lake.instDecidableEqJobAction x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance Lake.instOrdJobAction : Ord Lake.JobAction

Equations

• Lake.instOrdJobAction = { compare := Lake.ordJobAction✝ }

instance Lake.instLTJobAction : LT Lake.JobAction

Equations

• Lake.instLTJobAction = ltOfOrd

instance Lake.instLEJobAction : LE Lake.JobAction

Equations

• Lake.instLEJobAction = leOfOrd

instance Lake.instMinJobAction : Min Lake.JobAction

Equations

• Lake.instMinJobAction = minOfLe

instance Lake.instMaxJobAction : Max Lake.JobAction

Equations

• Lake.instMaxJobAction = maxOfLe

def Lake.JobAction.merge (a b : Lake.JobAction) : Lake.JobAction

Equations

• a.merge b = max a b

structure Lake.JobState : Type

Mutable state of a Lake job.

• log : Lake.Log

  The job's log.

• action : Lake.JobAction

  Tracks whether this job performed any significant build action.

• trace : Lake.BuildTrace

  Current trace of a build job.

instance Lake.instInhabitedJobState : Inhabited Lake.JobState

Equations

• Lake.instInhabitedJobState = { default := { log := default, action := default, trace := default } }

@[reducible, inline]

abbrev Lake.JobResult (α : Type u_1) : Type u_1

The result of a Lake job.

Equations

• Lake.JobResult α = Lake.EResult Lake.Log.Pos Lake.JobState α

@[reducible, inline]

abbrev Lake.JobTask (α : Type u_1) : Type u_1

The Task of a Lake job.

Equations

• Lake.JobTask α = Lake.BaseIOTask (Lake.JobResult α)

structure Lake.Job (α : Type u) : Type u

A Lake job.

• task : Lake.JobTask α

  The Lean Task object for the job.

• caption : String

  A caption for the job in Lake's build monitor. Will be formatted like ✔ [3/5] Ran <caption>.

• optional : Bool

  Whether this job failing should cause the build to fail.

instance Lake.instInhabitedJob {a✝ : Type u_1} : Inhabited (Lake.Job a✝)

Equations

• Lake.instInhabitedJob = { default := { task := default, caption := default, optional := default } }

@[reducible, inline]

abbrev Lake.OpaqueJob : Type

A Lake job with an opaque value in Type.

Equations

• Lake.OpaqueJob = Lake.Job Opaque

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

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

• oldMode : Bool
• trustHash : Bool
• noBuild : Bool
• verbosity : Lake.Verbosity
• failLv : Lake.LogLevel
• outLv : Lake.LogLevel
• out : Lake.OutStream
• ansiMode : Lake.AnsiMode
• opaqueWs : Lake.OpaqueWorkspace
• leanTrace : Lake.BuildTrace
• registeredJobs : IO.Ref (Array Lake.OpaqueJob)

@[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

@[inline]

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

Equations

• Lake.getBuildContext = readThe Lake.BuildContext

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

def Lake.getIsOldMode {m : Type → Type u_1} [Functor m] [Lake.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] [Lake.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] [Lake.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] [Lake.MonadBuild m] : m Lake.Verbosity

Equations

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

@[inline]

def Lake.getIsVerbose {m : Type → Type u_1} [Functor m] [Lake.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] [Lake.MonadBuild m] : m Bool

Equations

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

@[reducible, inline]

abbrev Lake.CoreBuildM (α : Type) : Type

The internal core monad of Lake builds. Not intended for user use.

Equations

• Lake.CoreBuildM = Lake.BuildT Lake.LogIO

@[inline, deprecated "See doc-string for deprecation information." (since := "2024-05-25")]

def Lake.logStep {m : Type → Type u_1} [Monad m] [Lake.MonadLog m] (message : String) : m Unit

Logs a build step with message.

Deprecated: Build steps are now managed by a top-level build monitor. As a result, this no longer functions the way it used to. It now just logs the message via logVerbose.

Equations

• Lake.logStep message = Lake.logVerbose message