chore: lake: add build log file path to warning (#4356)

Adds the path to build log to the warning for a missing/invalid build log to help with debugging.
leanprover · Jun 5, 2024 · 9c079a4 · 9c079a4
1 parent 9d47377
commit 9c079a4
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/lake/Lake/Build/Common.lean b/src/lake/Lake/Build/Common.lean
@@ -112,9 +112,9 @@ def replayBuildLog (logFile : FilePath) (depTrace : BuildTrace) : LogIO PUnit :=
     | .ok {log, depHash : BuildLog} =>
       if depTrace.hash == depHash then
         log.replay
-    | .error e => logWarning s!"failed to read cached build log: {e}"
+    | .error e => logWarning s!"{logFile}: invalid build log: {e}"
   | .error (.noFileOrDirectory ..) => pure ()
-  | .error e => logWarning s!"failed to read cached build log: {e}"
+  | .error e => logWarning s!"{logFile}: read failed: {e}"
 
 /-- Saves the log produce by `build` as JSON to `logFile`. -/
 def cacheBuildLog