Documentation

Lake.Build.Monad

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    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.
    Instances For
      @[inline]

      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.
      Instances For
        @[inline]

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

        Equations
        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.

          Equations
          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.

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

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

              Equations
              Instances For
                @[inline]

                The workspace's build lock file.

                Equations
                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.

                  Equations
                  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.

                    Equations
                    Instances For