HepLean Documentation

Lake.Util.Lock

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.

source
@[inline]
def Lake.busyAcquireLockFile (lockFile : Lake.FilePath) :
IO PUnit
Equations
Instances For
    source
    partial def Lake.busyAcquireLockFile.busyLoop (lockFile : Lake.FilePath) (firstTime : Bool) :
    IO PUnit
    source
    @[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.
    Instances For