Documentation

Lake.Build.Job.Monad

Job Monad #

This module contains additional definitions for Lake Job. In particular, it defines JobM, which uses BuildContext, which contains OpaqueJobs, hence the module split.

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

      Record that this job is trying to perform some action.

      Equations
        Instances For
          @[inline]

          Returns the current job's build trace.

          Equations
            Instances For
              @[inline]

              Sets the current job's build trace.

              Equations
                Instances For
                  @[inline]

                  Set the caption of the job's build trace.

                  Equations
                    Instances For
                      @[inline]
                      def Lake.newTrace (caption : String := "<nil>") :

                      Replace the job's build trace with a new empty trace.

                      Equations
                        Instances For
                          @[inline]

                          Mix a trace into the current job's build trace.

                          Equations
                            Instances For
                              @[inline]

                              Returns the current job's build trace and removes it from the state.

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

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

                                  Equations
                                    Instances For
                                      @[inline]
                                      def Lake.JobM.runSpawnM {α : Type} (x : SpawnM α) :
                                      JobM α
                                      Equations
                                        Instances For
                                          @[inline]
                                          def Lake.FetchM.runJobM {α : Type} (x : JobM α) :

                                          Run a JobM action in FetchM.

                                          Generally, this should not be done, and instead a job action should be run asynchronously in a Job (e.g., via Job.async).

                                          Equations
                                            Instances For
                                              @[inline]
                                              def Lake.JobM.runFetchM {α : Type} (x : FetchM α) :
                                              JobM α

                                              Run a FetchM action in JobM.

                                              Equations
                                                Instances For
                                                  @[inline]
                                                  def Lake.Job.bindTask {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] [OptDataKind β] (f : JobTask αm (JobTask β)) (self : Job α) :
                                                  m (Job β)
                                                  Equations
                                                    Instances For
                                                      @[inline]
                                                      def Lake.Job.async {α : Type} [OptDataKind α] (act : JobM α) (prio : Task.Priority := Task.Priority.default) (caption : String := "") :
                                                      SpawnM (Job α)

                                                      Spawn a job that asynchronously performs act.

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

                                                          Wait a the job to complete and return the result.

                                                          Equations
                                                            Instances For
                                                              @[inline]
                                                              def Lake.Job.wait? {α : Type} (self : 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 : 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
                                                                    Instances For
                                                                      def Lake.Job.mapM {β : Type} {α : Type u_1} [kind : OptDataKind β] (self : Job α) (f : αJobM β) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) :
                                                                      SpawnM (Job β)

                                                                      Apply f asynchronously to the job's output.

                                                                      Equations
                                                                        Instances For
                                                                          @[reducible, inline, deprecated Lake.Job.mapM (since := "2024-12-06")]
                                                                          abbrev Lake.Job.bindSync {β : Type} {α : Type u_1} [OptDataKind β] (self : Job α) (f : αJobM β) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) :
                                                                          SpawnM (Job β)
                                                                          Equations
                                                                            Instances For
                                                                              def Lake.Job.bindM {β : Type} {α : Type u_1} [kind : OptDataKind β] (self : Job α) (f : αJobM (Job β)) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) :
                                                                              SpawnM (Job β)

                                                                              Apply f asynchronously to the job's output and asynchronously await the resulting job.

                                                                              Equations
                                                                                Instances For
                                                                                  @[reducible, inline, deprecated Lake.Job.bindM (since := "2024-12-06")]
                                                                                  abbrev Lake.Job.bindAsync {β : Type} {α : Type u_1} [OptDataKind β] (self : Job α) (f : αSpawnM (Job β)) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) :
                                                                                  SpawnM (Job β)
                                                                                  Equations
                                                                                    Instances For
                                                                                      @[inline]
                                                                                      def Lake.Job.zipResultWith {γ : Type u_1} {α : Type u_2} {β : Type u_3} [OptDataKind γ] (f : JobResult αJobResult βJobResult γ) (self : Job α) (other : Job β) (prio : Task.Priority := Task.Priority.default) (sync : Bool := true) :
                                                                                      Job γ

                                                                                      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
                                                                                        Instances For
                                                                                          @[inline]
                                                                                          def Lake.Job.zipWith {γ : Type u_1} {α : Type u_2} {β : Type u_3} [OptDataKind γ] (f : αβγ) (self : Job α) (other : Job β) (prio : Task.Priority := Task.Priority.default) (sync : Bool := true) :
                                                                                          Job γ

                                                                                          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
                                                                                            Instances For
                                                                                              def Lake.Job.add {α : Type u_1} {β : Type u_2} (self : Job α) (other : Job β) :
                                                                                              Job α

                                                                                              Merges this job with another, discarding its output and trace.

                                                                                              Equations
                                                                                                Instances For
                                                                                                  def Lake.Job.mix {α : Type u_1} {β : Type u_2} (self : Job α) (other : Job β) :

                                                                                                  Merges this job with another, discarding both outputs.

                                                                                                  Equations
                                                                                                    Instances For
                                                                                                      def Lake.Job.mixList {α : Type u_1} (jobs : List (Job α)) (traceCaption : String := "<collection>") :

                                                                                                      Merge a List of jobs into one, discarding their outputs.

                                                                                                      Equations
                                                                                                        Instances For
                                                                                                          def Lake.Job.mixArray {α : Type u_1} (jobs : Array (Job α)) (traceCaption : String := "<collection>") :

                                                                                                          Merge an Array of jobs into one, discarding their outputs.

                                                                                                          Equations
                                                                                                            Instances For
                                                                                                              def Lake.Job.collectList {α : Type u_1} (jobs : List (Job α)) (traceCaption : String := "<collection>") :
                                                                                                              Job (List α)

                                                                                                              Merge a List of jobs into one, collecting their outputs into a List.

                                                                                                              Equations
                                                                                                                Instances For
                                                                                                                  def Lake.Job.collectArray {α : Type u_1} (jobs : Array (Job α)) (traceCaption : String := "<collection>") :
                                                                                                                  Job (Array α)

                                                                                                                  Merge an Array of jobs into one, collecting their outputs into an Array.

                                                                                                                  Equations
                                                                                                                    Instances For

                                                                                                                      BuildJob (deprecated) #

                                                                                                                      @[reducible, inline, deprecated Lake.Job (since := "2024-12-06")]
                                                                                                                      abbrev Lake.BuildJob (α : Type u_1) :
                                                                                                                      Type u_1

                                                                                                                      A Lake build job.

                                                                                                                      Equations
                                                                                                                        Instances For
                                                                                                                          @[inline, deprecated "Obsolete." (since := "2024-12-06")]
                                                                                                                          def Lake.BuildJob.mk {α : Type u_1} (job : Job (α × BuildTrace)) :
                                                                                                                          Equations
                                                                                                                            Instances For
                                                                                                                              @[inline, deprecated "Obsolete." (since := "2024-12-06")]
                                                                                                                              Equations
                                                                                                                                Instances For
                                                                                                                                  @[reducible, inline]
                                                                                                                                  abbrev Lake.BuildJob.toJob {α : Type u_1} (self : BuildJob α) :
                                                                                                                                  Job α
                                                                                                                                  Equations
                                                                                                                                    Instances For
                                                                                                                                      @[reducible, inline, deprecated Lake.Job.nil (since := "2024-12-06")]
                                                                                                                                      Equations
                                                                                                                                        Instances For
                                                                                                                                          @[reducible, inline, deprecated Lake.Job.map (since := "2024-12-06")]
                                                                                                                                          abbrev Lake.BuildJob.pure {α : Type u_1} [OptDataKind α] (a : α) :
                                                                                                                                          Equations
                                                                                                                                            Instances For
                                                                                                                                              @[reducible, inline, deprecated Lake.Job.map (since := "2024-12-06")]
                                                                                                                                              abbrev Lake.BuildJob.map {β : Type u_1} {α : Type u_2} [OptDataKind β] (f : αβ) (self : BuildJob α) :
                                                                                                                                              Equations
                                                                                                                                                Instances For
                                                                                                                                                  @[inline, deprecated "Removed without replacement." (since := "2024-12-06")]
                                                                                                                                                  def Lake.BuildJob.mapWithTrace {β : Type u_1} {α : Type u_2} [OptDataKind β] (f : αBuildTraceβ × BuildTrace) (self : BuildJob α) :
                                                                                                                                                  Equations
                                                                                                                                                    Instances For
                                                                                                                                                      @[inline, deprecated Lake.Job.mapM (since := "2024-12-06")]
                                                                                                                                                      def Lake.BuildJob.bindSync {β : Type} {α : Type u_1} [OptDataKind β] (self : BuildJob α) (f : αBuildTraceJobM (β × BuildTrace)) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) :
                                                                                                                                                      SpawnM (Job β)
                                                                                                                                                      Equations
                                                                                                                                                        Instances For
                                                                                                                                                          @[inline, deprecated Lake.Job.bindM (since := "2024-12-06")]
                                                                                                                                                          def Lake.BuildJob.bindAsync {β : Type} {α : Type u_1} [OptDataKind β] (self : BuildJob α) (f : αBuildTraceSpawnM (Job β)) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) :
                                                                                                                                                          SpawnM (Job β)
                                                                                                                                                          Equations
                                                                                                                                                            Instances For
                                                                                                                                                              @[reducible, inline, deprecated Lake.Job.wait? (since := "2024-12-06")]
                                                                                                                                                              abbrev Lake.BuildJob.wait? {α : Type} (self : BuildJob α) :
                                                                                                                                                              Equations
                                                                                                                                                                Instances For
                                                                                                                                                                  @[reducible, inline, deprecated Lake.Job.add (since := "2024-12-06")]
                                                                                                                                                                  abbrev Lake.BuildJob.add {α : Type u_1} {β : Type u_2} (self : BuildJob α) (other : BuildJob β) :
                                                                                                                                                                  Equations
                                                                                                                                                                    Instances For
                                                                                                                                                                      @[reducible, inline, deprecated Lake.Job.mix (since := "2024-12-06")]
                                                                                                                                                                      abbrev Lake.BuildJob.mix {α : Type u_1} {β : Type u_2} (self : BuildJob α) (other : BuildJob β) :
                                                                                                                                                                      Equations
                                                                                                                                                                        Instances For
                                                                                                                                                                          @[reducible, inline, deprecated Lake.Job.mixList (since := "2024-12-06")]
                                                                                                                                                                          abbrev Lake.BuildJob.mixList {α : Type u_1} (jobs : List (BuildJob α)) :
                                                                                                                                                                          Equations
                                                                                                                                                                            Instances For
                                                                                                                                                                              @[reducible, inline, deprecated Lake.Job.mixArray (since := "2024-12-06")]
                                                                                                                                                                              abbrev Lake.BuildJob.mixArray {α : Type u_1} (jobs : Array (BuildJob α)) :
                                                                                                                                                                              Equations
                                                                                                                                                                                Instances For
                                                                                                                                                                                  @[reducible, inline, deprecated Lake.Job.zipWith (since := "2024-12-06")]
                                                                                                                                                                                  abbrev Lake.BuildJob.zipWith {γ : Type u_1} {α : Type u_2} {β : Type u_3} [OptDataKind γ] (f : αβγ) (self : BuildJob α) (other : BuildJob β) :
                                                                                                                                                                                  Equations
                                                                                                                                                                                    Instances For
                                                                                                                                                                                      @[reducible, inline, deprecated Lake.Job.collectList (since := "2024-12-06")]
                                                                                                                                                                                      abbrev Lake.BuildJob.collectList {α : Type u_1} (jobs : List (BuildJob α)) :
                                                                                                                                                                                      Equations
                                                                                                                                                                                        Instances For
                                                                                                                                                                                          @[reducible, inline, deprecated Lake.Job.collectArray (since := "2024-12-06")]
                                                                                                                                                                                          abbrev Lake.BuildJob.collectArray {α : Type u_1} (jobs : Array (BuildJob α)) :
                                                                                                                                                                                          Equations
                                                                                                                                                                                            Instances For