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.

source
def Lake.mkBuildContext (ws : Lake.Workspace) (config : Lake.BuildConfig) :
BaseIO Lake.BuildContext

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
    source
    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, failIfWarnings := false, useStdout := false }) :
    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
      source
      @[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, failIfWarnings := false, useStdout := false }) :
      IO α

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

      Equations
      • ws.runBuild build cfg = do let job ← ws.runFetchM build cfg let __discr ← liftM job.wait? match __discr with | some a => pure a | x => Lake.error "build failed"
      Instances For
        source
        @[inline]
        def Lake.runBuild {α : Type} (build : Lake.FetchM (Lake.BuildJob α)) (cfg : optParam Lake.BuildConfig { oldMode := false, trustHash := true, noBuild := false, verbosity := Lake.Verbosity.normal, failIfWarnings := false, useStdout := false }) :
        Lake.LakeT IO α

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

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