Documentation

Lake.Build.Job

inductive Lake.JobAction :

Information on what this job did.

  • unknown: Lake.JobAction

    No information about this job's action is available.

  • replay: Lake.JobAction

    Tried to replay a cached build action (set by buildFileUnlessUpToDate)

  • fetch: Lake.JobAction

    Tried to fetch a build from a store (can be set by buildUnlessUpToDate?)

  • build: Lake.JobAction

    Tried to perform a build action (set by buildUnlessUpToDate?)

Instances For
    Equations
    @[inline]
    Equations
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        structure Lake.JobState :

        Mutable state of a Lake job.

        • log : Lake.Log

          The job's log.

        • Tracks whether this job performed any significant build action.

        Instances For
          Equations
          @[inline]

          Resets the job state after a checkpoint (e.g., registering the job). Preserves state that downstream jobs want to depend on while resetting job-local state that should not be inherited by downstream jobs.

          Equations
          Instances For
            Equations
            • a.merge b = { log := a.log ++ b.log, action := a.action.merge b.action }
            Instances For
              @[inline]
              Equations
              Instances For
                @[reducible, inline]
                abbrev Lake.JobResult (α : Type u_1) :
                Type u_1

                The result of a Lake job.

                Equations
                Instances For
                  @[reducible, inline]
                  abbrev Lake.JobTask (α : Type u_1) :
                  Type u_1

                  The Task of a Lake job.

                  Equations
                  Instances For
                    @[reducible, inline]
                    abbrev Lake.JobM (α : Type) :

                    The monad of asynchronous Lake jobs.

                    While this can be lifted into FetchM, job action should generally be wrapped into an asynchronous job (e.g., via Job.async) instead of being run directly in FetchM.

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

                      Record that this job is trying to perform some action.

                      Equations
                      Instances For
                        @[reducible, inline]
                        abbrev Lake.SpawnM (α : Type) :

                        The monad used to spawn asynchronous Lake build jobs. Lifts into FetchM.

                        Equations
                        Instances For
                          @[reducible, inline, deprecated Lake.SpawnM]
                          abbrev Lake.SchedulerM (α : Type) :

                          The monad used to spawn asynchronous Lake build jobs. Replaced by SpawnM.

                          Equations
                          Instances For
                            structure Lake.Job (α : Type u) :

                            A Lake job.

                            Instances For
                              instance Lake.instInhabitedJob :
                              {a : Type u_1} → Inhabited (Lake.Job a)
                              Equations
                              • Lake.instInhabitedJob = { default := { task := default, caption := default } }
                              structure Lake.BundledJob :
                              Type (u + 1)
                              Instances For
                                Equations
                                • Lake.instCoeOutJobBundledJob = { coe := Lake.BundledJob.mk }
                                Equations
                                @[implemented_by Lake.OpaqueJob.unsafeGet]
                                @[implemented_by Lake.OpaqueJob.unsafeMk]
                                @[reducible, inline]
                                Equations
                                • job.type = job.get.type
                                Instances For
                                  @[reducible, inline]
                                  Equations
                                  • job.toJob = job.get.job
                                  Instances For
                                    @[reducible, inline]
                                    Equations
                                    • job.task = job.toJob.task
                                    Instances For
                                      @[reducible, inline]
                                      Equations
                                      • job.caption = job.toJob.caption
                                      Instances For
                                        Equations
                                        • Lake.instCoeDepOpaqueJobJobType = { coe := job.toJob }
                                        @[inline]
                                        def Lake.Job.ofTask {α : Type u_1} (task : Lake.JobTask α) (caption : optParam String "") :
                                        Equations
                                        Instances For
                                          @[inline]
                                          def Lake.Job.error {α : Type u_1} (log : optParam Lake.Log ) (caption : optParam String "") :
                                          Equations
                                          Instances For
                                            @[inline]
                                            def Lake.Job.pure {α : Type u_1} (a : α) (log : optParam Lake.Log ) (caption : optParam String "") :
                                            Equations
                                            Instances For
                                              Equations
                                              instance Lake.Job.instInhabited {α : Type u_1} [Inhabited α] :
                                              Equations
                                              • Lake.Job.instInhabited = { default := pure default }
                                              @[inline]
                                              Equations
                                              Instances For
                                                @[inline]
                                                def Lake.Job.setCaption {α : Type u_1} (caption : String) (job : Lake.Job α) :

                                                Sets the job's caption.

                                                Equations
                                                Instances For
                                                  @[inline]
                                                  def Lake.Job.setCaption? {α : Type u_1} (caption : String) (job : Lake.Job α) :

                                                  Sets the job's caption if the job's current caption is empty.

                                                  Equations
                                                  Instances For
                                                    @[inline]
                                                    def Lake.Job.mapResult {α : Type u_1} {β : Type u_2} (f : Lake.JobResult αLake.JobResult β) (self : Lake.Job α) (prio : optParam Task.Priority Task.Priority.default) (sync : optParam Bool false) :
                                                    Equations
                                                    Instances For
                                                      @[inline]
                                                      def Lake.Job.bindTask {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : Lake.JobTask αm (Lake.JobTask β)) (self : Lake.Job α) :
                                                      m (Lake.Job β)
                                                      Equations
                                                      • Lake.Job.bindTask f self = do let __do_liftf self.task pure { task := __do_lift, caption := self.caption }
                                                      Instances For
                                                        @[inline]
                                                        def Lake.Job.map {α : Type u_1} {β : Type u_2} (f : αβ) (self : Lake.Job α) (prio : optParam Task.Priority Task.Priority.default) (sync : optParam Bool false) :
                                                        Equations
                                                        Instances For
                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          def Lake.Job.renew {α : Type u_1} (self : Lake.Job α) :

                                                          Resets the job's state after a checkpoint (e.g., registering the job). Preserves information that downstream jobs want to depend on while resetting job-local information that should not be inherited by downstream jobs.

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

                                                            Spawn a job that asynchronously performs act.

                                                            Equations
                                                            Instances For
                                                              @[inline]
                                                              def Lake.Job.wait {α : Type} (self : Lake.Job α) :

                                                              Wait a the job to complete and return the result.

                                                              Equations
                                                              Instances For
                                                                @[inline]
                                                                def Lake.Job.wait? {α : Type} (self : Lake.Job α) :

                                                                Wait for a job to complete and return the produced value. If an error occurred, return none and discarded any logs produced.

                                                                Equations
                                                                Instances For
                                                                  @[inline]
                                                                  def Lake.Job.await {α : Type} (self : Lake.Job α) :

                                                                  Wait for a job to complete and return the produced value. Logs the job's log and throws if there was an error.

                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    @[inline]
                                                                    def Lake.Job.bindSync {α : Type u_1} {β : Type} (self : Lake.Job α) (f : αLake.JobM β) (prio : optParam Task.Priority Task.Priority.default) (sync : optParam Bool false) :

                                                                    let c ← a.bindSync b asynchronously performs the action b after the job a completes.

                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      @[inline]
                                                                      def Lake.Job.bindAsync {α : Type u_1} {β : Type} (self : Lake.Job α) (f : αLake.SpawnM (Lake.Job β)) (prio : optParam Task.Priority Task.Priority.default) (sync : optParam Bool false) :

                                                                      let c ← a.bindAsync b asynchronously performs the action b after the job a completes and then merges into the job produced by b.

                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For
                                                                        @[inline]
                                                                        def Lake.Job.zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (x : Lake.Job α) (y : Lake.Job β) (prio : optParam Task.Priority Task.Priority.default) (sync : optParam Bool false) :

                                                                        a.zipWith f b produces a new job c that applies f to the results of a and b. The job c errors if either a or b error.

                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For
                                                                          @[reducible, inline]
                                                                          abbrev Lake.BuildJob (α : Type u_1) :
                                                                          Type u_1

                                                                          A Lake build job.

                                                                          Equations
                                                                          Instances For
                                                                            @[inline]
                                                                            Equations
                                                                            Instances For
                                                                              @[inline]
                                                                              Equations
                                                                              Instances For
                                                                                @[inline]
                                                                                Equations
                                                                                • self.toJob = self
                                                                                Instances For
                                                                                  @[inline]
                                                                                  Equations
                                                                                  Instances For
                                                                                    @[inline]
                                                                                    def Lake.BuildJob.pure {α : Type u_1} (a : α) :
                                                                                    Equations
                                                                                    Instances For
                                                                                      Equations
                                                                                      @[inline]
                                                                                      def Lake.BuildJob.map {α : Type u_1} {β : Type u_1} (f : αβ) (self : Lake.BuildJob α) :
                                                                                      Equations
                                                                                      Instances For
                                                                                        Equations
                                                                                        @[inline]
                                                                                        def Lake.BuildJob.mapWithTrace {α : Type u_1} {β : Type u_1} (f : αLake.BuildTraceβ × Lake.BuildTrace) (self : Lake.BuildJob α) :
                                                                                        Equations
                                                                                        Instances For
                                                                                          @[inline]
                                                                                          Equations
                                                                                          • self.bindSync f prio sync = self.toJob.bindSync (fun (x : α × Lake.BuildTrace) => match x with | (a, t) => f a t) prio sync
                                                                                          Instances For
                                                                                            @[inline]
                                                                                            Equations
                                                                                            • self.bindAsync f prio sync = self.toJob.bindAsync (fun (x : α × Lake.BuildTrace) => match x with | (a, t) => f a t) prio sync
                                                                                            Instances For
                                                                                              @[inline]
                                                                                              def Lake.BuildJob.wait? {α : Type} (self : Lake.BuildJob α) :
                                                                                              Equations
                                                                                              Instances For
                                                                                                def Lake.BuildJob.add {α : Type u_1} {β : Type u_2} (t1 : Lake.BuildJob α) (t2 : Lake.BuildJob β) :
                                                                                                Equations
                                                                                                Instances For
                                                                                                  def Lake.BuildJob.mix {α : Type u_1} {β : Type u_2} (t1 : Lake.BuildJob α) (t2 : Lake.BuildJob β) :
                                                                                                  Equations
                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                  Instances For
                                                                                                    Equations
                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                    Instances For
                                                                                                      Equations
                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                      Instances For
                                                                                                        def Lake.BuildJob.zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (t1 : Lake.BuildJob α) (t2 : Lake.BuildJob β) :
                                                                                                        Equations
                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                        Instances For
                                                                                                          Equations
                                                                                                          Instances For
                                                                                                            Equations
                                                                                                            Instances For