Documentation

Lake.Build.Fetch

Recursive Building #

This module defines Lake's top-level build monad, FetchM, used for performing recursive builds. A recursive build is a build function which can fetch the results of other (recursive) builds. This is done using the fetch function defined in this module.

@[reducible, inline]
abbrev Lake.RecBuildM (α : Type) :

A recursive build of a Lake build store that may encounter a cycle.

Equations
Instances For
    Equations
    @[inline]

    Run a JobM action in RecBuildM (and thus 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
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      @[inline]

      Run a recursive build.

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

        Run a recursive build in a fresh build store.

        Equations
        Instances For
          @[specialize #[]]
          def Lake.buildCycleError {m : Type u_1 → Type u_2} {α : Type u_1} [Lake.MonadError m] (cycle : Lake.Cycle Lake.BuildKey) :
          m α

          Log build cycle and error.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[reducible, inline]
            abbrev Lake.IndexBuildFn (m : TypeType v) :

            A build function for any element of the Lake build index.

            Equations
            Instances For
              @[reducible, inline]
              abbrev Lake.IndexT (m : TypeType v) (α : Type) :

              A transformer to equip a monad with a build function for the Lake index.

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

                The top-level monad for Lake build functions.

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

                  The top-level monad for Lake build functions. Renamed FetchM.

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

                    The old build monad. Uses should generally be replaced by FetchM.

                    Equations
                    Instances For
                      @[inline]

                      Fetch the result associated with the info using the Lake build index.

                      Equations
                      • self.fetch build = cast (build self)
                      Instances For

                        Wraps stray I/O, logs, and errors in x into the produced job.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          def Lake.registerJob {α : Type} (caption : String) (job : Lake.Job α) (optional : optParam Bool false) :

                          Registers the job for the top-level build monitor, (e.g., the Lake CLI progress UI), assigning it caption.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            def Lake.withRegisterJob {α : Type} (caption : String) (x : Lake.FetchM (Lake.Job α)) (optional : optParam Bool false) :

                            Registers the produced job for the top-level build monitor (e.g., the Lake CLI progress UI), assigning it caption.

                            Stray I/O, logs, and errors produced by x will be wrapped into the job.

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

                              Registers the produced job for the top-level build monitor if it is not already (i.e., it has an empty caption).

                              Equations
                              Instances For