Lock File Utilities

This module defines utilities to use a file to ensure mutual exclusions between processes manipulating some shared resource. Such a file is termed a "lock file".

Lake does not currently use a lock file. Previously, Lake used one for builds, but this was removed in lean4#2445. Without an API for catching Ctrl-C during a build, the lock file was deemed too disruptive for users.

@[inline]

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

Equations

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

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

@[inline]

def Lake.withLockFile {m : Type → Type u_1} {α : Type} [Monad m] [MonadFinally m] [MonadLiftT IO m] (lockFile : System.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.