structure Lake.BuildConfig : Type

• oldMode : Bool
• trustHash : Bool

Configuration options for a Lake build.

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

• oldMode : Bool
• trustHash : Bool
• opaqueWs : Lake.OpaqueWorkspace
• leanTrace : Lake.BuildTrace
• startedBuilds : IO.Ref Nat
• finishedBuilds : IO.Ref Nat

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

@[inline, reducible]

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

A transformer to equip a monad with a BuildContext.

@[inline]

def Lake.getLeanTrace {m : Type → Type u_1} [Monad m] : Lake.BuildT m Lake.BuildTrace

@[inline]

def Lake.getBuildConfig {m : Type → Type u_1} [Monad m] : Lake.BuildT m Lake.BuildConfig

@[inline]

def Lake.getIsOldMode {m : Type → Type u_1} [Monad m] : Lake.BuildT m Bool

@[inline]

def Lake.getTrustHash {m : Type → Type u_1} [Monad m] : Lake.BuildT m Bool

@[inline, reducible]

abbrev Lake.SchedulerM (α : Type) : Type

The monad for the Lake build manager.

@[inline, reducible]

abbrev Lake.BuildM (α : Type) : Type

The core monad for Lake builds.

@[inline, reducible]

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

A transformer to equip a monad with a Lake build store.

@[inline, reducible]

abbrev Lake.BuildCycle : Type

A Lake build cycle.

@[inline, reducible]

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

A transformer for monads that may encounter a build cycle.

@[inline, reducible]

abbrev Lake.RecBuildM (α : Type) : Type

A recursive build of a Lake build store that may encounter a cycle.

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

@[inline]

def Lake.BuildM.run {α : Type} (ctx : Lake.BuildContext) (self : Lake.BuildM α) : Lake.LogIO α

def Lake.BuildM.catchFailure {α : Type} (f : Unit → BaseIO α) (self : Lake.BuildM α) : Lake.SchedulerM α

def Lake.logStep (message : String) : Lake.BuildM Unit

def Lake.createParentDirs (path : Lake.FilePath) : IO Unit