From 3e16f5332faba0844efb1524222df026095bff14 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Tue, 20 Jan 2026 17:22:40 -0500 Subject: [PATCH] feat: lake: `.nobuild` trace file for debugging (#12076) This PR adds additional debugging information to a run of `lake build --no-build` via a `.nobuild` trace file. When a build fails due to needing a rebuild, Lake emits the new expected trace next as `.nobuild` file next to the build's old `.trace`. The inputs recorded in these files can then be compared to debug what caused the mismatch. To help keep the build directory clean, the `.nobuild` trace file is removed on the next successful build. --- src/lake/Lake/Build/Common.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/lake/Lake/Build/Common.lean b/src/lake/Lake/Build/Common.lean index c80ad94a95..d5c1219de7 100644 --- a/src/lake/Lake/Build/Common.lean +++ b/src/lake/Lake/Build/Common.lean @@ -9,7 +9,7 @@ prelude public import Lake.Build.Job.Monad public import Lake.Config.Monad public import Lake.Util.JsonObject -import Lake.Util.IO +public import Lake.Util.IO import Lake.Build.Target.Fetch public import Lake.Build.Actions @@ -304,8 +304,10 @@ and log are saved to `traceFile`, if the build completes without a fatal error (depTrace : BuildTrace) (traceFile : FilePath) (build : JobM α) (action : JobAction := .build) : JobM α := do + let noBuildTraceFile := traceFile.addExtension "nobuild" if (← getNoBuild) then updateAction .build + writeBuildTrace noBuildTraceFile depTrace Json.null {} error s!"target is out-of-date and needs to be rebuilt" else updateAction action @@ -315,6 +317,7 @@ and log are saved to `traceFile`, if the build completes without a fatal error let a ← build -- fatal errors will abort here let log := (← getLog).takeFrom iniPos writeBuildTrace traceFile depTrace (toOutputJson a) log + removeFileIfExists noBuildTraceFile return a finally let endTime ← IO.monoMsNow