Skip to content

Commit 6a60de2

Browse files
committed
fix: lake: source file not in module input trace & some logs dropped (#9101)
This PR fixes a bug introduce by #9081 where the source file was dropped from the module input trace and some entries were dropped from the module job log. (cherry picked from commit 9db41f9)
1 parent 7de2ded commit 6a60de2

File tree

1 file changed

+9
-3
lines changed

1 file changed

+9
-3
lines changed

src/lake/Lake/Build/Module.lean

Lines changed: 9 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -375,13 +375,19 @@ Fetch its dependencies and then elaborate the Lean source file, producing
375375
all possible artifacts (e.g., `.olean`, `.ilean`, `.c`, `.bc`).
376376
-/
377377
def Module.recBuildLean (mod : Module) : FetchM (Job ModuleOutputArtifacts) := do
378+
/-
379+
Remark: `withRegisterJob` must register `setupJob` to display module builds
380+
in the job monitor. However, it must also include the fetching of both jobs to
381+
ensure all logs end up under its caption in the job monitor.
382+
-/
383+
withRegisterJob mod.name.toString do
378384
let setupJob ← mod.setup.fetch
379385
let leanJob ← mod.lean.fetch
380-
leanJob.bindM (sync := true) fun srcFile => do
381-
let srcTrace ← getTrace
382-
withRegisterJob mod.name.toString do
383386
setupJob.mapM fun setup => do
384387
addLeanTrace
388+
let srcFile ← leanJob.await
389+
let srcTrace := leanJob.getTrace
390+
addTrace srcTrace
385391
addTrace <| traceOptions setup.options "options"
386392
addPureTrace mod.leanArgs "Module.leanArgs"
387393
setTraceCaption s!"{mod.name.toString}:leanArts"

0 commit comments

Comments
 (0)