Documentation

Lake.Build.Run

Build Runner #

This module defines the top-level functions used to execute a Lake build, monitor its progress, and await the result.

Create a fresh build context from a workspace and a build configuration.

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

    Unicode icons that make up the spinner in animation order.

    Equations
    Instances For

      Context of the Lake build monitor.

      Instances For

        State of the Lake build monitor.

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

          Monad of the Lake build monitor.

          Equations
          Instances For
            @[inline]
            Equations
            Instances For

              The ANSI escape sequence for clearing the current line and resetting the cursor back to the start.

              Equations
              Instances For
                @[inline]

                Like IO.FS.Stream.flush, but ignores errors.

                Equations
                Instances For
                  @[inline]

                  Like IO.FS.Stream.putStr, but panics on errors.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[inline]
                    Equations
                    Instances For
                      @[inline]
                      Equations
                      Instances For
                        def Lake.Monitor.renderProgress (running : Array Lake.OpaqueJob) (unfinished : Array Lake.OpaqueJob) (h : 0 < unfinished.size) :
                        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
                              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.monitorJobs (jobs : Array Lake.OpaqueJob) (out : IO.FS.Stream) (failLv : Lake.LogLevel) (outLv : Lake.LogLevel) (minAction : Lake.JobAction) (showOptional : Bool) (useAnsi : Bool) (showProgress : Bool) (resetCtrl : optParam String "") (initFailures : optParam (Array String) #[]) (totalJobs : optParam Nat jobs.size) (updateFrequency : optParam Nat 100) :

                                  The job monitor function. An auxiliary definition for runFetchM.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    def Lake.Workspace.runFetchM {α : Type} (ws : Lake.Workspace) (build : Lake.FetchM α) (cfg : optParam Lake.BuildConfig { oldMode := false, trustHash := true, noBuild := false, verbosity := Lake.Verbosity.normal, failLv := Lake.LogLevel.error, outLv := Lake.Verbosity.normal.minLogLv, out := Lake.OutStream.stderr, ansiMode := Lake.AnsiMode.auto }) :
                                    IO α

                                    Run a build function in the Workspace's context using the provided configuration. Reports incremental build progress and build logs. In quiet mode, only reports failing build jobs (e.g., when using -q or non-verbose --no-build).

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      @[inline]
                                      def Lake.Workspace.runBuild {α : Type} (ws : Lake.Workspace) (build : Lake.FetchM (Lake.BuildJob α)) (cfg : optParam Lake.BuildConfig { oldMode := false, trustHash := true, noBuild := false, verbosity := Lake.Verbosity.normal, failLv := Lake.LogLevel.error, outLv := Lake.Verbosity.normal.minLogLv, out := Lake.OutStream.stderr, ansiMode := Lake.AnsiMode.auto }) :
                                      IO α

                                      Run a build function in the Workspace's context and await the result.

                                      Equations
                                      • ws.runBuild build cfg = do let jobws.runFetchM build cfg let __discrliftM job.wait? match __discr with | some a => pure a | x => Lake.error "build failed"
                                      Instances For
                                        @[inline]
                                        def Lake.runBuild {α : Type} (build : Lake.FetchM (Lake.BuildJob α)) (cfg : optParam Lake.BuildConfig { oldMode := false, trustHash := true, noBuild := false, verbosity := Lake.Verbosity.normal, failLv := Lake.LogLevel.error, outLv := Lake.Verbosity.normal.minLogLv, out := Lake.OutStream.stderr, ansiMode := Lake.AnsiMode.auto }) :

                                        Produce a build job in the Lake monad's workspace and await the result.

                                        Equations
                                        • Lake.runBuild build cfg = do let __do_liftLake.getWorkspace liftM (__do_lift.runBuild build cfg)
                                        Instances For