-
Notifications
You must be signed in to change notification settings - Fork 403
/
Run.lean
106 lines (98 loc) · 3.65 KB
/
Run.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
/-
Copyright (c) 2021 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone, Gabriel Ebner, Sebastian Ullrich
-/
import Lake.Util.Lock
import Lake.Build.Index
/-! # Build Runner
This module defines the top-level functions used to execute a
Lake build, monitor its progress, and await the result.
-/
open System
namespace Lake
/-- Create a fresh build context from a workspace and a build configuration. -/
def mkBuildContext (ws : Workspace) (config : BuildConfig) : BaseIO BuildContext := do
return {
opaqueWs := ws,
toBuildConfig := config,
registeredJobs := ← IO.mkRef #[],
leanTrace := Hash.ofString ws.lakeEnv.leanGithash
}
/--
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`).
-/
def Workspace.runFetchM
(ws : Workspace) (build : FetchM α) (cfg : BuildConfig := {})
: IO α := do
let ctx ← mkBuildContext ws cfg
let out ← if cfg.useStdout then IO.getStdout else IO.getStderr
let useANSI ← out.isTty
let verbosity := cfg.verbosity
let showProgress :=
(cfg.noBuild && verbosity == .verbose) ||
verbosity != .quiet
let caption := "Computing build jobs"
let header := s!"[?/?] {caption}"
if showProgress then
out.putStr header; out.flush
let (io, a?, log) ← IO.FS.withIsolatedStreams (build.run.run'.run ctx).captureLog
let failLv : LogLevel := if ctx.failIfWarnings then .warning else .error
let failed := log.any (·.level ≥ failLv)
if !failed && io.isEmpty && !log.hasVisibleEntries verbosity then
if showProgress then
if useANSI then out.putStr "\x1B[2K\r" else out.putStr "\n"
else
unless showProgress do
out.putStr header
out.putStr "\n"
if failed || log.hasVisibleEntries verbosity then
let v := if failed then .verbose else verbosity
log.replay (logger := MonadLog.stream out v)
unless io.isEmpty do
out.putStr "stdout/stderr:\n"
out.putStr io
out.flush
let failures := if failed then #[caption] else #[]
let jobs ← ctx.registeredJobs.get
let numJobs := jobs.size
let failures ← numJobs.foldM (init := failures) fun i s => Prod.snd <$> StateT.run (s := s) do
let (caption, job) := jobs[i]!
let header := s!"[{i+1}/{numJobs}] {caption}"
if showProgress then
out.putStr header; out.flush
let log := (← job.wait).state
let failed := log.any (·.level ≥ failLv)
if failed then modify (·.push caption)
if !(failed || log.hasVisibleEntries verbosity) then
if showProgress then
if useANSI then out.putStr "\x1B[2K\r" else out.putStr "\n"
else
unless showProgress do
out.putStr header
out.putStr "\n"
let v := if failed then .verbose else verbosity
log.replay (logger := MonadLog.stream out v)
out.flush
if failures.isEmpty then
let some a := a?
| error "build failed"
return a
else
out.putStr "Some build steps logged failures:\n"
failures.forM (out.putStr s!"- {·}\n")
error "build failed"
/-- Run a build function in the Workspace's context and await the result. -/
@[inline] def Workspace.runBuild
(ws : Workspace) (build : FetchM (BuildJob α)) (cfg : BuildConfig := {})
: IO α := do
let job ← ws.runFetchM build cfg
let some a ← job.wait? | error "build failed"
return a
/-- Produce a build job in the Lake monad's workspace and await the result. -/
@[inline] def runBuild
(build : FetchM (BuildJob α)) (cfg : BuildConfig := {})
: LakeT IO α := do
(← getWorkspace).runBuild build cfg