feat: lake: build monitor improvements (#4127)
The new Lake build monitor is now more selective, accurate, and prettier in what it prints. **Key Changes:** * Poll jobs at a fixed frequency (100ms), updating the caption and finished job count. * Add `action` field to jobs to record information about what jobs do. It enables distinguishing between jobs which build something, fetch from a store, or reload logs from the cache. * At standard verbosity, print build captions only when a job is know to build or fetch something (i.e., `action >= .fetch`). * Add an icon and color to job captions based on their log-level / build status. Also add color to levels in logs. * Add `--ansi`/`--no-ansi` to toggle Lake's use of ANSI escape codes. * Fix some `v4.8.0-rc1` bugs and `--old`. Closes #2822.
This commit is contained in:
Mac Malone
GitHub
parent
4d2ff6fb04
commit
7648bf255c
30 changed files with 979 additions and 400 deletions
|
|
@ -24,68 +24,170 @@ structure BuildConfig where
|
|||
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
|
||||
Fail the top-level build if entries of at least this level have been logged.
|
||||
|
||||
abbrev JobResult α := ELogResult α
|
||||
Unlike some build systems, this does **NOT** convert such log entries to
|
||||
errors, and it does not abort jobs when warnings are logged (i.e.,
|
||||
dependent jobs will still continue unimpeded).
|
||||
-/
|
||||
failLv : LogLevel := .error
|
||||
/--
|
||||
The stream to which Lake reports build progress.
|
||||
By default, Lake uses `stderr`.
|
||||
-/
|
||||
out : OutStream := .stderr
|
||||
/-- Whether to use ANSI escape codes in build output. -/
|
||||
ansiMode : AnsiMode := .auto
|
||||
|
||||
/-- The minimum log level for an log entry to be reported. -/
|
||||
@[inline] def BuildConfig.outLv (cfg : BuildConfig) : LogLevel :=
|
||||
cfg.verbosity.minLogLv
|
||||
|
||||
/--
|
||||
Whether the build should show progress information.
|
||||
|
||||
`Verbosity.quiet` hides progress and, for a `noBuild`,
|
||||
`Verbosity.verbose` shows progress.
|
||||
-/
|
||||
def BuildConfig.showProgress (cfg : BuildConfig) : Bool :=
|
||||
(cfg.noBuild ∧ cfg.verbosity == .verbose) ∨ cfg.verbosity != .quiet
|
||||
|
||||
/-- Information on what this job did. -/
|
||||
inductive JobAction
|
||||
/-- No information about this job's action is available. -/
|
||||
| unknown
|
||||
/-- Tried to replay a cached build action (set by `buildFileUnlessUpToDate`) -/
|
||||
| replay
|
||||
/-- Tried to fetch a build from a store (can be set by `buildUnlessUpToDate?`) -/
|
||||
| fetch
|
||||
/-- Tried to perform a build action (set by `buildUnlessUpToDate?`) -/
|
||||
| build
|
||||
deriving Inhabited, Repr, DecidableEq, Ord
|
||||
|
||||
instance : LT JobAction := ltOfOrd
|
||||
instance : LE JobAction := leOfOrd
|
||||
instance : Min JobAction := minOfLe
|
||||
instance : Max JobAction := maxOfLe
|
||||
|
||||
@[inline] def JobAction.merge (a b : JobAction) : JobAction :=
|
||||
max a b
|
||||
|
||||
def JobAction.verb (failed : Bool) : JobAction → String
|
||||
| .unknown => if failed then "Running" else "Ran"
|
||||
| .replay => if failed then "Replaying" else "Replayed"
|
||||
| .fetch => if failed then "Fetching" else "Fetched"
|
||||
| .build => if failed then "Building" else "Built"
|
||||
|
||||
/-- Mutable state of a Lake job. -/
|
||||
structure JobState where
|
||||
/-- The job's log. -/
|
||||
log : Log := {}
|
||||
/-- Tracks whether this job performed any significant build action. -/
|
||||
action : JobAction := .unknown
|
||||
|
||||
/--
|
||||
Resets the job state after a checkpoint (e.g., registering the job).
|
||||
Preserves state that downstream jobs want to depend on while resetting
|
||||
job-local state that should not be inherited by downstream jobs.
|
||||
-/
|
||||
@[inline] def JobState.renew (_ : JobState) : JobState where
|
||||
log := {}
|
||||
action := .unknown
|
||||
|
||||
def JobState.merge (a b : JobState) : JobState where
|
||||
log := a.log ++ b.log
|
||||
action := a.action.merge b.action
|
||||
|
||||
@[inline] def JobState.modifyLog (f : Log → Log) (s : JobState) :=
|
||||
{s with log := f s.log}
|
||||
|
||||
/-- The result of a Lake job. -/
|
||||
abbrev JobResult α := EResult Log.Pos JobState α
|
||||
|
||||
/-- The `Task` of a Lake job. -/
|
||||
abbrev JobTask α := BaseIOTask (JobResult α)
|
||||
|
||||
/-- A Lake job. -/
|
||||
structure Job (α : Type u) where
|
||||
task : JobTask α
|
||||
caption : String
|
||||
|
||||
/-- 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))
|
||||
registeredJobs : IO.Ref (Array (Job Unit))
|
||||
|
||||
/-- A transformer to equip a monad with a `BuildContext`. -/
|
||||
abbrev BuildT := ReaderT BuildContext
|
||||
|
||||
/-- The monad of asynchronous Lake jobs. Lifts into `FetchM`. -/
|
||||
abbrev JobM := BuildT <| EStateT Log.Pos JobState BaseIO
|
||||
|
||||
instance [Pure m] : MonadLift LakeM (BuildT m) where
|
||||
monadLift x := fun ctx => pure <| x.run ctx.toContext
|
||||
|
||||
@[inline] def getBuildContext [Monad m] : BuildT m BuildContext :=
|
||||
instance : MonadStateOf Log JobM where
|
||||
get := (·.log) <$> get
|
||||
set log := modify fun s => {s with log}
|
||||
modifyGet f := modifyGet fun s => let (a, log) := f s.log; (a, {s with log})
|
||||
|
||||
instance : MonadStateOf JobState JobM := inferInstance
|
||||
|
||||
instance : MonadLog JobM := .ofMonadState
|
||||
instance : MonadError JobM := ELog.monadError
|
||||
instance : Alternative JobM := ELog.alternative
|
||||
instance : MonadLift LogIO JobM := ⟨ELogT.takeAndRun⟩
|
||||
|
||||
/-- Record that this job is trying to perform some action. -/
|
||||
@[inline] def updateAction (action : JobAction) : JobM PUnit :=
|
||||
modify fun s => {s with action := s.action.merge action}
|
||||
|
||||
/-- A monad equipped with a Lake build context. -/
|
||||
abbrev MonadBuild (m : Type → Type u) :=
|
||||
MonadReaderOf BuildContext m
|
||||
|
||||
@[inline] def getBuildContext [MonadBuild m] : m BuildContext :=
|
||||
readThe BuildContext
|
||||
|
||||
@[inline] def getLeanTrace [Monad m] : BuildT m BuildTrace :=
|
||||
@[inline] def getLeanTrace [Functor m] [MonadBuild m] : m BuildTrace :=
|
||||
(·.leanTrace) <$> getBuildContext
|
||||
|
||||
@[inline] def getBuildConfig [Monad m] : BuildT m BuildConfig :=
|
||||
@[inline] def getBuildConfig [Functor m] [MonadBuild m] : m BuildConfig :=
|
||||
(·.toBuildConfig) <$> getBuildContext
|
||||
|
||||
@[inline] def getIsOldMode [Monad m] : BuildT m Bool :=
|
||||
@[inline] def getIsOldMode [Functor m] [MonadBuild m] : m Bool :=
|
||||
(·.oldMode) <$> getBuildConfig
|
||||
|
||||
@[inline] def getTrustHash [Monad m] : BuildT m Bool :=
|
||||
@[inline] def getTrustHash [Functor m] [MonadBuild m] : m Bool :=
|
||||
(·.trustHash) <$> getBuildConfig
|
||||
|
||||
@[inline] def getNoBuild [Monad m] : BuildT m Bool :=
|
||||
@[inline] def getNoBuild [Functor m] [MonadBuild m] : m Bool :=
|
||||
(·.noBuild) <$> getBuildConfig
|
||||
|
||||
@[inline] def getVerbosity [Monad m] : BuildT m Verbosity :=
|
||||
@[inline] def getVerbosity [Functor m] [MonadBuild m] : m Verbosity :=
|
||||
(·.verbosity) <$> getBuildConfig
|
||||
|
||||
@[inline] def getIsVerbose [Monad m] : BuildT m Bool :=
|
||||
@[inline] def getIsVerbose [Functor m] [MonadBuild m] : m Bool :=
|
||||
(· == .verbose) <$> getVerbosity
|
||||
|
||||
@[inline] def getIsQuiet [Monad m] : BuildT m Bool :=
|
||||
@[inline] def getIsQuiet [Functor m] [MonadBuild m] : 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
|
||||
|
||||
/--
|
||||
Logs a build step with `message`.
|
||||
|
||||
**Deprecated:** Build steps are now managed by a top-level build monitor.
|
||||
As a result, this no longer functions the way it used to. It now just logs the
|
||||
`message` via `logVerbose`.
|
||||
-/
|
||||
@[deprecated] def logStep (message : String) : JobM Unit := do
|
||||
logVerbose message
|
||||
|
|
|
|||
|
|
@ -24,13 +24,23 @@ and will be rebuilt on different host platforms.
|
|||
-/
|
||||
def platformTrace := pureHash System.Platform.target
|
||||
|
||||
/-- Check if the `info` is up-to-date by comparing `depTrace` with `traceFile`. -/
|
||||
/--
|
||||
Checks if the `info` is up-to-date by comparing `depTrace` with `traceFile`.
|
||||
If old mode is enabled (e.g., `--old`), uses the modification time of `oldTrace`
|
||||
as the point of comparison instead.
|
||||
-/
|
||||
@[specialize] def BuildTrace.checkUpToDate
|
||||
[CheckExists ι] [GetMTime ι]
|
||||
(info : ι) (depTrace : BuildTrace) (traceFile : FilePath)
|
||||
(oldTrace := depTrace)
|
||||
: JobM Bool := do
|
||||
if (← getIsOldMode) then
|
||||
depTrace.checkAgainstTime info
|
||||
if (← oldTrace.checkAgainstTime info) then
|
||||
return true
|
||||
else if let some hash ← Hash.load? traceFile then
|
||||
depTrace.checkAgainstHash info hash
|
||||
else
|
||||
return false
|
||||
else
|
||||
depTrace.checkAgainstFile info traceFile
|
||||
|
||||
|
|
@ -42,12 +52,14 @@ Returns whether `info` was already up-to-date.
|
|||
@[inline] def buildUnlessUpToDate?
|
||||
[CheckExists ι] [GetMTime ι] (info : ι)
|
||||
(depTrace : BuildTrace) (traceFile : FilePath) (build : JobM PUnit)
|
||||
(action : JobAction := .build) (oldTrace := depTrace)
|
||||
: JobM Bool := do
|
||||
if (← depTrace.checkUpToDate info traceFile) then
|
||||
if (← depTrace.checkUpToDate info traceFile oldTrace) then
|
||||
return true
|
||||
else if (← getNoBuild) then
|
||||
IO.Process.exit noBuildCode.toUInt8
|
||||
else
|
||||
updateAction action
|
||||
build
|
||||
depTrace.writeToFile traceFile
|
||||
return false
|
||||
|
|
@ -122,6 +134,7 @@ def buildFileUnlessUpToDate
|
|||
let logFile := FilePath.mk <| file.toString ++ ".log.json"
|
||||
let build := cacheBuildLog logFile build
|
||||
if (← buildUnlessUpToDate? file depTrace traceFile build) then
|
||||
updateAction .replay
|
||||
replayBuildLog logFile
|
||||
fetchFileTrace file
|
||||
else
|
||||
|
|
|
|||
|
|
@ -12,7 +12,7 @@ The build function definition for a Lean executable.
|
|||
-/
|
||||
|
||||
def LeanExe.recBuildExe (self : LeanExe) : FetchM (BuildJob FilePath) :=
|
||||
withRegisterJob s!"Linking {self.fileName}" do
|
||||
withRegisterJob s!"{self.name}" do
|
||||
let imports ← self.root.transImports.fetch
|
||||
let mut linkJobs := #[← self.root.o.fetch]
|
||||
for mod in imports do for facet in mod.nativeFacets self.supportInterpreter do
|
||||
|
|
|
|||
|
|
@ -116,6 +116,13 @@ module_data o.noexport : BuildJob FilePath
|
|||
|
||||
/-! ## Package Facets -/
|
||||
|
||||
/--
|
||||
A package's *optional* cloud build release.
|
||||
Does not fail if the release cannot be fetched.
|
||||
-/
|
||||
abbrev Package.optReleaseFacet := `optRelease
|
||||
package_data optRelease : BuildJob Bool
|
||||
|
||||
/-- A package's cloud build release. -/
|
||||
abbrev Package.releaseFacet := `release
|
||||
package_data release : BuildJob Unit
|
||||
|
|
|
|||
|
|
@ -23,12 +23,7 @@ namespace Lake
|
|||
abbrev RecBuildM :=
|
||||
CallStackT BuildKey <| BuildT <| ELogT <| StateT BuildStore <| BaseIO
|
||||
|
||||
instance : MonadLift IO RecBuildM := ⟨MonadError.runIO⟩
|
||||
|
||||
@[inline] def RecBuildM.runLogIO (x : LogIO α) : RecBuildM α :=
|
||||
fun _ _ log store => (·, store) <$> x log
|
||||
|
||||
instance : MonadLift LogIO RecBuildM := ⟨RecBuildM.runLogIO⟩
|
||||
instance : MonadLift LogIO RecBuildM := ⟨ELogT.takeAndRun⟩
|
||||
|
||||
/-- Run a recursive build. -/
|
||||
@[inline] def RecBuildM.run
|
||||
|
|
@ -64,7 +59,7 @@ abbrev FetchM := IndexT RecBuildM
|
|||
@[deprecated FetchM] abbrev IndexBuildM := FetchM
|
||||
|
||||
/-- The old build monad. **Uses should generally be replaced by `FetchM`.** -/
|
||||
@[deprecated FetchM] abbrev BuildM := CoreBuildM
|
||||
@[deprecated FetchM] abbrev BuildM := BuildT LogIO
|
||||
|
||||
/-- Fetch the result associated with the info using the Lake build index. -/
|
||||
@[inline] def BuildInfo.fetch (self : BuildInfo) [FamilyOut BuildData self.key α] : FetchM α :=
|
||||
|
|
@ -72,19 +67,46 @@ abbrev FetchM := IndexT RecBuildM
|
|||
|
||||
export BuildInfo (fetch)
|
||||
|
||||
/-- Register the produced job for the CLI progress UI. -/
|
||||
def withRegisterJob
|
||||
(caption : String) (x : FetchM (Job α))
|
||||
/-- Wraps stray I/O, logs, and errors in `x` into the produced job. -/
|
||||
def ensureJob (x : FetchM (Job α))
|
||||
: FetchM (Job α) := fun fetch stack ctx log store => do
|
||||
let iniPos := log.endPos
|
||||
match (← (withLoggedIO x) fetch stack ctx log store) with
|
||||
| (.ok job log, store) =>
|
||||
let (log, jobLog) := log.split iniPos
|
||||
let regJob := job.mapResult (discard <| ·.modifyState (jobLog ++ ·))
|
||||
ctx.registeredJobs.modify (·.push (caption, regJob))
|
||||
return (.ok job.clearLog log, store)
|
||||
let job := if jobLog.isEmpty then job else job.mapResult (sync := true)
|
||||
(·.modifyState (.modifyLog (jobLog ++ ·)))
|
||||
return (.ok job log, store)
|
||||
| (.error _ log, store) =>
|
||||
let (log, jobLog) := log.split iniPos
|
||||
let regJob := ⟨Task.pure <| .error 0 jobLog⟩
|
||||
ctx.registeredJobs.modify (·.push (caption, regJob))
|
||||
return (.ok .error log, store)
|
||||
return (.ok (.error jobLog) log, store)
|
||||
|
||||
/--
|
||||
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.
|
||||
-/
|
||||
@[inline] def withRegisterJob
|
||||
(caption : String) (x : FetchM (Job α))
|
||||
: FetchM (Job α) := do
|
||||
let job ← ensureJob x
|
||||
let job := job.setCaption caption
|
||||
let regJob := job.mapResult (sync := true) discard
|
||||
(← readThe BuildContext).registeredJobs.modify (·.push regJob)
|
||||
return job.renew
|
||||
|
||||
/--
|
||||
Registers the produced job for the top-level build monitor
|
||||
if it is not already (i.e., it has an empty caption).
|
||||
-/
|
||||
@[inline] def maybeRegisterJob
|
||||
(fallbackCaption : String) (job : Job α)
|
||||
: FetchM (Job α) := do
|
||||
if job.caption.isEmpty then
|
||||
let job := job.setCaption fallbackCaption
|
||||
let regJob := job.mapResult (sync := true) discard
|
||||
(← readThe BuildContext).registeredJobs.modify (·.push regJob)
|
||||
return job.renew
|
||||
else
|
||||
return job
|
||||
|
|
|
|||
|
|
@ -19,7 +19,7 @@ by `lake lean` to build the imports of a file.
|
|||
Returns the set of module dynlibs built (so they can be loaded by Lean).
|
||||
-/
|
||||
def buildImportsAndDeps (leanFile : FilePath) (imports : Array Module) : FetchM (BuildJob (Array FilePath)) := do
|
||||
withRegisterJob s!"Building imports of '{leanFile}'" do
|
||||
withRegisterJob s!"imports ({leanFile})" do
|
||||
if imports.isEmpty then
|
||||
-- build the package's (and its dependencies') `extraDepTarget`
|
||||
(← getRootPackage).extraDep.fetch <&> (·.map fun _ => #[])
|
||||
|
|
|
|||
|
|
@ -29,15 +29,15 @@ dynamically-typed equivalent.
|
|||
cast (by rw [← h.family_key_eq_type]) build
|
||||
|
||||
def ExternLib.recBuildStatic (lib : ExternLib) : FetchM (BuildJob FilePath) :=
|
||||
withRegisterJob s!"Building {lib.staticTargetName.toString}" do
|
||||
withRegisterJob s!"{lib.staticTargetName.toString}:static" do
|
||||
lib.config.getJob <$> fetch (lib.pkg.target lib.staticTargetName)
|
||||
|
||||
def ExternLib.recBuildShared (lib : ExternLib) : FetchM (BuildJob FilePath) :=
|
||||
withRegisterJob s!"Linking {lib.staticTargetName.toString}" do
|
||||
withRegisterJob s!"{lib.staticTargetName.toString}:shared" do
|
||||
buildLeanSharedLibOfStatic (← lib.static.fetch) lib.linkArgs
|
||||
|
||||
def ExternLib.recComputeDynlib (lib : ExternLib) : FetchM (BuildJob Dynlib) := do
|
||||
withRegisterJob s!"Computing {lib.staticTargetName.toString} dynlib" do
|
||||
withRegisterJob s!"{lib.staticTargetName.toString}:dynlib" do
|
||||
computeDynlibOfShared (← lib.shared.fetch)
|
||||
|
||||
/-!
|
||||
|
|
|
|||
|
|
@ -220,6 +220,10 @@ abbrev Package.facet (facet : Name) (self : Package) : BuildInfo :=
|
|||
abbrev Package.release (self : Package) : BuildInfo :=
|
||||
self.facet releaseFacet
|
||||
|
||||
@[inherit_doc optReleaseFacet]
|
||||
abbrev Package.optRelease (self : Package) : BuildInfo :=
|
||||
self.facet optReleaseFacet
|
||||
|
||||
@[inherit_doc extraDepFacet]
|
||||
abbrev Package.extraDep (self : Package) : BuildInfo :=
|
||||
self.facet extraDepFacet
|
||||
|
|
|
|||
|
|
@ -12,23 +12,39 @@ namespace Lake
|
|||
|
||||
namespace Job
|
||||
|
||||
@[inline] protected def pure (a : α) : Job α :=
|
||||
{task := Task.pure (.ok a {})}
|
||||
@[inline] def ofTask (task : JobTask α) (caption := "") : Job α :=
|
||||
{task, caption}
|
||||
|
||||
@[inline] protected def error (log : Log := {}) (caption := "") : Job α :=
|
||||
{task := Task.pure (.error 0 {log}), caption}
|
||||
|
||||
@[inline] protected def pure (a : α) (log : Log := {}) (caption := "") : Job α :=
|
||||
{task := Task.pure (.ok a {log}), caption}
|
||||
|
||||
instance : Pure Job := ⟨Job.pure⟩
|
||||
instance [Inhabited α] : Inhabited (Job α) := ⟨pure default⟩
|
||||
|
||||
@[inline] protected def nop : Job Unit :=
|
||||
pure ()
|
||||
@[inline] protected def nop (log : Log := {}) (caption := "") : Job Unit :=
|
||||
.pure () log caption
|
||||
|
||||
@[inline] protected def error (l : Log := {}) : Job α :=
|
||||
{task := Task.pure (.error 0 l)}
|
||||
/-- Sets the job's caption. -/
|
||||
@[inline] def setCaption (caption : String) (job : Job α) : Job α :=
|
||||
{job with caption}
|
||||
|
||||
/-- Sets the job's caption if the job's current caption is empty. -/
|
||||
@[inline] def setCaption? (caption : String) (job : Job α) : Job α :=
|
||||
if job.caption.isEmpty then {job with caption} else job
|
||||
|
||||
@[inline] def mapResult
|
||||
(f : JobResult α → JobResult β) (self : Job α)
|
||||
(prio := Task.Priority.default) (sync := false)
|
||||
: Job β :=
|
||||
{task := self.task.map f prio sync}
|
||||
{self with task := self.task.map f prio sync}
|
||||
|
||||
@[inline] def bindTask [Monad m]
|
||||
(f : JobTask α → m (JobTask β)) (self : Job α)
|
||||
: m (Job β) :=
|
||||
return {self with task := ← f self.task}
|
||||
|
||||
@[inline] protected def map
|
||||
(f : α → β) (self : Job α)
|
||||
|
|
@ -38,25 +54,20 @@ instance [Inhabited α] : Inhabited (Job α) := ⟨pure default⟩
|
|||
|
||||
instance : Functor Job where map := Job.map
|
||||
|
||||
@[inline] def clearLog (self : Job α) : Job α :=
|
||||
/--
|
||||
Resets the job's state after a checkpoint (e.g., registering the job).
|
||||
Preserves information that downstream jobs want to depend on while resetting
|
||||
job-local information that should not be inherited by downstream jobs.
|
||||
-/
|
||||
def renew (self : Job α) : Job α :=
|
||||
self.mapResult (sync := true) fun
|
||||
| .ok a _ => .ok a {}
|
||||
| .error .. => .error 0 {}
|
||||
|
||||
@[inline] def attempt (self : Job α) : Job Bool :=
|
||||
self.mapResult (sync := true) fun
|
||||
| .error n l => .ok false (l.dropFrom n)
|
||||
| .ok _ l => .ok true l
|
||||
|
||||
@[inline] def attempt? (self : Job α) : Job (Option α) :=
|
||||
self.mapResult (sync := true) fun
|
||||
| .error n l => .ok none (l.dropFrom n)
|
||||
| .ok a l => .ok (some a) l
|
||||
| .ok a s => .ok a s.renew
|
||||
| .error _ s => .error 0 s.renew
|
||||
|
||||
/-- Spawn a job that asynchronously performs `act`. -/
|
||||
@[inline] protected def async
|
||||
(act : JobM α) (prio := Task.Priority.default)
|
||||
: SpawnM (Job α) := fun ctx => Job.mk <$> do
|
||||
: SpawnM (Job α) := fun ctx => .ofTask <$> do
|
||||
BaseIO.asTask (prio := prio) do (withLoggedIO act) ctx {}
|
||||
|
||||
/-- Wait a the job to complete and return the result. -/
|
||||
|
|
@ -76,8 +87,8 @@ Logs the job's log and throws if there was an error.
|
|||
-/
|
||||
@[inline] protected def await (self : Job α) : LogIO α := do
|
||||
match (← self.wait) with
|
||||
| .error n l => l.replay; throw n
|
||||
| .ok a l => l.replay; pure a
|
||||
| .error n {log, ..} => log.replay; throw n
|
||||
| .ok a {log, ..} => log.replay; pure a
|
||||
|
||||
/--
|
||||
`let c ← a.bindSync b` asynchronously performs the action `b`
|
||||
|
|
@ -86,10 +97,10 @@ after the job `a` completes.
|
|||
@[inline] protected def bindSync
|
||||
(self : Job α) (f : α → JobM β)
|
||||
(prio := Task.Priority.default) (sync := false)
|
||||
: SpawnM (Job β) := fun ctx => Job.mk <$> do
|
||||
BaseIO.mapTask (t := self.task) (prio := prio) (sync := sync) fun
|
||||
| EResult.ok a l => (withLoggedIO (f a)) ctx l
|
||||
| EResult.error n l => return .error n l
|
||||
: SpawnM (Job β) := fun ctx => self.bindTask fun task => do
|
||||
BaseIO.mapTask (t := task) (prio := prio) (sync := sync) fun
|
||||
| EResult.ok a s => (withLoggedIO (f a)) ctx s
|
||||
| EResult.error n s => return .error n s
|
||||
|
||||
/--
|
||||
`let c ← a.bindAsync b` asynchronously performs the action `b`
|
||||
|
|
@ -98,14 +109,13 @@ after the job `a` completes and then merges into the job produced by `b`.
|
|||
@[inline] protected def bindAsync
|
||||
(self : Job α) (f : α → SpawnM (Job β))
|
||||
(prio := Task.Priority.default) (sync := false)
|
||||
: SpawnM (Job β) := fun ctx => Job.mk <$> do
|
||||
BaseIO.bindTask self.task (prio := prio) (sync := sync) fun
|
||||
| .ok a l => do
|
||||
: SpawnM (Job β) := fun ctx => self.bindTask fun task => do
|
||||
BaseIO.bindTask task (prio := prio) (sync := sync) fun
|
||||
| .ok a sa => do
|
||||
let job ← f a ctx
|
||||
if l.isEmpty then return job.task else
|
||||
return job.task.map (prio := prio) (sync := true) fun
|
||||
| EResult.ok a l' => .ok a (l ++ l')
|
||||
| EResult.error n l' => .error ⟨l.size + n.val⟩ (l ++ l')
|
||||
| EResult.ok a sb => .ok a (sa.merge sb)
|
||||
| EResult.error n sb => .error ⟨sa.log.size + n.val⟩ (sa.merge sb)
|
||||
| .error n l => return Task.pure (.error n l)
|
||||
|
||||
/--
|
||||
|
|
@ -115,12 +125,12 @@ results of `a` and `b`. The job `c` errors if either `a` or `b` error.
|
|||
@[inline] def zipWith
|
||||
(f : α → β → γ) (x : Job α) (y : Job β)
|
||||
(prio := Task.Priority.default) (sync := false)
|
||||
: BaseIO (Job γ) := Job.mk <$> do
|
||||
BaseIO.bindTask x.task (prio := prio) (sync := true) fun rx =>
|
||||
BaseIO.mapTask (t := y.task) (prio := prio) (sync := sync) fun ry =>
|
||||
: Job γ := Job.ofTask $
|
||||
x.task.bind (prio := prio) (sync := true) fun rx =>
|
||||
y.task.map (prio := prio) (sync := sync) fun ry =>
|
||||
match rx, ry with
|
||||
| .ok a la, .ok b lb => return .ok (f a b) (la ++ lb)
|
||||
| rx, ry => return .error 0 (rx.state ++ ry.state)
|
||||
| .ok a sa, .ok b sb => .ok (f a b) (sa.merge sb)
|
||||
| rx, ry => .error 0 (rx.state.merge ry.state)
|
||||
|
||||
end Job
|
||||
|
||||
|
|
@ -146,16 +156,6 @@ namespace BuildJob
|
|||
|
||||
instance : Pure BuildJob := ⟨BuildJob.pure⟩
|
||||
|
||||
@[inline] def attempt (self : BuildJob α) : BuildJob Bool :=
|
||||
{task := self.toJob.task.map fun
|
||||
| .error _ l => .ok (false, nilTrace) l
|
||||
| .ok (_, t) l => .ok (true, t) l}
|
||||
|
||||
@[inline] def attempt? (self : BuildJob α) : BuildJob (Option α) :=
|
||||
{task := self.toJob.task.map fun
|
||||
| .error _ l => .ok (none, nilTrace) l
|
||||
| .ok (a, t) l => .ok (some a, t) l}
|
||||
|
||||
@[inline] protected def map (f : α → β) (self : BuildJob α) : BuildJob β :=
|
||||
mk <| (fun (a,t) => (f a,t)) <$> self.toJob
|
||||
|
||||
|
|
@ -180,25 +180,25 @@ instance : Functor BuildJob where
|
|||
@[inline] protected def wait? (self : BuildJob α) : BaseIO (Option α) :=
|
||||
(·.map (·.1)) <$> self.toJob.wait?
|
||||
|
||||
def add (t1 : BuildJob α) (t2 : BuildJob β) : BaseIO (BuildJob α) :=
|
||||
mk <$> t1.toJob.zipWith (fun a _ => a) t2.toJob
|
||||
def add (t1 : BuildJob α) (t2 : BuildJob β) : BuildJob α :=
|
||||
mk <| t1.toJob.zipWith (fun a _ => a) t2.toJob
|
||||
|
||||
def mix (t1 : BuildJob α) (t2 : BuildJob β) : BaseIO (BuildJob Unit) :=
|
||||
mk <$> t1.toJob.zipWith (fun (_,t) (_,t') => ((), mixTrace t t')) t2.toJob
|
||||
def mix (t1 : BuildJob α) (t2 : BuildJob β) : BuildJob Unit :=
|
||||
mk <| t1.toJob.zipWith (fun (_,t) (_,t') => ((), mixTrace t t')) t2.toJob
|
||||
|
||||
def mixList (jobs : List (BuildJob α)) : BaseIO (BuildJob Unit) := ofJob <$> do
|
||||
jobs.foldrM (·.toJob.zipWith (fun (_,t') t => mixTrace t t') ·) (pure nilTrace)
|
||||
def mixList (jobs : List (BuildJob α)) : Id (BuildJob Unit) := ofJob $
|
||||
jobs.foldr (·.toJob.zipWith (fun (_,t') t => mixTrace t t') ·) (pure nilTrace)
|
||||
|
||||
def mixArray (jobs : Array (BuildJob α)) : BaseIO (BuildJob Unit) := ofJob <$> do
|
||||
jobs.foldlM (·.zipWith (fun t (_,t') => mixTrace t t') ·.toJob) (pure nilTrace)
|
||||
def mixArray (jobs : Array (BuildJob α)) : Id (BuildJob Unit) := ofJob $
|
||||
jobs.foldl (·.zipWith (fun t (_,t') => mixTrace t t') ·.toJob) (pure nilTrace)
|
||||
|
||||
protected def zipWith
|
||||
def zipWith
|
||||
(f : α → β → γ) (t1 : BuildJob α) (t2 : BuildJob β)
|
||||
: BaseIO (BuildJob γ) :=
|
||||
mk <$> t1.toJob.zipWith (fun (a,t) (b,t') => (f a b, mixTrace t t')) t2.toJob
|
||||
: BuildJob γ :=
|
||||
mk <| t1.toJob.zipWith (fun (a,t) (b,t') => (f a b, mixTrace t t')) t2.toJob
|
||||
|
||||
def collectList (jobs : List (BuildJob α)) : BaseIO (BuildJob (List α)) :=
|
||||
jobs.foldrM (BuildJob.zipWith List.cons) (pure [])
|
||||
def collectList (jobs : List (BuildJob α)) : Id (BuildJob (List α)) :=
|
||||
return jobs.foldr (zipWith List.cons) (pure [])
|
||||
|
||||
def collectArray (jobs : Array (BuildJob α)) : BaseIO (BuildJob (Array α)) :=
|
||||
jobs.foldlM (BuildJob.zipWith Array.push) (pure #[])
|
||||
def collectArray (jobs : Array (BuildJob α)) : Id (BuildJob (Array α)) :=
|
||||
return jobs.foldl (zipWith Array.push) (pure #[])
|
||||
|
|
|
|||
|
|
@ -23,6 +23,18 @@ def toString : (self : BuildKey) → String
|
|||
| targetFacet p t f => s!"{p}/{t}:{f}"
|
||||
| customTarget p t => s!"{p}/{t}"
|
||||
|
||||
/-- Like the default `toString`, but without disambiguation markers. -/
|
||||
def toSimpleString : (self : BuildKey) → String
|
||||
| moduleFacet m f => s!"{m}:{f}"
|
||||
| packageFacet p f => s!"{p}:{f}"
|
||||
| targetFacet p t f => s!"{p}/{t}:{eraseHead f}"
|
||||
| customTarget p t => s!"{p}/{t}"
|
||||
where
|
||||
eraseHead : Name → Name
|
||||
| .anonymous | .str .anonymous _ | .num .anonymous _ => .anonymous
|
||||
| .str p s => .str (eraseHead p) s
|
||||
| .num p s => .num (eraseHead p) s
|
||||
|
||||
instance : ToString BuildKey := ⟨(·.toString)⟩
|
||||
|
||||
def quickCmp (k k' : BuildKey) : Ordering :=
|
||||
|
|
|
|||
|
|
@ -45,7 +45,7 @@ protected def LeanLib.recBuildLean
|
|||
(self : LeanLib) : FetchM (BuildJob Unit) := do
|
||||
let mods ← self.modules.fetch
|
||||
mods.foldlM (init := BuildJob.nil) fun job mod => do
|
||||
job.mix <| ← mod.leanArts.fetch
|
||||
return job.mix <| ← mod.leanArts.fetch
|
||||
|
||||
/-- The `LibraryFacetConfig` for the builtin `leanArtsFacet`. -/
|
||||
def LeanLib.leanArtsFacetConfig : LibraryFacetConfig leanArtsFacet :=
|
||||
|
|
@ -53,8 +53,12 @@ def LeanLib.leanArtsFacetConfig : LibraryFacetConfig leanArtsFacet :=
|
|||
|
||||
@[specialize] protected def LeanLib.recBuildStatic
|
||||
(self : LeanLib) (shouldExport : Bool) : FetchM (BuildJob FilePath) := do
|
||||
let exports := if shouldExport then "w/ exports" else "w/o exports"
|
||||
withRegisterJob s!"Building {self.staticLibFileName} ({exports})" do
|
||||
let suffix :=
|
||||
if (← getIsVerbose) then
|
||||
if shouldExport then " (with exports)" else " (without exports)"
|
||||
else
|
||||
""
|
||||
withRegisterJob s!"{self.name}:static{suffix}" do
|
||||
let mods ← self.modules.fetch
|
||||
let oJobs ← mods.concatMapM fun mod =>
|
||||
mod.nativeFacets shouldExport |>.mapM fun facet => fetch <| mod.facet facet.name
|
||||
|
|
@ -74,7 +78,7 @@ def LeanLib.staticExportFacetConfig : LibraryFacetConfig staticExportFacet :=
|
|||
|
||||
protected def LeanLib.recBuildShared
|
||||
(self : LeanLib) : FetchM (BuildJob FilePath) := do
|
||||
withRegisterJob s!"Linking {self.sharedLibFileName}" do
|
||||
withRegisterJob s!"{self.name}:shared" do
|
||||
let mods ← self.modules.fetch
|
||||
let oJobs ← mods.concatMapM fun mod =>
|
||||
mod.nativeFacets true |>.mapM fun facet => fetch <| mod.facet facet.name
|
||||
|
|
@ -91,7 +95,7 @@ def LeanLib.sharedFacetConfig : LibraryFacetConfig sharedFacet :=
|
|||
/-- Build the `extraDepTargets` for the library and its package. -/
|
||||
def LeanLib.recBuildExtraDepTargets (self : LeanLib) : FetchM (BuildJob Unit) := do
|
||||
self.extraDepTargets.foldlM (init := ← self.pkg.extraDep.fetch) fun job target => do
|
||||
job.mix <| ← self.pkg.fetchTargetJob target
|
||||
return job.mix <| ← self.pkg.fetchTargetJob target
|
||||
|
||||
/-- The `LibraryFacetConfig` for the builtin `extraDepFacet`. -/
|
||||
def LeanLib.extraDepFacetConfig : LibraryFacetConfig extraDepFacet :=
|
||||
|
|
|
|||
|
|
@ -149,12 +149,12 @@ Fetch its dependencies and then elaborate the Lean source file, producing
|
|||
all possible artifacts (i.e., `.olean`, `ilean`, `.c`, and `.bc`).
|
||||
-/
|
||||
def Module.recBuildLean (mod : Module) : FetchM (BuildJob Unit) := do
|
||||
withRegisterJob s!"Building {mod.name}" do
|
||||
withRegisterJob mod.name.toString do
|
||||
(← mod.deps.fetch).bindSync fun (dynlibPath, dynlibs) depTrace => do
|
||||
let argTrace : BuildTrace := pureHash mod.leanArgs
|
||||
let srcTrace : BuildTrace ← computeTrace { path := mod.leanFile : TextFilePath }
|
||||
let modTrace := (← getLeanTrace).mix <| argTrace.mix <| srcTrace.mix depTrace
|
||||
let upToDate ← buildUnlessUpToDate? mod modTrace mod.traceFile do
|
||||
let upToDate ← buildUnlessUpToDate? (oldTrace := srcTrace) mod modTrace mod.traceFile do
|
||||
let hasLLVM := Lean.Internal.hasLLVMBackend ()
|
||||
let bcFile? := if hasLLVM then some mod.bcFile else none
|
||||
cacheBuildLog mod.logFile do
|
||||
|
|
@ -166,6 +166,7 @@ def Module.recBuildLean (mod : Module) : FetchM (BuildJob Unit) := do
|
|||
if hasLLVM then
|
||||
discard <| cacheFileHash mod.bcFile
|
||||
if upToDate then
|
||||
updateAction .replay
|
||||
replayBuildLog mod.logFile
|
||||
return ((), depTrace)
|
||||
|
||||
|
|
@ -203,8 +204,9 @@ def Module.bcFacetConfig : ModuleFacetConfig bcFacet :=
|
|||
Recursively build the module's object file from its C file produced by `lean`
|
||||
with `-DLEAN_EXPORTING` set, which exports Lean symbols defined within the C files.
|
||||
-/
|
||||
def Module.recBuildLeanCToOExport (self : Module) : FetchM (BuildJob FilePath) :=
|
||||
withRegisterJob s!"Compiling {self.name}" do
|
||||
def Module.recBuildLeanCToOExport (self : Module) : FetchM (BuildJob FilePath) := do
|
||||
let suffix := if (← getIsVerbose) then " (with exports)" else ""
|
||||
withRegisterJob s!"{self.name}:c.o{suffix}" do
|
||||
-- TODO: add option to pass a target triplet for cross compilation
|
||||
let leancArgs := self.leancArgs ++ #["-DLEAN_EXPORTING"]
|
||||
buildLeanO self.coExportFile (← self.c.fetch) self.weakLeancArgs leancArgs
|
||||
|
|
@ -217,8 +219,9 @@ def Module.coExportFacetConfig : ModuleFacetConfig coExportFacet :=
|
|||
Recursively build the module's object file from its C file produced by `lean`.
|
||||
This version does not export any Lean symbols.
|
||||
-/
|
||||
def Module.recBuildLeanCToONoExport (self : Module) : FetchM (BuildJob FilePath) :=
|
||||
withRegisterJob s!"Compiling {self.name}" do
|
||||
def Module.recBuildLeanCToONoExport (self : Module) : FetchM (BuildJob FilePath) := do
|
||||
let suffix := if (← getIsVerbose) then " (without exports)" else ""
|
||||
withRegisterJob s!"{self.name}:c.o{suffix}" do
|
||||
-- TODO: add option to pass a target triplet for cross compilation
|
||||
buildLeanO self.coNoExportFile (← self.c.fetch) self.weakLeancArgs self.leancArgs
|
||||
|
||||
|
|
@ -233,7 +236,7 @@ def Module.coFacetConfig : ModuleFacetConfig coFacet :=
|
|||
|
||||
/-- Recursively build the module's object file from its bitcode file produced by `lean`. -/
|
||||
def Module.recBuildLeanBcToO (self : Module) : FetchM (BuildJob FilePath) := do
|
||||
withRegisterJob s!"Compiling {self.name}" do
|
||||
withRegisterJob s!"{self.name}:bc.o" do
|
||||
-- TODO: add option to pass a target triplet for cross compilation
|
||||
buildLeanO self.bcoFile (← self.bc.fetch) self.weakLeancArgs self.leancArgs
|
||||
|
||||
|
|
@ -265,7 +268,7 @@ def Module.oFacetConfig : ModuleFacetConfig oFacet :=
|
|||
-- TODO: Return `BuildJob OrdModuleSet × OrdPackageSet` or `OrdRBSet Dynlib`
|
||||
/-- Recursively build the shared library of a module (e.g., for `--load-dynlib`). -/
|
||||
def Module.recBuildDynlib (mod : Module) : FetchM (BuildJob Dynlib) :=
|
||||
withRegisterJob s!"Linking {mod.name} dynlib" do
|
||||
withRegisterJob s!"{mod.name}:dynlib" do
|
||||
|
||||
-- Compute dependencies
|
||||
let transImports ← mod.transImports.fetch
|
||||
|
|
|
|||
|
|
@ -32,16 +32,16 @@ def Package.recBuildExtraDepTargets (self : Package) : FetchM (BuildJob Unit) :=
|
|||
let mut job := BuildJob.nil
|
||||
-- Build dependencies' extra dep targets
|
||||
for dep in self.deps do
|
||||
job ← job.mix <| ← dep.extraDep.fetch
|
||||
job := job.mix <| ← dep.extraDep.fetch
|
||||
-- Fetch pre-built release if desired and this package is a dependency
|
||||
if self.name ≠ (← getWorkspace).root.name ∧ self.preferReleaseBuild then
|
||||
job ← job.add <| ← (← self.release.fetch).attempt.bindSync fun success t => do
|
||||
job := job.add <| ← (← self.optRelease.fetch).bindSync fun success t => do
|
||||
unless success do
|
||||
logWarning "fetching cloud release failed; falling back to local build"
|
||||
logWarning "failed to fetch cloud release; falling back to local build"
|
||||
return ((), t)
|
||||
-- Build this package's extra dep targets
|
||||
for target in self.extraDepTargets do
|
||||
job ← job.mix <| ← self.fetchTargetJob target
|
||||
job := job.mix <| ← self.fetchTargetJob target
|
||||
return job
|
||||
|
||||
/-- The `PackageFacetConfig` for the builtin `dynlibFacet`. -/
|
||||
|
|
@ -49,31 +49,42 @@ def Package.extraDepFacetConfig : PackageFacetConfig extraDepFacet :=
|
|||
mkFacetJobConfig Package.recBuildExtraDepTargets
|
||||
|
||||
/-- Download and unpack the package's prebuilt release archive (from GitHub). -/
|
||||
def Package.fetchRelease (self : Package) : FetchM (BuildJob Unit) :=
|
||||
withRegisterJob s!"Fetching {self.name} cloud release" <| Job.async do
|
||||
def Package.fetchOptRelease (self : Package) : FetchM (BuildJob Bool) := Job.async do
|
||||
updateAction .fetch
|
||||
let repo := GitRepo.mk self.dir
|
||||
let repoUrl? := self.releaseRepo? <|> self.remoteUrl?
|
||||
let some repoUrl := repoUrl? <|> (← repo.getFilteredRemoteUrl?)
|
||||
| error <| s!"{self.name}: wanted prebuilt release, " ++
|
||||
"but package's repository URL was not known; it may need to set `releaseRepo?`"
|
||||
| logInfo s!"{self.name}: wanted prebuilt release, \
|
||||
but package's repository URL was not known; it may need to set 'releaseRepo'"
|
||||
return (false, .nil)
|
||||
let some tag ← repo.findTag?
|
||||
| error <| s!"{self.name}: wanted prebuilt release, " ++
|
||||
"but could not find an associated tag for the package's revision"
|
||||
| logInfo s!"{self.name}: wanted prebuilt release, \
|
||||
but could not find an associated tag for the package's revision"
|
||||
return (false, .nil)
|
||||
let url := s!"{repoUrl}/releases/download/{tag}/{self.buildArchive}"
|
||||
let logName := s!"{self.name}/{tag}/{self.buildArchive}"
|
||||
let depTrace := Hash.ofString url
|
||||
let traceFile := FilePath.mk <| self.buildArchiveFile.toString ++ ".trace"
|
||||
let upToDate ← buildUnlessUpToDate? self.buildArchiveFile depTrace traceFile do
|
||||
let upToDate ← buildUnlessUpToDate? (action := .fetch) self.buildArchiveFile depTrace traceFile do
|
||||
logVerbose s!"downloading {logName}"
|
||||
download url self.buildArchiveFile
|
||||
unless upToDate && (← self.buildDir.pathExists) do
|
||||
logVerbose s!"unpacking {logName}"
|
||||
untar self.buildArchiveFile self.buildDir
|
||||
return ((), .nil)
|
||||
return (true, .nil)
|
||||
|
||||
/-- The `PackageFacetConfig` for the builtin `optReleaseFacet`. -/
|
||||
def Package.optReleaseFacetConfig : PackageFacetConfig optReleaseFacet :=
|
||||
mkFacetJobConfig (·.fetchOptRelease)
|
||||
|
||||
/-- The `PackageFacetConfig` for the builtin `releaseFacet`. -/
|
||||
def Package.releaseFacetConfig : PackageFacetConfig releaseFacet :=
|
||||
mkFacetJobConfig (·.fetchRelease)
|
||||
mkFacetJobConfig fun pkg =>
|
||||
withRegisterJob s!"{pkg.name}:release" do
|
||||
(← pkg.optRelease.fetch).bindSync fun success t => do
|
||||
unless success do
|
||||
error "failed to fetch cloud release"
|
||||
return ((), t)
|
||||
|
||||
/-- Perform a build job after first checking for a cloud release for the package. -/
|
||||
def Package.afterReleaseAsync (self : Package) (build : SpawnM (Job α)) : FetchM (Job α) := do
|
||||
|
|
@ -98,4 +109,5 @@ def initPackageFacetConfigs : DNameMap PackageFacetConfig :=
|
|||
DNameMap.empty
|
||||
|>.insert depsFacet depsFacetConfig
|
||||
|>.insert extraDepFacet extraDepFacetConfig
|
||||
|>.insert optReleaseFacet optReleaseFacetConfig
|
||||
|>.insert releaseFacet releaseFacetConfig
|
||||
|
|
|
|||
|
|
@ -25,6 +25,150 @@ def mkBuildContext (ws : Workspace) (config : BuildConfig) : BaseIO BuildContext
|
|||
leanTrace := Hash.ofString ws.lakeEnv.leanGithash
|
||||
}
|
||||
|
||||
/-- Context of the Lake build monitor. -/
|
||||
structure MonitorContext where
|
||||
totalJobs : Nat
|
||||
out : IO.FS.Stream
|
||||
outLv : LogLevel
|
||||
failLv : LogLevel
|
||||
showProgress : Bool
|
||||
useAnsi : Bool
|
||||
/-- How often to poll jobs (in milliseconds). -/
|
||||
updateFrequency : Nat := 100
|
||||
|
||||
/-- State of the Lake build monitor. -/
|
||||
structure MonitorState where
|
||||
jobNo : Nat := 1
|
||||
jobs : Array (Job Unit)
|
||||
failures : Array String
|
||||
resetCtrl : String
|
||||
lastUpdate : Nat
|
||||
|
||||
/-- Monad of the Lake build monitor. -/
|
||||
abbrev MonitorM := ReaderT MonitorContext <| StateT MonitorState BaseIO
|
||||
|
||||
@[inline] def MonitorM.run
|
||||
(ctx : MonitorContext) (s : MonitorState) (self : MonitorM α)
|
||||
: BaseIO (α × MonitorState) :=
|
||||
self ctx s
|
||||
|
||||
/--
|
||||
The ANSI escape sequence for clearing the current line
|
||||
and resetting the cursor back to the start.
|
||||
-/
|
||||
def Ansi.resetLine : String :=
|
||||
"\x1B[2K\r"
|
||||
|
||||
/-- Like `IO.FS.Stream.flush`, but ignores errors. -/
|
||||
@[inline] def flush (out : IO.FS.Stream) : BaseIO PUnit :=
|
||||
out.flush |>.catchExceptions fun _ => pure ()
|
||||
|
||||
/-- Like `IO.FS.Stream.putStr`, but panics on errors. -/
|
||||
@[inline] def print! (out : IO.FS.Stream) (s : String) : BaseIO PUnit :=
|
||||
out.putStr s |>.catchExceptions fun e =>
|
||||
panic! s!"[{decl_name%} failed: {e}] {repr s}"
|
||||
|
||||
namespace Monitor
|
||||
|
||||
@[inline] def print (s : String) : MonitorM PUnit := do
|
||||
print! (← read).out s
|
||||
|
||||
@[inline] nonrec def flush : MonitorM PUnit := do
|
||||
flush (← read).out
|
||||
|
||||
def renderProgress : MonitorM PUnit := do
|
||||
let {jobNo, jobs, ..} ← get
|
||||
let {totalJobs, useAnsi, showProgress, ..} ← read
|
||||
if showProgress ∧ useAnsi then
|
||||
if h : 0 < jobs.size then
|
||||
let caption := jobs[0]'h |>.caption
|
||||
let resetCtrl ← modifyGet fun s => (s.resetCtrl, {s with resetCtrl := Ansi.resetLine})
|
||||
print s!"{resetCtrl}[{jobNo}/{totalJobs}] Checking {caption}"
|
||||
flush
|
||||
|
||||
def reportJob (job : Job Unit) : MonitorM PUnit := do
|
||||
let {jobNo, ..} ← get
|
||||
let {totalJobs, failLv, outLv, out, useAnsi, showProgress, ..} ← read
|
||||
let {log, action, ..} := job.task.get.state
|
||||
let maxLv := log.maxLv
|
||||
let failed := log.hasEntries ∧ maxLv ≥ failLv
|
||||
if failed then
|
||||
modify fun s => {s with failures := s.failures.push job.caption}
|
||||
let hasOutput := failed ∨ (log.hasEntries ∧ maxLv ≥ outLv)
|
||||
if hasOutput ∨ (showProgress ∧ action ≥ .fetch) then
|
||||
let verb := action.verb failed
|
||||
let icon := if hasOutput then maxLv.icon else '✔'
|
||||
let caption := s!"{icon} [{jobNo}/{totalJobs}] {verb} {job.caption}"
|
||||
let caption :=
|
||||
if useAnsi then
|
||||
let color := if hasOutput then maxLv.ansiColor else "32"
|
||||
Ansi.chalk color caption
|
||||
else
|
||||
caption
|
||||
let resetCtrl ← modifyGet fun s => (s.resetCtrl, {s with resetCtrl := ""})
|
||||
print s!"{resetCtrl}{caption}\n"
|
||||
if hasOutput then
|
||||
let outLv := if failed then .trace else outLv
|
||||
log.replay (logger := .stream out outLv useAnsi)
|
||||
flush
|
||||
|
||||
def pollJobs : MonitorM PUnit := do
|
||||
let prevJobs ← modifyGet fun s => (s.jobs, {s with jobs := #[]})
|
||||
for h : i in [0:prevJobs.size] do
|
||||
let job := prevJobs[i]'h.upper
|
||||
if (← IO.hasFinished job.task) then
|
||||
reportJob job
|
||||
modify fun s => {s with jobNo := s.jobNo + 1}
|
||||
else
|
||||
modify fun s => {s with jobs := s.jobs.push job}
|
||||
|
||||
def sleep : MonitorM PUnit := do
|
||||
let now ← IO.monoMsNow
|
||||
let lastUpdate ← modifyGet fun s => (s.lastUpdate, {s with lastUpdate := now})
|
||||
let sleepTime : Nat := (← read).updateFrequency - (now - lastUpdate)
|
||||
if sleepTime > 0 then
|
||||
IO.sleep sleepTime.toUInt32
|
||||
|
||||
partial def loop : MonitorM PUnit := do
|
||||
renderProgress
|
||||
pollJobs
|
||||
if 0 < (← get).jobs.size then
|
||||
renderProgress
|
||||
sleep
|
||||
loop
|
||||
|
||||
def main : MonitorM PUnit := do
|
||||
loop
|
||||
let resetCtrl ← modifyGet fun s => (s.resetCtrl, {s with resetCtrl := ""})
|
||||
unless resetCtrl.isEmpty do
|
||||
print resetCtrl
|
||||
flush
|
||||
|
||||
end Monitor
|
||||
|
||||
/-- The job monitor function. An auxiliary definition for `runFetchM`. -/
|
||||
def monitorJobs
|
||||
(jobs : Array (Job Unit))
|
||||
(out : IO.FS.Stream)
|
||||
(failLv outLv : LogLevel)
|
||||
(useAnsi showProgress : Bool)
|
||||
(resetCtrl : String := "")
|
||||
(initFailures : Array String := #[])
|
||||
(totalJobs := jobs.size)
|
||||
(updateFrequency := 100)
|
||||
: BaseIO (Array String) := do
|
||||
let ctx := {
|
||||
totalJobs, out, failLv, outLv,
|
||||
useAnsi, showProgress, updateFrequency
|
||||
}
|
||||
let s := {
|
||||
jobs, resetCtrl
|
||||
lastUpdate := ← IO.monoMsNow
|
||||
failures := initFailures
|
||||
}
|
||||
let (_,s) ← Monitor.main.run ctx s
|
||||
return s.failures
|
||||
|
||||
/--
|
||||
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
|
||||
|
|
@ -33,62 +177,51 @@ failing build jobs (e.g., when using `-q` or non-verbose `--no-build`).
|
|||
def Workspace.runFetchM
|
||||
(ws : Workspace) (build : FetchM α) (cfg : BuildConfig := {})
|
||||
: IO α := do
|
||||
-- Configure
|
||||
let out ← cfg.out.get
|
||||
let useAnsi ← cfg.ansiMode.isEnabled out
|
||||
let outLv := cfg.outLv
|
||||
let failLv := cfg.failLv
|
||||
let showProgress := cfg.showProgress
|
||||
let showAnsiProgress := showProgress ∧ useAnsi
|
||||
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
|
||||
-- Job Computation
|
||||
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 showAnsiProgress then
|
||||
print! out s!"[?/?] {caption}"
|
||||
flush out
|
||||
let (a?, log) ← ((withLoggedIO build).run.run'.run ctx).run?
|
||||
let failed := log.hasEntries ∧ log.maxLv ≥ failLv
|
||||
if failed ∨ (log.hasEntries ∧ log.maxLv ≥ outLv) then
|
||||
let icon := log.maxLv.icon
|
||||
let caption := s!"{icon} [?/?] {caption}"
|
||||
if useAnsi then
|
||||
let caption := Ansi.chalk log.maxLv.ansiColor caption
|
||||
if showProgress then
|
||||
if useANSI then out.putStr "\x1B[2K\r" else out.putStr "\n"
|
||||
print! out s!"{Ansi.resetLine}{caption}"
|
||||
else
|
||||
print! out caption
|
||||
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
|
||||
print! out caption
|
||||
print! out "\n"
|
||||
let outLv := if failed then .trace else outLv
|
||||
log.replay (logger := .stream out outLv useAnsi)
|
||||
flush out
|
||||
let failures := if failed then #[caption] else #[]
|
||||
-- Job Monitor
|
||||
let jobs ← ctx.registeredJobs.get
|
||||
let resetCtrl := if showAnsiProgress then Ansi.resetLine else ""
|
||||
let failures ← monitorJobs jobs out failLv outLv useAnsi showProgress
|
||||
(resetCtrl := resetCtrl) (initFailures := failures)
|
||||
-- Failure Report
|
||||
if failures.isEmpty then
|
||||
let some a := a?
|
||||
| error "build failed"
|
||||
| error "top-level build failed"
|
||||
return a
|
||||
else
|
||||
out.putStr "Some build steps logged failures:\n"
|
||||
failures.forM (out.putStr s!"- {·}\n")
|
||||
print! out "Some builds logged failures:\n"
|
||||
failures.forM (print! out s!"- {·}\n")
|
||||
flush out
|
||||
error "build failed"
|
||||
|
||||
/-- Run a build function in the Workspace's context and await the result. -/
|
||||
|
|
|
|||
|
|
@ -29,8 +29,9 @@ structure BuildSpec where
|
|||
| throw <| CliError.nonCliFacet facetType facet
|
||||
return {info, getBuildJob := h ▸ getJob}
|
||||
|
||||
@[inline] protected def BuildSpec.fetch (self : BuildSpec) : FetchM (BuildJob Unit) :=
|
||||
self.getBuildJob <$> self.info.fetch
|
||||
@[inline] protected def BuildSpec.fetch (self : BuildSpec) : FetchM (BuildJob Unit) := do
|
||||
maybeRegisterJob (self.info.key.toSimpleString) <| ← do
|
||||
self.getBuildJob <$> self.info.fetch
|
||||
|
||||
def buildSpecs (specs : Array BuildSpec) : FetchM (BuildJob Unit) := do
|
||||
BuildJob.mixArray (← specs.mapM (·.fetch))
|
||||
|
|
|
|||
|
|
@ -43,7 +43,10 @@ OPTIONS:
|
|||
--rehash, -H hash all files for traces (do not trust `.hash` files)
|
||||
--update, -U update manifest before building
|
||||
--reconfigure, -R elaborate configuration files instead of using OLeans
|
||||
--wfail report a build failure if warnings are logged
|
||||
--wfail fail build if warnings are logged
|
||||
--iofail fail build if any I/O or other info is logged
|
||||
--ansi, --no-ansi toggle the use of ANSI escape codes to prettify output
|
||||
--no-build exit immediately if a build target is not up-to-date
|
||||
|
||||
See `lake help <command>` for more information on a specific command."
|
||||
|
||||
|
|
|
|||
|
|
@ -40,7 +40,8 @@ structure LakeOptions where
|
|||
oldMode : Bool := false
|
||||
trustHash : Bool := true
|
||||
noBuild : Bool := false
|
||||
failIfWarnings : Bool := false
|
||||
failLv : LogLevel := .error
|
||||
ansiMode : AnsiMode := .auto
|
||||
|
||||
/-- Get the Lean installation. Error if missing. -/
|
||||
def LakeOptions.getLeanInstall (opts : LakeOptions) : Except CliError LeanInstall :=
|
||||
|
|
@ -75,13 +76,14 @@ def LakeOptions.mkLoadConfig (opts : LakeOptions) : EIO CliError LoadConfig :=
|
|||
}
|
||||
|
||||
/-- Make a `BuildConfig` from a `LakeOptions`. -/
|
||||
def LakeOptions.mkBuildConfig (opts : LakeOptions) (useStdout := false) : BuildConfig where
|
||||
def LakeOptions.mkBuildConfig (opts : LakeOptions) (out := OutStream.stderr) : BuildConfig where
|
||||
oldMode := opts.oldMode
|
||||
trustHash := opts.trustHash
|
||||
noBuild := opts.noBuild
|
||||
verbosity := opts.verbosity
|
||||
failIfWarnings := opts.failIfWarnings
|
||||
useStdout := useStdout
|
||||
failLv := opts.failLv
|
||||
ansiMode := opts.ansiMode
|
||||
out := out
|
||||
|
||||
export LakeOptions (mkLoadConfig mkBuildConfig)
|
||||
|
||||
|
|
@ -98,7 +100,7 @@ def CliM.run (self : CliM α) (args : List String) : BaseIO ExitCode := do
|
|||
main.run
|
||||
|
||||
instance : MonadLift LogIO CliStateM :=
|
||||
⟨fun x => do MainM.runLogIO x (← get).verbosity⟩
|
||||
⟨fun x => do MainM.runLogIO x (← get).verbosity.minLogLv (← get).ansiMode⟩
|
||||
|
||||
/-! ## Argument Parsing -/
|
||||
|
||||
|
|
@ -160,7 +162,10 @@ def lakeLongOption : (opt : String) → CliM PUnit
|
|||
| "--old" => modifyThe LakeOptions ({· with oldMode := true})
|
||||
| "--no-build" => modifyThe LakeOptions ({· with noBuild := true})
|
||||
| "--rehash" => modifyThe LakeOptions ({· with trustHash := false})
|
||||
| "--wfail" => modifyThe LakeOptions ({· with failIfWarnings := true})
|
||||
| "--wfail" => modifyThe LakeOptions ({· with failLv := .warning})
|
||||
| "--iofail" => modifyThe LakeOptions ({· with failLv := .info})
|
||||
| "--ansi" => modifyThe LakeOptions ({· with ansiMode := .ansi})
|
||||
| "--no-ansi" => modifyThe LakeOptions ({· with ansiMode := .noAnsi})
|
||||
| "--dir" => do let rootDir ← takeOptArg "--dir" "path"; modifyThe LakeOptions ({· with rootDir})
|
||||
| "--file" => do let configFile ← takeOptArg "--file" "path"; modifyThe LakeOptions ({· with configFile})
|
||||
| "--lean" => do setLean <| ← takeOptArg "--lean" "path or command"
|
||||
|
|
@ -302,8 +307,11 @@ protected def build : CliM PUnit := do
|
|||
let ws ← loadWorkspace config opts.updateDeps
|
||||
let targetSpecs ← takeArgs
|
||||
let specs ← parseTargetSpecs ws targetSpecs
|
||||
let buildConfig := mkBuildConfig opts (useStdout := true)
|
||||
let buildConfig := mkBuildConfig opts (out := .stdout)
|
||||
let showProgress := buildConfig.showProgress
|
||||
ws.runBuild (buildSpecs specs) buildConfig
|
||||
if showProgress then
|
||||
IO.println "Build completed successfully."
|
||||
|
||||
protected def resolveDeps : CliM PUnit := do
|
||||
processOptions lakeOption
|
||||
|
|
@ -333,7 +341,7 @@ protected def setupFile : CliM PUnit := do
|
|||
let buildConfig := mkBuildConfig opts
|
||||
let filePath ← takeArg "file path"
|
||||
let imports ← takeArgs
|
||||
setupFile loadConfig filePath imports buildConfig opts.verbosity
|
||||
setupFile loadConfig filePath imports buildConfig
|
||||
|
||||
protected def test : CliM PUnit := do
|
||||
processOptions lakeOption
|
||||
|
|
|
|||
|
|
@ -29,17 +29,20 @@ The `setup-file` command is used internally by the Lean 4 server.
|
|||
-/
|
||||
def setupFile
|
||||
(loadConfig : LoadConfig) (path : FilePath) (imports : List String := [])
|
||||
(buildConfig : BuildConfig := {}) (verbosity : Verbosity := .normal)
|
||||
(buildConfig : BuildConfig := {})
|
||||
: MainM PUnit := do
|
||||
if (← configFileExists loadConfig.configFile) then
|
||||
if let some errLog := (← IO.getEnv invalidConfigEnvVar) then
|
||||
IO.eprint errLog
|
||||
IO.eprintln s!"Invalid Lake configuration. Please restart the server after fixing the Lake configuration file."
|
||||
exit 1
|
||||
let ws ← MainM.runLogIO (loadWorkspace loadConfig) verbosity
|
||||
let outLv := buildConfig.verbosity.minLogLv
|
||||
let ws ← MainM.runLogIO (minLv := outLv) (ansiMode := .noAnsi) do
|
||||
loadWorkspace loadConfig
|
||||
let imports := imports.foldl (init := #[]) fun imps imp =>
|
||||
if let some mod := ws.findModule? imp.toName then imps.push mod else imps
|
||||
let dynlibs ← MainM.runLogIO (ws.runBuild (buildImportsAndDeps path imports) buildConfig) verbosity
|
||||
let dynlibs ← MainM.runLogIO (minLv := outLv) (ansiMode := .noAnsi) do
|
||||
ws.runBuild (buildImportsAndDeps path imports) buildConfig
|
||||
let paths : LeanPaths := {
|
||||
oleanPath := ws.leanPath
|
||||
srcPath := ws.leanSrcPath
|
||||
|
|
@ -67,7 +70,7 @@ with the given additional `args`.
|
|||
-/
|
||||
def serve (config : LoadConfig) (args : Array String) : IO UInt32 := do
|
||||
let (extraEnv, moreServerArgs) ← do
|
||||
let (ws?, log) ← (loadWorkspace config).captureLog
|
||||
let (ws?, log) ← (loadWorkspace config).run?
|
||||
log.replay (logger := MonadLog.stderr)
|
||||
if let some ws := ws? then
|
||||
let ctx := mkLakeContext ws
|
||||
|
|
|
|||
|
|
@ -20,10 +20,13 @@ syntax buildDeclSig :=
|
|||
/-! ## Facet Declarations -/
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
@[inline] def mkModuleFacetJob
|
||||
(mod : Module) (facet : Name) (f : Module → FetchM (BuildJob α))
|
||||
: FetchM (BuildJob α) := do
|
||||
withRegisterJob s!"Building {mod.name}:{facet}" (f mod)
|
||||
abbrev mkModuleFacetDecl
|
||||
(α) (facet : Name)
|
||||
[FamilyDef ModuleData facet (BuildJob α)]
|
||||
(f : Module → FetchM (BuildJob α))
|
||||
: ModuleFacetDecl := .mk facet <| mkFacetJobConfig fun mod => do
|
||||
withRegisterJob (mod.facet facet |>.key.toSimpleString)
|
||||
(f mod)
|
||||
|
||||
/--
|
||||
Define a new module facet. Has one form:
|
||||
|
|
@ -42,21 +45,22 @@ kw:"module_facet " sig:buildDeclSig : command => do
|
|||
| `(buildDeclSig| $id:ident $[$mod?]? : $ty := $defn $[$wds?:whereDecls]?) =>
|
||||
let attr ← withRef kw `(Term.attrInstance| module_facet)
|
||||
let attrs := #[attr] ++ expandAttrs attrs?
|
||||
let name := Name.quoteFrom id id.getId
|
||||
let facetId := mkIdentFrom id <| id.getId.modifyBase (.str · "_modFacet")
|
||||
let facet := Name.quoteFrom id id.getId
|
||||
let declId := mkIdentFrom id <| id.getId.modifyBase (.str · "_modFacet")
|
||||
let mod ← expandOptSimpleBinder mod?
|
||||
`(module_data $id : BuildJob $ty
|
||||
$[$doc?:docComment]? @[$attrs,*] abbrev $facetId : ModuleFacetDecl := {
|
||||
name := $name
|
||||
config := Lake.mkFacetJobConfig fun mod =>
|
||||
Lake.DSL.mkModuleFacetJob (α := $ty) mod $name (fun $mod => $defn)
|
||||
} $[$wds?:whereDecls]?)
|
||||
$[$doc?:docComment]? @[$attrs,*] abbrev $declId :=
|
||||
Lake.DSL.mkModuleFacetDecl $ty $facet (fun $mod => $defn)
|
||||
$[$wds?:whereDecls]?)
|
||||
| stx => Macro.throwErrorAt stx "ill-formed module facet declaration"
|
||||
|
||||
@[inline] def mkPackageFacetJob
|
||||
(pkg : Package) (facet : Name) (f : Package → FetchM (BuildJob α))
|
||||
: FetchM (BuildJob α) := do
|
||||
withRegisterJob s!"Building {pkg.name}:{facet}" (f pkg)
|
||||
abbrev mkPackageFacetDecl
|
||||
(α) (facet : Name)
|
||||
[FamilyDef PackageData facet (BuildJob α)]
|
||||
(f : Package → FetchM (BuildJob α))
|
||||
: PackageFacetDecl := .mk facet <| mkFacetJobConfig fun pkg => do
|
||||
withRegisterJob (pkg.facet facet |>.key.toSimpleString)
|
||||
(f pkg)
|
||||
|
||||
/--
|
||||
Define a new package facet. Has one form:
|
||||
|
|
@ -75,21 +79,22 @@ kw:"package_facet " sig:buildDeclSig : command => do
|
|||
| `(buildDeclSig| $id:ident $[$pkg?]? : $ty := $defn $[$wds?:whereDecls]?) =>
|
||||
let attr ← withRef kw `(Term.attrInstance| package_facet)
|
||||
let attrs := #[attr] ++ expandAttrs attrs?
|
||||
let name := Name.quoteFrom id id.getId
|
||||
let facetId := mkIdentFrom id <| id.getId.modifyBase (.str · "_pkgFacet")
|
||||
let facet := Name.quoteFrom id id.getId
|
||||
let declId := mkIdentFrom id <| id.getId.modifyBase (.str · "_pkgFacet")
|
||||
let pkg ← expandOptSimpleBinder pkg?
|
||||
`(package_data $id : BuildJob $ty
|
||||
$[$doc?]? @[$attrs,*] abbrev $facetId : PackageFacetDecl := {
|
||||
name := $name
|
||||
config := Lake.mkFacetJobConfig fun pkg =>
|
||||
Lake.DSL.mkPackageFacetJob (α := $ty) pkg $name (fun $pkg => $defn)
|
||||
} $[$wds?:whereDecls]?)
|
||||
$[$doc?]? @[$attrs,*] abbrev $declId :=
|
||||
Lake.DSL.mkPackageFacetDecl $ty $facet (fun $pkg => $defn)
|
||||
$[$wds?:whereDecls]?)
|
||||
| stx => Macro.throwErrorAt stx "ill-formed package facet declaration"
|
||||
|
||||
@[inline] def mkLibraryFacetJob
|
||||
(lib : LeanLib) (facet : Name) (f : LeanLib → FetchM (BuildJob α))
|
||||
: FetchM (BuildJob α) := do
|
||||
withRegisterJob s!"Building {lib.name}:{facet}" (f lib)
|
||||
abbrev mkLibraryFacetDecl
|
||||
(α) (facet : Name)
|
||||
[FamilyDef LibraryData facet (BuildJob α)]
|
||||
(f : LeanLib → FetchM (BuildJob α))
|
||||
: LibraryFacetDecl := .mk facet <| mkFacetJobConfig fun lib => do
|
||||
withRegisterJob (lib.facet facet |>.key.toSimpleString)
|
||||
(f lib)
|
||||
|
||||
/--
|
||||
Define a new library facet. Has one form:
|
||||
|
|
@ -108,25 +113,26 @@ kw:"library_facet " sig:buildDeclSig : command => do
|
|||
| `(buildDeclSig| $id:ident $[$lib?]? : $ty := $defn $[$wds?:whereDecls]?) =>
|
||||
let attr ← withRef kw `(Term.attrInstance| library_facet)
|
||||
let attrs := #[attr] ++ expandAttrs attrs?
|
||||
let name := Name.quoteFrom id id.getId
|
||||
let facetId := mkIdentFrom id <| id.getId.modifyBase (.str · "_libFacet")
|
||||
let facet := Name.quoteFrom id id.getId
|
||||
let declId := mkIdentFrom id <| id.getId.modifyBase (.str · "_libFacet")
|
||||
let lib ← expandOptSimpleBinder lib?
|
||||
`(library_data $id : BuildJob $ty
|
||||
$[$doc?]? @[$attrs,*] abbrev $facetId : LibraryFacetDecl := {
|
||||
name := $name
|
||||
config := Lake.mkFacetJobConfig fun lib =>
|
||||
Lake.DSL.mkLibraryFacetJob (α := $ty) lib $name (fun $lib => $defn)
|
||||
} $[$wds?:whereDecls]?)
|
||||
$[$doc?]? @[$attrs,*] abbrev $declId : LibraryFacetDecl :=
|
||||
Lake.DSL.mkLibraryFacetDecl $ty $facet (fun $lib => $defn)
|
||||
$[$wds?:whereDecls]?)
|
||||
| stx => Macro.throwErrorAt stx "ill-formed library facet declaration"
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
/-! ## Custom Target Declaration -/
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
@[inline] def mkTargetJob
|
||||
(pkg : NPackage n) (target : Name) (f : NPackage n → FetchM (BuildJob α))
|
||||
: FetchM (BuildJob α) := do
|
||||
withRegisterJob s!"Building {n}/{target}" (f pkg)
|
||||
abbrev mkTargetDecl
|
||||
(α) (pkgName target : Name)
|
||||
[FamilyDef CustomData (pkgName, target) (BuildJob α)]
|
||||
(f : NPackage pkgName → FetchM (BuildJob α))
|
||||
: TargetDecl := .mk pkgName target <| mkTargetJobConfig fun pkg => do
|
||||
withRegisterJob (pkg.target target |>.key.toSimpleString)
|
||||
(f pkg)
|
||||
|
||||
/--
|
||||
Define a new custom target for the package. Has one form:
|
||||
|
|
@ -151,12 +157,9 @@ kw:"target " sig:buildDeclSig : command => do
|
|||
let pkgName := mkIdentFrom id `_package.name
|
||||
let pkg ← expandOptSimpleBinder pkg?
|
||||
`(family_def $id : CustomData ($pkgName, $name) := BuildJob $ty
|
||||
$[$doc?]? @[$attrs,*] abbrev $id : TargetDecl := {
|
||||
pkg := $pkgName
|
||||
name := $name
|
||||
config := Lake.mkTargetJobConfig fun pkg =>
|
||||
Lake.DSL.mkTargetJob (α := $ty) pkg $name (fun $pkg => $defn)
|
||||
} $[$wds?:whereDecls]?)
|
||||
$[$doc?]? @[$attrs,*] abbrev $id :=
|
||||
Lake.DSL.mkTargetDecl $ty $pkgName $name (fun $pkg => $defn)
|
||||
$[$wds?:whereDecls]?)
|
||||
| stx => Macro.throwErrorAt stx "ill-formed target declaration"
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -34,6 +34,16 @@ instance [Inhabited ε] [Inhabited σ] : Inhabited (EResult ε σ α) where
|
|||
@[inline] def EResult.setState (s : σ') (r : EResult ε σ α) : EResult ε σ' α :=
|
||||
r.modifyState fun _ => s
|
||||
|
||||
/-- Convert a `EResult ε σ α` into `Except ε α × σ`. -/
|
||||
@[inline] def EResult.toProd : EResult ε σ α → Except ε α × σ
|
||||
| .ok a s => (.ok a, s)
|
||||
| .error e s => (.error e, s)
|
||||
|
||||
/-- Convert an `EResult ε σ α` into `Option α × σ`, discarding the exception contents. -/
|
||||
@[inline] def EResult.toProd? : EResult ε σ α → Option α × σ
|
||||
| .ok a s => (some a, s)
|
||||
| .error _ s => (none, s)
|
||||
|
||||
/-- Extract the result `α` from a `EResult ε σ α`. -/
|
||||
@[inline] def EResult.result? : EResult ε σ α → Option α
|
||||
| .ok a _ => some a
|
||||
|
|
@ -65,36 +75,61 @@ def EStateT (ε : Type u) (σ : Type v) (m : Type max u v w → Type x) (α : Ty
|
|||
σ → m (EResult ε σ α)
|
||||
|
||||
namespace EStateT
|
||||
variable {ε ε' : Type u} {σ : Type v} {α β : Type w}
|
||||
|
||||
instance [Inhabited ε] [Pure m] : Inhabited (EStateT ε σ m α) where
|
||||
default := fun s => pure (EResult.error default s)
|
||||
|
||||
/-- Execute an `EStateT` on initial state `init` to get an `EResult` result. -/
|
||||
@[always_inline, inline]
|
||||
def run (init : σ) (self : EStateT ε σ m α) : m (EResult ε σ α) :=
|
||||
self init
|
||||
|
||||
/--
|
||||
Execute an `EStateT` on initial state `init`
|
||||
to get an `Except` result, discarding the final state.
|
||||
-/
|
||||
@[always_inline, inline]
|
||||
def run' {σ : Type max u w} [Functor m] (init : σ) (x : EStateT ε σ m α) : m (Except ε α) :=
|
||||
EResult.toExcept <$> x init
|
||||
|
||||
/-- Convert an `EStateT` to a `StateT`, returning an `Except` result. -/
|
||||
@[inline] def toStateT {ε σ α : Type u} [Functor m] (x : EStateT ε σ m α) : StateT σ m (Except ε α) :=
|
||||
fun s => EResult.toProd <$> x s
|
||||
|
||||
/-- Convert an `EStateT` to a `StateT`, returning an `Option` result. -/
|
||||
@[inline] def toStateT? {ε σ α : Type u} [Functor m] (x : EStateT ε σ m α) : StateT σ m (Option α) :=
|
||||
fun s => EResult.toProd? <$> x s
|
||||
|
||||
/--
|
||||
Execute an `EStateT` on initial state `init`
|
||||
to get an `Option` result, discarding the exception contents.
|
||||
-/
|
||||
@[always_inline, inline]
|
||||
def run? {ε : Type max v w} [Functor m] (init : σ) (x : EStateT ε σ m α) : m (Option α × σ) :=
|
||||
EResult.toProd? <$> x init
|
||||
|
||||
/--
|
||||
Execute an `EStateT` on initial state `init` to get an `Option` result,
|
||||
discarding the final state.
|
||||
-/
|
||||
@[always_inline, inline]
|
||||
def run?' {ε σ α : Type u} [Functor m] (init : σ) (x : EStateT ε σ m α) : m (Option α) :=
|
||||
EResult.result? <$> x init
|
||||
|
||||
@[inline] def catchExceptions {ε σ α : Type u}
|
||||
[Monad m] (x : EStateT ε σ m α) (h : ε → StateT σ m α)
|
||||
: StateT σ m α := fun s => do
|
||||
match (← x s) with
|
||||
| .ok a s => return (a, s)
|
||||
| .error e s => h e s
|
||||
|
||||
/-- Lift the `m` monad into the `EStateT ε σ m` monad transformer. -/
|
||||
@[always_inline, inline]
|
||||
protected def lift {ε σ α : Type u} [Monad m] (x : m α) : EStateT ε σ m α := fun s => do
|
||||
let a ← x; pure (.ok a s)
|
||||
|
||||
@[inline] def toStateT {ε σ α : Type u} [Monad m] (x : EStateT ε σ m α) : StateT σ m (Except ε α) := fun s => do
|
||||
match (← x s) with
|
||||
| .ok a s => return (.ok a, s)
|
||||
| .error e s => return (.error e, s)
|
||||
|
||||
@[inline] def toStateT? {ε σ α : Type u} [Monad m] (x : EStateT ε σ m α) : StateT σ m (Option α) := do
|
||||
(·.toOption) <$> x.toStateT
|
||||
|
||||
instance [Monad m] : MonadLift m (EStateT ε σ m) := ⟨EStateT.lift⟩
|
||||
|
||||
variable {ε ε' : Type u} {σ : Type v} {α β : Type w}
|
||||
|
||||
/-- Execute an `EStateT` on initial state `s` to get an `EResult` result. -/
|
||||
@[always_inline, inline]
|
||||
def run (init : σ) (self : EStateT ε σ m α) : m (EResult ε σ α) :=
|
||||
self init
|
||||
|
||||
/-- Execute an `EStateT` on initial state `s` to get an `Except` result. -/
|
||||
@[always_inline, inline]
|
||||
def run' {σ : Type max u w} [Functor m] (init : σ) (x : EStateT ε σ m α) : m (Except ε α) :=
|
||||
EResult.toExcept <$> x init
|
||||
instance {ε σ : Type u} [Monad m] : MonadLift m (EStateT ε σ m) := ⟨EStateT.lift⟩
|
||||
|
||||
/-- The `pure` operation of the `EStateT` monad transformer. -/
|
||||
@[always_inline, inline]
|
||||
|
|
|
|||
|
|
@ -25,6 +25,46 @@ instance : Max Verbosity := maxOfLe
|
|||
|
||||
instance : Inhabited Verbosity := ⟨.normal⟩
|
||||
|
||||
/-- Whether to ANSI escape codes. -/
|
||||
inductive AnsiMode
|
||||
/--
|
||||
Automatically determine whether to use ANSI escape codes
|
||||
based on whether the stream written to is a terminal.
|
||||
-/
|
||||
| auto
|
||||
/-- Use ANSI escape codes. -/
|
||||
| ansi
|
||||
/-- Do not use ANSI escape codes. -/
|
||||
| noAnsi
|
||||
|
||||
/-- Returns whether to ANSI escape codes with the stream `out`. -/
|
||||
def AnsiMode.isEnabled (out : IO.FS.Stream) : AnsiMode → BaseIO Bool
|
||||
| .auto => out.isTty
|
||||
| .ansi => pure true
|
||||
| .noAnsi => pure false
|
||||
|
||||
/--
|
||||
Wrap text in ANSI escape sequences to make it bold and color it the ANSI `colorCode`.
|
||||
Resets all terminal font attributes at the end of the text.
|
||||
-/
|
||||
def Ansi.chalk (colorCode text : String) : String :=
|
||||
s!"\x1B[1;{colorCode}m{text}\x1B[m"
|
||||
|
||||
/-- A pure representation of output stream. -/
|
||||
inductive OutStream
|
||||
| stdout
|
||||
| stderr
|
||||
| stream (s : IO.FS.Stream)
|
||||
|
||||
/-- Returns the real output stream associated with `OutStream`. -/
|
||||
def OutStream.get : OutStream → BaseIO IO.FS.Stream
|
||||
| .stdout => IO.getStdout
|
||||
| .stderr => IO.getStderr
|
||||
| .stream s => pure s
|
||||
|
||||
instance : Coe IO.FS.Stream OutStream := ⟨.stream⟩
|
||||
instance : Coe IO.FS.Handle OutStream := ⟨fun h => .stream (.ofHandle h)⟩
|
||||
|
||||
inductive LogLevel
|
||||
| trace
|
||||
| info
|
||||
|
|
@ -37,6 +77,18 @@ instance : LE LogLevel := leOfOrd
|
|||
instance : Min LogLevel := minOfLe
|
||||
instance : Max LogLevel := maxOfLe
|
||||
|
||||
/-- Unicode icon for representing the log level. -/
|
||||
def LogLevel.icon : LogLevel → Char
|
||||
| .trace | .info => 'ℹ'
|
||||
| .warning => '⚠'
|
||||
| .error => '✖'
|
||||
|
||||
/-- ANSI escape code for coloring text of at the log level. -/
|
||||
def LogLevel.ansiColor : LogLevel → String
|
||||
| .trace | .info => "34"
|
||||
| .warning => "33"
|
||||
| .error => "31"
|
||||
|
||||
protected def LogLevel.toString : LogLevel → String
|
||||
| .trace => "trace"
|
||||
| .info => "info"
|
||||
|
|
@ -50,19 +102,23 @@ protected def LogLevel.ofMessageSeverity : MessageSeverity → LogLevel
|
|||
|
||||
instance : ToString LogLevel := ⟨LogLevel.toString⟩
|
||||
|
||||
def LogLevel.visibleAtVerbosity (self : LogLevel) (verbosity : Verbosity) : Bool :=
|
||||
match self with
|
||||
| .trace => verbosity == .verbose
|
||||
| .info => verbosity != .quiet
|
||||
| _ => true
|
||||
def Verbosity.minLogLv : Verbosity → LogLevel
|
||||
| .quiet => .warning
|
||||
| .normal => .info
|
||||
| .verbose => .trace
|
||||
|
||||
structure LogEntry where
|
||||
level : LogLevel
|
||||
message : String
|
||||
deriving Inhabited, ToJson, FromJson
|
||||
|
||||
protected def LogEntry.toString (self : LogEntry) : String :=
|
||||
s!"{self.level}: {self.message.trim}"
|
||||
protected def LogEntry.toString (self : LogEntry) (useAnsi := false) : String :=
|
||||
if useAnsi then
|
||||
let {level := lv, message := msg} := self
|
||||
let pre := Ansi.chalk lv.ansiColor s!"{lv.toString}:"
|
||||
s!"{pre} {msg.trim}"
|
||||
else
|
||||
s!"{self.level}: {self.message.trim}"
|
||||
|
||||
instance : ToString LogEntry := ⟨LogEntry.toString⟩
|
||||
|
||||
|
|
@ -83,75 +139,99 @@ export MonadLog (logEntry)
|
|||
@[inline] def logError [MonadLog m] (message : String) : m PUnit :=
|
||||
logEntry {level := .error, message}
|
||||
|
||||
def logToIO (e : LogEntry) (verbosity : Verbosity) : BaseIO PUnit := do
|
||||
match e.level with
|
||||
| .trace => if verbosity == .verbose then
|
||||
IO.println e.message.trim |>.catchExceptions fun _ => pure ()
|
||||
| .info => if verbosity != .quiet then
|
||||
IO.println e.message.trim |>.catchExceptions fun _ => pure ()
|
||||
| .warning => IO.eprintln s!"warning: {e.message.trim}" |>.catchExceptions fun _ => pure ()
|
||||
| .error => IO.eprintln s!"error: {e.message.trim}" |>.catchExceptions fun _ => pure ()
|
||||
|
||||
def logToStream (e : LogEntry) (h : IO.FS.Stream) (verbosity : Verbosity) : BaseIO PUnit := do
|
||||
match e.level with
|
||||
| .trace => if verbosity == .verbose then
|
||||
h.putStrLn s!"trace: {e.message.trim}" |>.catchExceptions fun _ => pure ()
|
||||
| .info => if verbosity != .quiet then
|
||||
h.putStrLn s!"info: {e.message.trim}" |>.catchExceptions fun _ => pure ()
|
||||
| .warning => h.putStrLn s!"warning: {e.message.trim}" |>.catchExceptions fun _ => pure ()
|
||||
| .error => h.putStrLn s!"error: {e.message.trim}" |>.catchExceptions fun _ => pure ()
|
||||
|
||||
@[specialize] def logSerialMessage (msg : SerialMessage) [MonadLog m] : m PUnit :=
|
||||
let str := msg.data
|
||||
let str := if msg.caption.trim.isEmpty then
|
||||
str.trim else s!"{msg.caption.trim}:\n{str.trim}"
|
||||
msg.data.trim else s!"{msg.caption.trim}:\n{msg.data.trim}"
|
||||
logEntry {
|
||||
level := .ofMessageSeverity msg.severity
|
||||
message := mkErrorStringWithPos msg.fileName msg.pos str msg.endPos
|
||||
message := mkErrorStringWithPos msg.fileName msg.pos str none
|
||||
}
|
||||
|
||||
@[deprecated] def logToIO (e : LogEntry) (minLv : LogLevel) : BaseIO PUnit := do
|
||||
match e.level with
|
||||
| .trace => if minLv ≥ .trace then
|
||||
IO.println e.message.trim |>.catchExceptions fun _ => pure ()
|
||||
| .info => if minLv ≥ .info then
|
||||
IO.println e.message.trim |>.catchExceptions fun _ => pure ()
|
||||
| .warning => IO.eprintln e.toString |>.catchExceptions fun _ => pure ()
|
||||
| .error => IO.eprintln e.toString |>.catchExceptions fun _ => pure ()
|
||||
|
||||
def logToStream
|
||||
(e : LogEntry) (out : IO.FS.Stream) (minLv : LogLevel) (useAnsi : Bool)
|
||||
: BaseIO PUnit := do
|
||||
if e.level ≥ minLv then
|
||||
out.putStrLn (e.toString useAnsi) |>.catchExceptions fun _ => pure ()
|
||||
|
||||
namespace MonadLog
|
||||
|
||||
@[specialize] def nop [Pure m] : MonadLog m :=
|
||||
⟨fun _ => pure ()⟩
|
||||
abbrev nop [Pure m] : MonadLog m where
|
||||
logEntry _ := pure ()
|
||||
|
||||
instance [Pure m] : Inhabited (MonadLog m) := ⟨MonadLog.nop⟩
|
||||
|
||||
@[specialize] def io [MonadLiftT BaseIO m] (verbosity := Verbosity.normal) : MonadLog m where
|
||||
logEntry e := logToIO e verbosity
|
||||
|
||||
@[inline] def stream [MonadLiftT BaseIO m] (h : IO.FS.Stream) (verbosity := Verbosity.normal) : MonadLog m where
|
||||
logEntry e := logToStream e h verbosity
|
||||
|
||||
@[inline] def stdout [MonadLiftT BaseIO m] (verbosity := Verbosity.normal) : MonadLog m where
|
||||
logEntry e := liftM (m := BaseIO) do logToStream e (← IO.getStdout) verbosity
|
||||
|
||||
@[inline] def stderr [MonadLiftT BaseIO m] (verbosity := Verbosity.normal) : MonadLog m where
|
||||
logEntry e := liftM (m := BaseIO) do logToStream e (← IO.getStderr) verbosity
|
||||
|
||||
@[inline] def lift [MonadLiftT m n] (self : MonadLog m) : MonadLog n where
|
||||
abbrev lift [MonadLiftT m n] (self : MonadLog m) : MonadLog n where
|
||||
logEntry e := liftM <| self.logEntry e
|
||||
|
||||
instance [MonadLift m n] [methods : MonadLog m] : MonadLog n := lift methods
|
||||
instance [MonadLift m n] [methods : MonadLog m] : MonadLog n := methods.lift
|
||||
|
||||
set_option linter.deprecated false in
|
||||
@[deprecated] abbrev io [MonadLiftT BaseIO m] (minLv := LogLevel.info) : MonadLog m where
|
||||
logEntry e := logToIO e minLv
|
||||
|
||||
abbrev stream [MonadLiftT BaseIO m]
|
||||
(out : IO.FS.Stream) (minLv := LogLevel.info) (useAnsi := false)
|
||||
: MonadLog m where logEntry e := logToStream e out minLv useAnsi
|
||||
|
||||
end MonadLog
|
||||
|
||||
def OutStream.logEntry
|
||||
(self : OutStream) (e : LogEntry)
|
||||
(minLv : LogLevel := .info) (ansiMode := AnsiMode.auto)
|
||||
: BaseIO PUnit := do
|
||||
let out ← self.get
|
||||
let useAnsi ← ansiMode.isEnabled out
|
||||
logToStream e out minLv useAnsi
|
||||
|
||||
abbrev OutStream.logger [MonadLiftT BaseIO m]
|
||||
(out : OutStream) (minLv := LogLevel.info) (ansiMode := AnsiMode.auto)
|
||||
: MonadLog m where logEntry e := out.logEntry e minLv ansiMode
|
||||
|
||||
abbrev MonadLog.stdout
|
||||
[MonadLiftT BaseIO m] (minLv := LogLevel.info) (ansiMode := AnsiMode.auto)
|
||||
: MonadLog m := OutStream.stdout.logger minLv ansiMode
|
||||
|
||||
abbrev MonadLog.stderr
|
||||
[MonadLiftT BaseIO m] (minLv := LogLevel.info) (ansiMode := AnsiMode.auto)
|
||||
: MonadLog m := OutStream.stderr.logger minLv ansiMode
|
||||
|
||||
@[inline] def OutStream.getLogger [MonadLiftT BaseIO m]
|
||||
(out : OutStream) (minLv := LogLevel.info) (ansiMode := AnsiMode.auto)
|
||||
: BaseIO (MonadLog m) := do
|
||||
let out ← out.get
|
||||
let useAnsi ← ansiMode.isEnabled out
|
||||
return .stream out minLv useAnsi
|
||||
|
||||
/-- A monad equipped with a `MonadLog` instance -/
|
||||
abbrev MonadLogT (m : Type u → Type v) (n : Type v → Type w) :=
|
||||
ReaderT (MonadLog m) n
|
||||
|
||||
namespace MonadLogT
|
||||
|
||||
instance [Pure n] [Inhabited α] : Inhabited (MonadLogT m n α) :=
|
||||
⟨fun _ => pure Inhabited.default⟩
|
||||
|
||||
instance [Monad n] [MonadLiftT m n] : MonadLog (MonadLogT m n) where
|
||||
logEntry e := do (← read).logEntry e
|
||||
|
||||
@[inline] def MonadLogT.adaptMethods [Monad n]
|
||||
@[inline] def adaptMethods [Monad n]
|
||||
(f : MonadLog m → MonadLog m') (self : MonadLogT m' n α) : MonadLogT m n α :=
|
||||
ReaderT.adapt f self
|
||||
|
||||
@[inline] def MonadLogT.ignoreLog [Pure m] (self : MonadLogT m n α) : n α :=
|
||||
@[inline] def ignoreLog [Pure m] (self : MonadLogT m n α) : n α :=
|
||||
self MonadLog.nop
|
||||
|
||||
end MonadLogT
|
||||
|
||||
/- A Lake log. An `Array` of log entries. -/
|
||||
structure Log where
|
||||
entries : Array LogEntry
|
||||
|
|
@ -172,12 +252,15 @@ namespace Log
|
|||
|
||||
instance : EmptyCollection Log := ⟨Log.empty⟩
|
||||
|
||||
@[inline] def isEmpty (log : Log) : Bool :=
|
||||
log.entries.isEmpty
|
||||
|
||||
@[inline] def size (log : Log) : Nat :=
|
||||
log.entries.size
|
||||
|
||||
@[inline] def isEmpty (log : Log) : Bool :=
|
||||
log.size = 0
|
||||
|
||||
@[inline] def hasEntries (log : Log) : Bool :=
|
||||
log.size ≠ 0
|
||||
|
||||
@[inline] def endPos (log : Log) : Log.Pos :=
|
||||
⟨log.entries.size⟩
|
||||
|
||||
|
|
@ -220,17 +303,22 @@ instance : ToString Log := ⟨Log.toString⟩
|
|||
@[inline] def filter (f : LogEntry → Bool) (log : Log) : Log :=
|
||||
.mk <| log.entries.filter f
|
||||
|
||||
def filterByVerbosity (log : Log) (verbosity := Verbosity.normal) : Log :=
|
||||
log.filter (·.level.visibleAtVerbosity verbosity)
|
||||
|
||||
@[inline] def any (f : LogEntry → Bool) (log : Log) : Bool :=
|
||||
log.entries.any f
|
||||
|
||||
def hasVisibleEntries (log : Log) (verbosity := Verbosity.normal) : Bool :=
|
||||
log.any (·.level.visibleAtVerbosity verbosity)
|
||||
/-- The max log level of entries in this log. If empty, returns `trace`. -/
|
||||
def maxLv (log : Log) : LogLevel :=
|
||||
log.entries.foldl (max · ·.level) .trace
|
||||
|
||||
end Log
|
||||
|
||||
/-- Add a `LogEntry` to the end of the monad's `Log`. -/
|
||||
@[inline] def pushLogEntry
|
||||
[MonadStateOf Log m] (e : LogEntry)
|
||||
: m PUnit := modify (·.push e)
|
||||
|
||||
abbrev MonadLog.ofMonadState [MonadStateOf Log m] : MonadLog m := ⟨pushLogEntry⟩
|
||||
|
||||
/-- Returns the monad's log. -/
|
||||
@[inline] def getLog [MonadStateOf Log m] : m Log :=
|
||||
get
|
||||
|
|
@ -239,6 +327,18 @@ end Log
|
|||
@[inline] def getLogPos [Functor m] [MonadStateOf Log m] : m Log.Pos :=
|
||||
(·.endPos) <$> getLog
|
||||
|
||||
/-- Removes the section monad's log starting and returns it. -/
|
||||
@[inline] def takeLog [MonadStateOf Log m] : m Log :=
|
||||
modifyGet fun log => (log, {})
|
||||
|
||||
/--
|
||||
Removes the monad's log starting at `pos` and returns it.
|
||||
Useful for extracting logged errors after catching an error position
|
||||
from an `ELogT` (e.g., `LogIO`).
|
||||
-/
|
||||
@[inline] def takeLogFrom [MonadStateOf Log m] (pos : Log.Pos) : m Log :=
|
||||
modifyGet fun log => (log.takeFrom pos, log.dropFrom pos)
|
||||
|
||||
/--
|
||||
Backtracks the monad's log to `pos`.
|
||||
Useful for discarding logged errors after catching an error position
|
||||
|
|
@ -247,14 +347,6 @@ from an `ELogT` (e.g., `LogIO`).
|
|||
@[inline] def dropLogFrom [MonadStateOf Log m] (pos : Log.Pos) : m PUnit :=
|
||||
modify (·.dropFrom pos)
|
||||
|
||||
/--
|
||||
Removes the section monad's log starting at `pos` and returns it.
|
||||
Useful for extracting logged errors after catching an error position
|
||||
from an `ELogT` (e.g., `LogIO`).
|
||||
-/
|
||||
@[inline] def takeLogFrom [MonadStateOf Log m] (pos : Log.Pos) : m Log :=
|
||||
modifyGet fun log => (log.takeFrom pos, log.dropFrom pos)
|
||||
|
||||
/-- Returns the log from `x` while leaving it intact in the monad. -/
|
||||
@[inline] def extractLog [Monad m] [MonadStateOf Log m] (x : m PUnit) : m Log := do
|
||||
let iniPos ← getLogPos
|
||||
|
|
@ -284,17 +376,75 @@ from an `ELogT` (e.g., `LogIO`).
|
|||
try self catch _ => pure ()
|
||||
throw iniPos
|
||||
|
||||
/-- Captures IO in `x` into an informational log entry. -/
|
||||
@[inline] def withLoggedIO
|
||||
[Monad m] [MonadLiftT BaseIO m] [MonadLog m] [MonadFinally m] (x : m α)
|
||||
: m α := do
|
||||
let (out, a) ← IO.FS.withIsolatedStreams x
|
||||
unless out.isEmpty do logInfo s!"stdout/stderr:\n{out}"
|
||||
return a
|
||||
|
||||
/-- Throw with the logged error `message`. -/
|
||||
@[inline] protected def ELog.error
|
||||
[Monad m] [MonadLog m] [MonadStateOf Log m] [MonadExceptOf Log.Pos m]
|
||||
(msg : String)
|
||||
: m α := errorWithLog (logError msg)
|
||||
|
||||
/-- `Alternative` instance for monads with `Log` state and `Log.Pos` errors. -/
|
||||
abbrev ELog.monadError
|
||||
[Monad m] [MonadLog m] [MonadStateOf Log m] [MonadExceptOf Log.Pos m]
|
||||
: MonadError m := ⟨ELog.error⟩
|
||||
|
||||
/-- Fail without logging anything. -/
|
||||
@[inline] protected def ELog.failure
|
||||
[Monad m] [MonadStateOf Log m] [MonadExceptOf Log.Pos m]
|
||||
: m α := do throw (← getLogPos)
|
||||
|
||||
/-- Performs `x`. If it fails, drop its log and perform `y`. -/
|
||||
@[inline] protected def ELog.orElse
|
||||
[Monad m] [MonadStateOf Log m] [MonadExceptOf Log.Pos m]
|
||||
(x : m α) (y : Unit → m α)
|
||||
: m α := try x catch errPos => dropLogFrom errPos; y ()
|
||||
|
||||
/-- `Alternative` instance for monads with `Log` state and `Log.Pos` errors. -/
|
||||
abbrev ELog.alternative
|
||||
[Monad m] [MonadStateOf Log m] [MonadExceptOf Log.Pos m]
|
||||
: Alternative m where
|
||||
failure := ELog.failure
|
||||
orElse := ELog.orElse
|
||||
|
||||
/-- A monad equipped with a log. -/
|
||||
abbrev LogT (m : Type → Type) :=
|
||||
StateT Log m
|
||||
|
||||
instance [Monad m] : MonadLog (LogT m) := .ofMonadState
|
||||
|
||||
namespace LogT
|
||||
|
||||
@[inline] protected def log [Monad m] (e : LogEntry) : LogT m PUnit :=
|
||||
modify (·.push e)
|
||||
abbrev run [Functor m] (self : LogT m α) (log : Log := {}) : m (α × Log) :=
|
||||
StateT.run self log
|
||||
|
||||
instance [Monad m] : MonadLog (LogT m) := ⟨LogT.log⟩
|
||||
abbrev run' [Functor m] (self : LogT m α) (log : Log := {}) : m α :=
|
||||
StateT.run' self log
|
||||
|
||||
/--
|
||||
Run `self` with the log taken from the state of the monad `n`.
|
||||
|
||||
**Warning:** If lifting `self` from `m` to `n` fails, the log will be lost.
|
||||
Thus, this is best used when the lift cannot fail.
|
||||
-/
|
||||
@[inline] def takeAndRun
|
||||
[Monad n] [MonadStateOf Log n] [MonadLiftT m n] [MonadFinally n]
|
||||
(self : LogT m α)
|
||||
: n α := do
|
||||
let (a, log) ← self (← takeLog)
|
||||
set log
|
||||
return a
|
||||
|
||||
/--
|
||||
Runs `self` in `n` and then replays the entries of the resulting log
|
||||
using the new monad's `logger`.
|
||||
-/
|
||||
@[inline] def replayLog [Monad n] [logger : MonadLog n] [MonadLiftT m n] (self : LogT m α) : n α := do
|
||||
let (a, log) ← self {}
|
||||
log.replay (logger := logger)
|
||||
|
|
@ -308,29 +458,49 @@ abbrev ELogT (m : Type → Type) :=
|
|||
|
||||
abbrev ELogResult (α) := EResult Log.Pos Log α
|
||||
|
||||
instance [Monad m] : MonadLog (ELogT m) := .ofMonadState
|
||||
instance [Monad m] : MonadError (ELogT m) := ELog.monadError
|
||||
instance [Monad m] : Alternative (ELogT m) := ELog.alternative
|
||||
|
||||
namespace ELogT
|
||||
|
||||
@[inline] protected def log [Monad m] (e : LogEntry) : ELogT m PUnit :=
|
||||
modify (·.push e)
|
||||
abbrev run (self : ELogT m α) (log : Log := {}) : m (ELogResult α) :=
|
||||
EStateT.run log self
|
||||
|
||||
instance [Monad m] : MonadLog (ELogT m) := ⟨ELogT.log⟩
|
||||
abbrev run' [Functor m] (self : ELogT m α) (log : Log := {}) : m (Except Log.Pos α) :=
|
||||
EStateT.run' log self
|
||||
|
||||
@[inline] protected def error [Monad m] (msg : String) : ELogT m α :=
|
||||
errorWithLog (logError msg)
|
||||
abbrev toLogT [Functor m] (self : ELogT m α) : LogT m (Except Log.Pos α) :=
|
||||
self.toStateT
|
||||
|
||||
instance [Monad m] : MonadError (ELogT m) := ⟨ELogT.error⟩
|
||||
abbrev toLogT? [Functor m] (self : ELogT m α) : LogT m (Option α) :=
|
||||
self.toStateT?
|
||||
|
||||
/-- Fail without logging anything. -/
|
||||
@[inline] protected def ELogT.failure [Monad m] : ELogT m α := do
|
||||
throw (← getLogPos)
|
||||
abbrev run? [Functor m] (self : ELogT m α) (log : Log := {}) : m (Option α × Log) :=
|
||||
EStateT.run? log self
|
||||
|
||||
/-- Performs `x`. If it fails, drop its log and perform `y`. -/
|
||||
@[inline] protected def ELogT.orElse [Monad m] (x : ELogT m α) (y : Unit → ELogT m α) : ELogT m α :=
|
||||
try x catch errPos => dropLogFrom errPos; y ()
|
||||
abbrev run?' [Functor m] (self : ELogT m α) (log : Log := {}) : m (Option α) :=
|
||||
EStateT.run?' log self
|
||||
|
||||
instance [Monad m] : Alternative (ELogT m) where
|
||||
failure := ELogT.failure
|
||||
orElse := ELogT.orElse
|
||||
@[inline] def catchLog [Monad m] (f : Log → LogT m α) (self : ELogT m α) : LogT m α := do
|
||||
self.catchExceptions fun errPos => do f (← takeLogFrom errPos)
|
||||
|
||||
@[deprecated run?] abbrev captureLog := @run?
|
||||
|
||||
/--
|
||||
Run `self` with the log taken from the state of the monad `n`,
|
||||
|
||||
**Warning:** If lifting `self` from `m` to `n` fails, the log will be lost.
|
||||
Thus, this is best used when the lift cannot fail. Note excludes the
|
||||
native log position failure of `ELogT`, which are lifted safely.
|
||||
-/
|
||||
@[inline] def takeAndRun
|
||||
[Monad n] [MonadStateOf Log n] [MonadExceptOf Log.Pos n] [MonadLiftT m n]
|
||||
(self : ELogT m α)
|
||||
: n α := do
|
||||
match (← self (← takeLog)) with
|
||||
| .ok a log => set log; return a
|
||||
| .error e log => set log; throw e
|
||||
|
||||
/--
|
||||
Runs `self` in `n` and then replays the entries of the resulting log
|
||||
|
|
@ -352,36 +522,24 @@ a `failure` in the new monad.
|
|||
| .ok a log => log.replay (logger := logger) *> pure a
|
||||
| .error _ log => log.replay (logger := logger) *> failure
|
||||
|
||||
@[inline] def catchFailure [Monad m] (f : Log → LogT m α) (self : ELogT m α) : LogT m α := fun log => do
|
||||
match (← self log) with
|
||||
| .error n log => let (h,t) := log.split n; f h t
|
||||
| .ok a log => return (a, log)
|
||||
|
||||
@[inline] def captureLog [Monad m] (self : ELogT m α) : m (Option α × Log) := do
|
||||
match (← self {}) with
|
||||
| .ok a log => return (some a, log)
|
||||
| .error _ log => return (none, log)
|
||||
|
||||
end ELogT
|
||||
|
||||
/-- A monad equipped with a log, a log error position, and the ability to perform I/O. -/
|
||||
abbrev LogIO := ELogT BaseIO
|
||||
|
||||
instance : MonadLift IO LogIO := ⟨MonadError.runIO⟩
|
||||
|
||||
namespace LogIO
|
||||
|
||||
@[deprecated ELogT.run?] abbrev captureLog := @ELogT.run?
|
||||
|
||||
/--
|
||||
Runs a `LogIO` action in `BaseIO`.
|
||||
Prints logs message at `verbosity` to stderr or stdout (if `useStdout`).
|
||||
Prints log entries of at least `minLv` to `out`.
|
||||
-/
|
||||
@[inline] def LogIO.toBaseIO
|
||||
(x : LogIO α) (verbosity := Verbosity.normal) (useStdout := false)
|
||||
: BaseIO (Option α) :=
|
||||
let logger := if useStdout then .stdout verbosity else .stderr verbosity
|
||||
x.replayLog? (logger := logger)
|
||||
@[inline] def toBaseIO (self : LogIO α)
|
||||
(minLv := LogLevel.info) (ansiMode := AnsiMode.auto) (out := OutStream.stderr)
|
||||
: BaseIO (Option α) := do
|
||||
self.replayLog? (logger := ← out.getLogger minLv ansiMode)
|
||||
|
||||
/-- Captures IO in `x` into an informational log entry. -/
|
||||
@[inline] def withLoggedIO
|
||||
[Monad m] [MonadLiftT BaseIO m] [MonadLog m] [MonadFinally m] (x : m α)
|
||||
: m α := do
|
||||
let (out, a) ← IO.FS.withIsolatedStreams x
|
||||
unless out.isEmpty do logInfo s!"stdout/stderr:\n{out}"
|
||||
return a
|
||||
end LogIO
|
||||
|
|
|
|||
|
|
@ -66,7 +66,7 @@ instance : Alternative MainM where
|
|||
|
||||
/-! # Logging and IO -/
|
||||
|
||||
instance : MonadLog MainM := MonadLog.stderr
|
||||
instance : MonadLog MainM := .stderr
|
||||
|
||||
/-- Print out a error line with the given message and then exit with an error code. -/
|
||||
@[inline] protected def error (msg : String) (rc : ExitCode := 1) : MainM α := do
|
||||
|
|
@ -76,7 +76,9 @@ instance : MonadLog MainM := MonadLog.stderr
|
|||
instance : MonadError MainM := ⟨MainM.error⟩
|
||||
instance : MonadLift IO MainM := ⟨MonadError.runIO⟩
|
||||
|
||||
@[inline] def runLogIO (x : LogIO α) (verbosity := Verbosity.normal) : MainM α :=
|
||||
x.replayLog (logger := MonadLog.stderr verbosity)
|
||||
@[inline] def runLogIO (x : LogIO α)
|
||||
(minLv := LogLevel.info) (ansiMode := AnsiMode.auto) (out := OutStream.stderr)
|
||||
: MainM α := do
|
||||
x.replayLog (logger := ← out.getLogger minLv ansiMode)
|
||||
|
||||
instance : MonadLift LogIO MainM := ⟨runLogIO⟩
|
||||
|
|
|
|||
|
|
@ -23,25 +23,25 @@ fi
|
|||
$LAKE build targets:noexistent && exit 1 || true
|
||||
|
||||
# Test custom targets and package, library, and module facets
|
||||
$LAKE build bark | awk '/Building/,/Bark!/' | diff -u --strip-trailing-cr <(cat << 'EOF'
|
||||
[1/1] Building targets/bark
|
||||
$LAKE build bark | awk '/Ran/,/Bark!/' | diff -u --strip-trailing-cr <(cat << 'EOF'
|
||||
ℹ [1/1] Ran targets/bark
|
||||
info: Bark!
|
||||
EOF
|
||||
) -
|
||||
$LAKE build targets/bark_bark | awk '/Building/,/bark_bark/' | diff -u --strip-trailing-cr <(cat << 'EOF'
|
||||
[1/2] Building targets/bark
|
||||
$LAKE build targets/bark_bark | awk '/Ran/,0' | diff -u --strip-trailing-cr <(cat << 'EOF'
|
||||
ℹ [1/2] Ran targets/bark
|
||||
info: Bark!
|
||||
[2/2] Building targets/bark_bark
|
||||
Build completed successfully.
|
||||
EOF
|
||||
) -
|
||||
$LAKE build targets:print_name | awk '/Building/,0' | diff -u --strip-trailing-cr <(cat << 'EOF'
|
||||
[1/1] Building targets:print_name
|
||||
$LAKE build targets:print_name | awk '/Ran/,/^targets/' | diff -u --strip-trailing-cr <(cat << 'EOF'
|
||||
ℹ [1/1] Ran targets:print_name
|
||||
info: stdout/stderr:
|
||||
targets
|
||||
EOF
|
||||
) -
|
||||
$LAKE build Foo:print_name | awk '/Building/,0' | diff -u --strip-trailing-cr <(cat << 'EOF'
|
||||
[1/1] Building Foo:print_name
|
||||
$LAKE build Foo:print_name | awk '/Ran/,/^Foo/' | diff -u --strip-trailing-cr <(cat << 'EOF'
|
||||
ℹ [1/1] Ran targets/Foo:print_name
|
||||
info: stdout/stderr:
|
||||
Foo
|
||||
EOF
|
||||
|
|
|
|||
1
src/lake/tests/noRelease/clean.sh
Executable file
1
src/lake/tests/noRelease/clean.sh
Executable file
|
|
@ -0,0 +1 @@
|
|||
rm -rf .lake lake-manifest.json
|
||||
6
src/lake/tests/noRelease/dep/lakefile.lean
Normal file
6
src/lake/tests/noRelease/dep/lakefile.lean
Normal file
|
|
@ -0,0 +1,6 @@
|
|||
import Lake
|
||||
open Lake DSL
|
||||
|
||||
package dep where
|
||||
preferReleaseBuild := true
|
||||
releaseRepo := "https://example.com"
|
||||
5
src/lake/tests/noRelease/lakefile.lean
Normal file
5
src/lake/tests/noRelease/lakefile.lean
Normal file
|
|
@ -0,0 +1,5 @@
|
|||
import Lake
|
||||
open Lake DSL
|
||||
|
||||
package test
|
||||
require dep from "dep"
|
||||
29
src/lake/tests/noRelease/test.sh
Executable file
29
src/lake/tests/noRelease/test.sh
Executable file
|
|
@ -0,0 +1,29 @@
|
|||
#!/usr/bin/env bash
|
||||
set -euxo pipefail
|
||||
|
||||
LAKE=${LAKE:-../../.lake/build/bin/lake}
|
||||
|
||||
./clean.sh
|
||||
|
||||
# ---
|
||||
# Test Lake's behavior when failing to fetch a cloud release
|
||||
# ---
|
||||
|
||||
# Test that a direct invocation fo `lake build *:release` fails
|
||||
($LAKE build dep:release && exit 1 || true) | diff -u --strip-trailing-cr <(cat << 'EOF'
|
||||
✖ [1/1] Fetching dep:release
|
||||
info: dep: wanted prebuilt release, but could not find an associated tag for the package's revision
|
||||
error: failed to fetch cloud release
|
||||
Some builds logged failures:
|
||||
- dep:release
|
||||
EOF
|
||||
) -
|
||||
|
||||
# Test that an indirect fetch on the release does not cause the build to fail
|
||||
$LAKE build -v test:extraDep | diff -u --strip-trailing-cr <(cat << 'EOF'
|
||||
⚠ [1/1] Fetched test:extraDep
|
||||
info: dep: wanted prebuilt release, but could not find an associated tag for the package's revision
|
||||
warning: failed to fetch cloud release; falling back to local build
|
||||
Build completed successfully.
|
||||
EOF
|
||||
) -
|
||||
|
|
@ -1,6 +0,0 @@
|
|||
Building Hello
|
||||
Compiling Hello
|
||||
Linking hello
|
||||
Building Hello
|
||||
Compiling Hello
|
||||
Linking hello
|
||||
|
|
@ -5,23 +5,42 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
|
|||
|
||||
./clean.sh
|
||||
|
||||
# Tests the `--old` option for using outdate oleans
|
||||
# See https://github.com/leanprover/lake/issues/44
|
||||
# Test the `--old` option for using outdate oleans
|
||||
# https://github.com/leanprover/lake/issues/44
|
||||
# https://github.com/leanprover/lean4/issues/2822
|
||||
|
||||
diff_out() {
|
||||
grep 'Built' || true |
|
||||
sed 's/^.*\[.*\] //' |
|
||||
sed 's/\s*(.*)$//' |
|
||||
LANG=POSIX sort |
|
||||
diff -u --strip-trailing-cr "$1" -
|
||||
}
|
||||
|
||||
$LAKE new hello
|
||||
$LAKE -d hello build
|
||||
sleep 0.5 # for some reason, delay needed for `--old` rebuild consistency
|
||||
echo 'def hello := "old"' > hello/Hello.lean
|
||||
$LAKE -d hello build --old | sed 's/\[.*\] //' | tee produced.out
|
||||
echo 'def hello := "normal"' > hello/Hello.lean
|
||||
$LAKE -d hello build | sed 's/\[.*\] //' | tee -a produced.out
|
||||
sleep 1 # sleep needed to guarantee modification time difference
|
||||
|
||||
grep -i main produced.out
|
||||
grep -i hello produced.out > produced.out.tmp
|
||||
mv produced.out.tmp produced.out
|
||||
if [ "$OS" = Windows_NT ]; then
|
||||
sed -i 's/.exe//g' produced.out
|
||||
diff --strip-trailing-cr expected.out produced.out
|
||||
else
|
||||
diff expected.out produced.out
|
||||
fi
|
||||
# Test basic `--old`
|
||||
echo 'def hello := "old"' > hello/Hello/Basic.lean
|
||||
$LAKE -d hello build --old | diff_out <(cat << 'EOF'
|
||||
Built Hello.Basic
|
||||
Built Hello.Basic:c
|
||||
Built hello
|
||||
EOF
|
||||
)
|
||||
|
||||
# Test a normal build works after an `--old` build
|
||||
echo 'def hello := "normal"' > hello/Hello/Basic.lean
|
||||
$LAKE -d hello build | diff_out <(cat << 'EOF'
|
||||
Built Hello
|
||||
Built Hello.Basic
|
||||
Built Hello.Basic:c
|
||||
Built Main
|
||||
Built hello
|
||||
EOF
|
||||
)
|
||||
|
||||
# Test that `--old` does not rebuild touched but unchanged files (lean4#2822)
|
||||
touch hello/Hello/Basic.lean
|
||||
$LAKE -d hello build --old | diff_out /dev/null
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
error: ././././TestExtern.lean:5:0-5:27: native implementation did not agree with reference implementation!
|
||||
error: ././././TestExtern.lean:5:0: native implementation did not agree with reference implementation!
|
||||
Compare the outputs of:
|
||||
#eval Nat.not_add 4 5
|
||||
and
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue