From 9db41f99310c517e5cd6e9551734c3eab8e5ed35 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Mon, 30 Jun 2025 11:48:01 -0400 Subject: [PATCH] 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. --- src/lake/Lake/Build/Module.lean | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean index c427909220..d9e2150ae6 100644 --- a/src/lake/Lake/Build/Module.lean +++ b/src/lake/Lake/Build/Module.lean @@ -375,13 +375,19 @@ Fetch its dependencies and then elaborate the Lean source file, producing all possible artifacts (e.g., `.olean`, `.ilean`, `.c`, `.bc`). -/ def Module.recBuildLean (mod : Module) : FetchM (Job ModuleOutputArtifacts) := do + /- + Remark: `withRegisterJob` must register `setupJob` to display module builds + in the job monitor. However, it must also include the fetching of both jobs to + ensure all logs end up under its caption in the job monitor. + -/ + withRegisterJob mod.name.toString do let setupJob ← mod.setup.fetch let leanJob ← mod.lean.fetch - leanJob.bindM (sync := true) fun srcFile => do - let srcTrace ← getTrace - withRegisterJob mod.name.toString do setupJob.mapM fun setup => do addLeanTrace + let srcFile ← leanJob.await + let srcTrace := leanJob.getTrace + addTrace srcTrace addTrace <| traceOptions setup.options "options" addPureTrace mod.leanArgs "Module.leanArgs" setTraceCaption s!"{mod.name.toString}:leanArts"