Documentation

Lake.Build.Trace

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 (i : Type u) (m : outParam (Type v → Type w)) (t : Type v) :
    Type (max u w)
    • computeTrace : im t

      Compute the trace of some target info using information from the monadic context.

    Instances
      @[inline]
      def Lake.computeTrace {i : Type u_1} {m : Type u_2 → Type u_3} {t : Type u_2} {n : Type u_2 → Type u_4} [Lake.ComputeTrace i m t] [MonadLiftT m n] (info : i) :
      n t
      Equations
      Instances For
        class Lake.NilTrace (t : Type u) :
        • nilTrace : t

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

        Instances
          Equations
          • Lake.inhabitedOfNilTrace = { default := Lake.nilTrace }
          class Lake.MixTrace (t : Type u) :
          • mixTrace : ttt

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

          Instances
            def Lake.mixTraceList {t : Type u_1} [Lake.MixTrace t] [Lake.NilTrace t] (traces : List t) :
            t
            Equations
            Instances For
              def Lake.mixTraceArray {t : Type u_1} [Lake.MixTrace t] [Lake.NilTrace t] (traces : Array t) :
              t
              Equations
              Instances For
                @[specialize #[]]
                def Lake.computeListTrace {t : Type u_1} {i : Type u_2} {m : Type u_1 → Type u_3} [Lake.MixTrace t] [Lake.NilTrace t] [Lake.ComputeTrace i m t] {n : Type u_1 → Type u_4} [MonadLiftT m n] [Monad n] (artifacts : List i) :
                n t
                Equations
                Instances For
                  instance Lake.instComputeTraceListOfMonad {t : Type u_1} {i : Type u_2} {m : Type u_1 → Type u_3} [Lake.MixTrace t] [Lake.NilTrace t] [Lake.ComputeTrace i m t] [Monad m] :
                  Equations
                  • Lake.instComputeTraceListOfMonad = { computeTrace := Lake.computeListTrace }
                  @[specialize #[]]
                  def Lake.computeArrayTrace {t : Type u_1} {i : Type u_2} {m : Type u_1 → Type u_3} [Lake.MixTrace t] [Lake.NilTrace t] [Lake.ComputeTrace i m t] {n : Type u_1 → Type u_4} [MonadLiftT m n] [Monad n] (artifacts : Array i) :
                  n t
                  Equations
                  Instances For
                    instance Lake.instComputeTraceArrayOfMonad {t : Type u_1} {i : Type u_2} {m : Type u_1 → Type u_3} [Lake.MixTrace t] [Lake.NilTrace t] [Lake.ComputeTrace i m t] [Monad m] :
                    Equations
                    • Lake.instComputeTraceArrayOfMonad = { computeTrace := Lake.computeArrayTrace }

                    Hash Trace #

                    structure Lake.Hash :

                    A content hash. TODO: Use a secure hash rather than the builtin Lean hash function.

                    Instances For
                      @[inline]
                      Equations
                      Instances For
                        Equations
                        Instances For
                          @[inline]
                          Equations
                          • h1.mix h2 = { val := mixHash h1.val h2.val }
                          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)
                                      Instances
                                        Equations
                                        • Lake.instComputeTraceHashOfComputeHash = { computeTrace := Lake.ComputeHash.computeHash }
                                        @[inline]
                                        def Lake.pureHash {α : Type u_1} [Lake.ComputeHash α Id] (a : α) :
                                        Equations
                                        Instances For
                                          @[inline]
                                          def Lake.computeHash {α : Type u_1} {m : TypeType u_2} {n : TypeType u_3} [Lake.ComputeHash α m] [MonadLiftT m n] (a : α) :
                                          Equations
                                          Instances For
                                            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
                                                @[specialize #[]]
                                                def Lake.computeArrayHash {α : Type u_1} {m : TypeType u_2} [Lake.ComputeHash α m] [Monad m] (xs : Array α) :
                                                Equations
                                                Instances For
                                                  instance Lake.instComputeHashArrayOfMonad {α : Type u_1} {m : TypeType u_2} [Lake.ComputeHash α m] [Monad m] :
                                                  Equations
                                                  • Lake.instComputeHashArrayOfMonad = { computeHash := Lake.computeArrayHash }

                                                  Modification Time (MTime) Trace #

                                                  A modification time.

                                                  Equations
                                                  Instances For
                                                    Equations
                                                    class Lake.GetMTime (α : Sort u_1) :
                                                    Sort (max 1 u_1)
                                                    Instances
                                                      Equations
                                                      • Lake.instComputeTraceIOMTimeOfGetMTime = { computeTrace := Lake.getMTime }
                                                      @[inline]
                                                      Equations
                                                      Instances For
                                                        @[specialize #[]]
                                                        def Lake.MTime.checkUpToDate {i : Sort u_1} [Lake.GetMTime i] (info : i) (self : Lake.MTime) :

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

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

                                                          Lake Build Trace (Hash + MTIme) #

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

                                                          Instances For
                                                            @[inline]
                                                            Equations
                                                            Instances For
                                                              @[inline]
                                                              Equations
                                                              Instances For
                                                                Equations
                                                                Instances For
                                                                  @[specialize #[]]
                                                                  def Lake.BuildTrace.compute {i : Type u_1} {m : TypeType u_2} [Lake.ComputeHash i m] [MonadLiftT m IO] [Lake.GetMTime i] (info : i) :
                                                                  Equations
                                                                  Instances For
                                                                    Equations
                                                                    • Lake.BuildTrace.instComputeTraceIOOfComputeHashOfMonadLiftTOfGetMTime = { computeTrace := Lake.BuildTrace.compute }
                                                                    Equations
                                                                    • t1.mix t2 = { hash := t1.hash.mix t2.hash, mtime := max t1.mtime t2.mtime }
                                                                    Instances For
                                                                      @[specialize #[]]

                                                                      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]

                                                                        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
                                                                          @[specialize #[], deprecated]

                                                                          Check if the info is up-to-date using a trace file. If the file exists, match its hash to this trace's hash. If not, check if the info is newer than this trace's modification time.

                                                                          Deprecated: Should not be done manually, but as part of buildUnlessUpToDate.

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

                                                                            Write trace to a file.

                                                                            Deprecated: Should not be done manually, but as part of buildUnlessUpToDate.

                                                                            Equations
                                                                            Instances For