Documentation

Lake.Build.Trace

Lake Traces #

This module defines Lake traces and associated utilities. Traces are used to determine whether a Lake build artifact is dirty (needs to be rebuilt) or is already up-to-date. The primary type is Lake.BuildTrace.

Utilities #

class Lake.CheckExists (i : Type u) :
  • checkExists : iBaseIO Bool

    Check whether there already exists an artifact for the given target info.

Instances

    Trace Abstraction #

    class Lake.ComputeTrace (α : Type u) (m : outParam (Type v → Type w)) (τ : Type v) :
    Type (max u w)
    • computeTrace : αm τ

      Compute the trace of an object in its preferred monad.

    Instances
      @[inline]
      def Lake.computeTrace {α : Type u_1} {m : Type u_2 → Type u_3} {τ : Type u_2} {n : Type u_2 → Type u_4} [ComputeTrace α m τ] [MonadLiftT m n] (a : α) :
      n τ

      Compute the trace of an object in a supporting monad.

      Equations
        Instances For
          class Lake.NilTrace (α : Type u) :
          • nilTrace : α

            The nil trace. Should not unduly clash with a proper trace.

          Instances
            instance Lake.inhabitedOfNilTrace {α : Type u_1} [NilTrace α] :
            Equations
              class Lake.MixTrace (α : Type u) :
              • mixTrace : ααα

                Combine two traces. The result should be dirty if either of the inputs is dirty.

              Instances
                def Lake.mixTraceList {τ : Type u_1} [MixTrace τ] [NilTrace τ] (traces : List τ) :
                τ
                Equations
                  Instances For
                    def Lake.mixTraceArray {τ : Type u_1} [MixTrace τ] [NilTrace τ] (traces : Array τ) :
                    τ
                    Equations
                      Instances For
                        @[inline]
                        def Lake.computeListTrace {τ : Type u_1} {α : Type u_2} {m : Type u_1 → Type u_3} [MixTrace τ] [NilTrace τ] [ComputeTrace α m τ] {n : Type u_1 → Type u_4} [MonadLiftT m n] [Monad n] (as : List α) :
                        n τ
                        Equations
                          Instances For
                            instance Lake.instComputeTraceListOfMonad {τ : Type u_1} {α : Type u_2} {m : Type u_1 → Type u_3} [MixTrace τ] [NilTrace τ] [ComputeTrace α m τ] [Monad m] :
                            ComputeTrace (List α) m τ
                            Equations
                              @[inline]
                              def Lake.computeArrayTrace {τ : Type u_1} {α : Type u_2} {m : Type u_1 → Type u_3} [MixTrace τ] [NilTrace τ] [ComputeTrace α m τ] {n : Type u_1 → Type u_4} [MonadLiftT m n] [Monad n] (as : Array α) :
                              n τ
                              Equations
                                Instances For
                                  instance Lake.instComputeTraceArrayOfMonad {τ : Type u_1} {α : Type u_2} {m : Type u_1 → Type u_3} [MixTrace τ] [NilTrace τ] [ComputeTrace α m τ] [Monad m] :
                                  Equations

                                    Hash Trace #

                                    structure Lake.Hash :

                                    A content hash.

                                    Instances For
                                      Equations
                                        Equations
                                          @[inline]
                                          Equations
                                            Instances For
                                              Equations
                                                Instances For
                                                  Equations
                                                    Instances For
                                                      Equations
                                                        Instances For
                                                          @[inline]
                                                          def Lake.Hash.mix (h1 h2 : Hash) :
                                                          Equations
                                                            Instances For
                                                              @[inline]
                                                              Equations
                                                                Instances For
                                                                  @[inline]
                                                                  Equations
                                                                    Instances For
                                                                      @[inline]
                                                                      Equations
                                                                        Instances For
                                                                          @[inline]
                                                                          Equations
                                                                            Instances For
                                                                              @[inline]
                                                                              Equations
                                                                                Instances For
                                                                                  @[inline]
                                                                                  Equations
                                                                                    Instances For
                                                                                      class Lake.ComputeHash (α : Type u) (m : outParam (TypeType v)) :
                                                                                      Type (max u v)
                                                                                      • computeHash : αm Hash

                                                                                        Compute the hash of an object in its preferred monad.

                                                                                      Instances
                                                                                        instance Lake.instComputeTraceHashOfComputeHash {α : Type u_1} {m : TypeType u_2} [ComputeHash α m] :
                                                                                        Equations
                                                                                          @[inline]
                                                                                          def Lake.pureHash {α : Type u_1} [ComputeHash α Id] (a : α) :

                                                                                          Compute the hash of object a in a pure context.

                                                                                          Equations
                                                                                            Instances For
                                                                                              @[inline]
                                                                                              def Lake.computeHash {α : Type u_1} {m : TypeType u_2} {n : TypeType u_3} [ComputeHash α m] [MonadLiftT m n] (a : α) :

                                                                                              Compute the hash an object in an supporting monad.

                                                                                              Equations
                                                                                                Instances For

                                                                                                  Compute the hash of a binary file. Binary files are equivalent only if they are byte identical.

                                                                                                  Equations
                                                                                                    Instances For

                                                                                                      Compute the hash of a text file. Normalizes \r\n sequences to \n for cross-platform compatibility.

                                                                                                      Equations
                                                                                                        Instances For

                                                                                                          A wrapper around FilePath that adjusts its ComputeHash implementation to normalize \r\n sequences to \n for cross-platform compatibility.

                                                                                                          Instances For
                                                                                                            @[inline]

                                                                                                            Compute the hash of a file. If text := true, normalize line endings.

                                                                                                            Equations
                                                                                                              Instances For
                                                                                                                @[inline]
                                                                                                                def Lake.computeArrayHash {α : Type u_1} {m : TypeType u_2} [ComputeHash α m] [Monad m] (as : Array α) :

                                                                                                                Compute the hash of each element of an array and combine them (left-to-right).

                                                                                                                Equations
                                                                                                                  Instances For
                                                                                                                    instance Lake.instComputeHashArrayOfMonad {α : Type u_1} {m : TypeType u_2} [ComputeHash α m] [Monad m] :
                                                                                                                    Equations

                                                                                                                      Modification Time (MTime) Trace #

                                                                                                                      A modification time (e.g., of a file).

                                                                                                                      Equations
                                                                                                                        Instances For
                                                                                                                          Equations
                                                                                                                            Equations
                                                                                                                              class Lake.GetMTime (α : Type u) :
                                                                                                                              • getMTime : αIO MTime

                                                                                                                                Return the modification time of an object.

                                                                                                                              Instances
                                                                                                                                @[inline]

                                                                                                                                Return the modification time of a file recorded by the OS.

                                                                                                                                Equations
                                                                                                                                  Instances For
                                                                                                                                    @[specialize #[]]
                                                                                                                                    def Lake.MTime.checkUpToDate {i : Type u_1} [GetMTime i] (info : i) (self : MTime) :

                                                                                                                                    Check if info is up-to-date using modification time. That is, check if the info is newer than self.

                                                                                                                                    Equations
                                                                                                                                      Instances For

                                                                                                                                        Lake Build Trace #

                                                                                                                                        Trace used for common Lake targets. Combines Hash and MTime.

                                                                                                                                        Instances For
                                                                                                                                          @[inline]

                                                                                                                                          Sets the caption of the trace.

                                                                                                                                          Equations
                                                                                                                                            Instances For
                                                                                                                                              @[inline]

                                                                                                                                              Clear the inputs of the build trace. This is used to remove unnecessary repetition of trace trees across multiple trace files.

                                                                                                                                              Equations
                                                                                                                                                Instances For
                                                                                                                                                  @[inline]
                                                                                                                                                  def Lake.BuildTrace.ofHash (hash : Hash) (caption : String := "<hash>") :
                                                                                                                                                  Equations
                                                                                                                                                    Instances For
                                                                                                                                                      @[inline]
                                                                                                                                                      def Lake.BuildTrace.ofMTime (mtime : MTime) (caption : String := "<mtime>") :
                                                                                                                                                      Equations
                                                                                                                                                        Instances For
                                                                                                                                                          def Lake.BuildTrace.nil (caption : String := "<nil>") :
                                                                                                                                                          Equations
                                                                                                                                                            Instances For
                                                                                                                                                              @[specialize #[]]
                                                                                                                                                              def Lake.BuildTrace.compute {α : Type u_1} {m : TypeType u_2} [ToString α] [ComputeHash α m] [MonadLiftT m IO] [GetMTime α] (info : α) :
                                                                                                                                                              Equations
                                                                                                                                                                Instances For
                                                                                                                                                                  Equations
                                                                                                                                                                    Instances For
                                                                                                                                                                      @[specialize #[]]
                                                                                                                                                                      def Lake.BuildTrace.checkAgainstHash {i : Type u_1} [CheckExists i] (info : i) (hash : Hash) (self : BuildTrace) :

                                                                                                                                                                      Check if the info is up-to-date using a hash. That is, check that info exists and its input hash matches this trace's hash.

                                                                                                                                                                      Equations
                                                                                                                                                                        Instances For
                                                                                                                                                                          @[inline]
                                                                                                                                                                          def Lake.BuildTrace.checkAgainstTime {i : Type u_1} [GetMTime i] (info : i) (self : BuildTrace) :

                                                                                                                                                                          Check if the info is up-to-date using modification time. That is, check if the info is newer than this input trace's modification time.

                                                                                                                                                                          Equations
                                                                                                                                                                            Instances For