def Lake.mkBuildContext (ws : Lake.Workspace) (config : Lake.BuildConfig) : IO Lake.BuildContext

Equations

• One or more equations did not get rendered due to their size.

def Lake.failOnBuildCycle {k : Type u_1} {α : Type} [ToString k] : Except (List k) α → Lake.BuildM α

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Lake.RecBuildM.runIn {α : Type} (store : Lake.BuildStore) (build : Lake.RecBuildM α) : Lake.BuildM (α × Lake.BuildStore)

Run the recursive build in the given build store. If a cycle is encountered, log it and then fail.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Lake.RecBuildM.run {α : Type} (build : Lake.RecBuildM α) : Lake.BuildM α

Run the recursive build in a fresh build store. If a cycle is encountered, log it and then fail.

Equations

• Lake.RecBuildM.run build = (fun x => x.fst) <$> Lake.RecBuildM.runIn ∅ build

@[inline]

def Lake.busyAcquireLockFile (lockFile : Lake.FilePath) : IO PUnit

Busy waits to acquire the lock represented by the lockFile. Prints a warning if on the first time it has to wait.

Equations

• Lake.busyAcquireLockFile lockFile = Lake.busyAcquireLockFile.busyLoop lockFile true

partial def Lake.busyAcquireLockFile.busyLoop (lockFile : Lake.FilePath) (firstTime : Bool) : IO PUnit

@[inline]

def Lake.withLockFile {m : Type → Type u_1} {α : Type} [Monad m] [MonadFinally m] [MonadLiftT IO m] (lockFile : Lake.FilePath) (act : m α) : m α

Busy wait to acquire the lock of lockFile, run act, and then release the lock.

Equations

• One or more equations did not get rendered due to their size.

def Lake.lockFileName : String

The name of the Lake build lock file name (i.e., lake.lock).

Equations

• Lake.lockFileName = "lake.lock"

@[inline]

def Lake.Workspace.lockFile (self : Lake.Workspace) : Lake.FilePath

The workspace's build lock file.

Equations

• Lake.Workspace.lockFile self = Lake.Package.buildDir self.root / { toString := Lake.lockFileName }

@[inline]

def Lake.Workspace.runBuild {α : Type} (ws : Lake.Workspace) (build : Lake.BuildM α) (config : optParam Lake.BuildConfig { oldMode := false, trustHash := true }) : Lake.LogIO α

Run the given build function in the Workspace's context.

Equations

• Lake.Workspace.runBuild ws build config = do let ctx ← liftM (Lake.mkBuildContext ws config) Lake.BuildM.run ctx build

@[inline]

def Lake.runBuild {α : Type} (build : Lake.BuildM α) (config : optParam Lake.BuildConfig { oldMode := false, trustHash := true }) : Lake.LakeT Lake.LogIO α

Run the given build function in the Lake monad's workspace.

Equations

• Lake.runBuild build config = do let __do_lift ← Lake.getWorkspace liftM (Lake.Workspace.runBuild __do_lift build config)