Documentation

Lake.Build.Monad

source
def Lake.mkBuildContext (ws : Lake.Workspace) (oldMode : Bool) :
IO Lake.BuildContext
Instances For
    source
    @[inline]
    def Lake.getLeanTrace :
    Lake.BuildM Lake.BuildTrace
    Instances For
      source
      @[inline]
      def Lake.getIsOldMode :
      Lake.BuildM Bool
      Instances For
        source
        def Lake.failOnBuildCycle {k : Type u_1} {α : Type} [ToString k] :
        Except (List k) α → Lake.BuildM α
        Instances For
          source
          @[inline]
          def Lake.RecBuildM.runIn {α : Type} (store : Lake.BuildStore) (build : Lake.RecBuildM α) :
          Lake.BuildM (α × Lake.BuildStore)

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

          Instances For
            source
            @[inline]
            def Lake.RecBuildM.run {α : Type} (build : Lake.RecBuildM α) :
            Lake.BuildM α

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

            Instances For
              source
              @[inline]
              def Lake.busyAcquireLockFile (lockFile : Lake.FilePath) :
              IO PUnit

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

              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.

                Instances For
                  source
                  @[noinline]
                  def Lake.lockFileName :
                  String

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

                  Instances For
                    source
                    @[inline]
                    def Lake.Workspace.lockFile (self : Lake.Workspace) :
                    Lake.FilePath

                    The workspace's build lock file.

                    Instances For
                      source
                      @[inline]
                      def Lake.Workspace.runBuild {α : Type} (ws : Lake.Workspace) (build : Lake.BuildM α) (oldMode : optParam Bool false) :
                      Lake.LogIO α

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

                      Instances For
                        source
                        @[inline]
                        def Lake.runBuild {α : Type} (build : Lake.BuildM α) (oldMode : optParam Bool false) :
                        Lake.LakeT Lake.LogIO α

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

                        Instances For