From 9c079a42e1a0d45940c7b39768a12e77800fa45d Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Wed, 5 Jun 2024 11:18:08 -0400 Subject: [PATCH] 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. --- src/lake/Lake/Build/Common.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/lake/Lake/Build/Common.lean b/src/lake/Lake/Build/Common.lean index c3d0c2bbfc..71f1ce9947 100644 --- 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