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