-
Notifications
You must be signed in to change notification settings - Fork 336
/
Basic.lean
88 lines (68 loc) · 2.77 KB
/
Basic.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
/-
Copyright (c) 2021 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
import Lake.Util.Log
import Lake.Util.Exit
import Lake.Util.Task
import Lake.Util.Lift
import Lake.Config.Context
import Lake.Build.Trace
open System
namespace Lake
/-- Exit code to return if `--no-build` is set and a build is required. -/
def noBuildCode : ExitCode := 3
/-- Configuration options for a Lake build. -/
structure BuildConfig where
oldMode : Bool := false
trustHash : Bool := true
/-- Early exit if a target has to be rebuilt. -/
noBuild : Bool := false
verbosity : Verbosity := .normal
/--
Fail the top-level build if warnings have been logged.
Unlike some build systems, this does **NOT** convert warnings to errors,
and it does not abort jobs when warnings are logged (i.e., dependent jobs
will still continue unimpeded).
-/
failIfWarnings : Bool := false
/-- Report build output on `stdout`. Otherwise, Lake uses `stderr`. -/
useStdout : Bool := false
abbrev JobResult α := EResult Nat Log α
abbrev JobTask α := BaseIOTask (JobResult α)
/-- A Lake job. -/
structure Job (α : Type u) where
task : JobTask α
/-- A Lake context with a build configuration and additional build data. -/
structure BuildContext extends BuildConfig, Context where
leanTrace : BuildTrace
registeredJobs : IO.Ref (Array (String × Job Unit))
/-- A transformer to equip a monad with a `BuildContext`. -/
abbrev BuildT := ReaderT BuildContext
instance [Pure m] : MonadLift LakeM (BuildT m) where
monadLift x := fun ctx => pure <| x.run ctx.toContext
@[inline] def getLeanTrace [Monad m] : BuildT m BuildTrace :=
(·.leanTrace) <$> readThe BuildContext
@[inline] def getBuildConfig [Monad m] : BuildT m BuildConfig :=
(·.toBuildConfig) <$> readThe BuildContext
@[inline] def getIsOldMode [Monad m] : BuildT m Bool :=
(·.oldMode) <$> getBuildConfig
@[inline] def getTrustHash [Monad m] : BuildT m Bool :=
(·.trustHash) <$> getBuildConfig
@[inline] def getNoBuild [Monad m] : BuildT m Bool :=
(·.noBuild) <$> getBuildConfig
@[inline] def getVerbosity [Monad m] : BuildT m Verbosity :=
(·.verbosity) <$> getBuildConfig
@[inline] def getIsVerbose [Monad m] : BuildT m Bool :=
(· == .verbose) <$> getVerbosity
@[inline] def getIsQuiet [Monad m] : BuildT m Bool :=
(· == .quiet) <$> getVerbosity
/-- The internal core monad of Lake builds. Not intended for user use. -/
abbrev CoreBuildM := BuildT LogIO
/-- The monad of asynchronous Lake jobs. -/
abbrev JobM := CoreBuildM
/-- The monad used to spawn asynchronous Lake build jobs. Lifts into `FetchM`. -/
abbrev SpawnM := BuildT BaseIO
/-- The monad used to spawn asynchronous Lake build jobs. **Replaced by `SpawnM`.** -/
@[deprecated SpawnM] abbrev SchedulerM := SpawnM