Documentation

Lake.Build.Monad

def Lake.failOnBuildCycle {k : Type u_1} {α : Type} [ToString k] :
Except (List k) αLake.BuildM α
Instances For
    @[inline]

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

    Instances For
      @[inline]

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

      Instances For
        @[inline]

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

        Instances For
          partial def Lake.busyAcquireLockFile.busyLoop (lockFile : Lake.FilePath) (firstTime : Bool) :
          @[inline]
          def Lake.withLockFile {m : TypeType 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.

          Instances For

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

            Instances For
              @[inline]

              The workspace's build lock file.

              Instances For
                @[inline]
                def Lake.Workspace.runBuild {α : Type} (ws : Lake.Workspace) (build : Lake.BuildM α) (config : optParam Lake.BuildConfig { oldMode := false, trustHash := true }) :

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

                Instances For
                  @[inline]
                  def Lake.runBuild {α : Type} (build : Lake.BuildM α) (config : optParam Lake.BuildConfig { oldMode := false, trustHash := true }) :

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

                  Instances For