fix: lake: track trace of cached build logs (#4343)

Stores the dependency trace for a build in the cached build log and then
verifies that it matches the trace of the current build before replaying
the log. Includes test.

Closes #4303.

src/lake/Lake/Build/Common.lean

@@ -95,27 +95,39 @@ def cacheFileHash (file : FilePath) : IO Hash := do
   IO.FS.writeFile hashFile hash.toString
   return hash
 
+/-- The build log file format. -/
+structure BuildLog where
+  depHash : Hash
+  log : Log
+  deriving ToJson, FromJson
+
 /--
 Replays the JSON log in `logFile` (if it exists).
 If the log file is malformed, logs a warning.
 -/
-def replayBuildLog (logFile : FilePath) : LogIO PUnit := do
+def replayBuildLog (logFile : FilePath) (depTrace : BuildTrace) : LogIO PUnit := do
   match (← IO.FS.readFile logFile |>.toBaseIO) with
   | .ok contents =>
     match Json.parse contents >>= fromJson? with
-    | .ok entries => Log.mk entries |>.replay
-    | .error e => logWarning s!"cached build log is corrupted: {e}"
+    | .ok {log, depHash : BuildLog} =>
+      if depTrace.hash == depHash then
+        log.replay
+    | .error e => logWarning s!"failed to read cached build log: {e}"
   | .error (.noFileOrDirectory ..) => pure ()
   | .error e => logWarning s!"failed to read cached build log: {e}"
 
 /-- Saves the log produce by `build` as JSON to `logFile`. -/
-def cacheBuildLog (logFile : FilePath) (build : JobM PUnit) : JobM PUnit := do
+def cacheBuildLog
+  (logFile : FilePath) (depTrace : BuildTrace) (build : JobM PUnit)
+: JobM PUnit := do
   let iniPos ← getLogPos
   let errPos? ← try build; pure none catch errPos => pure (some errPos)
   let log := (← getLog).takeFrom iniPos
   unless log.isEmpty do
+    let log := {log, depHash := depTrace.hash : BuildLog}
     IO.FS.writeFile logFile (toJson log).pretty
-  if let some errPos := errPos? then throw errPos
+  if let some errPos := errPos? then
+    throw errPos
 
 /--
 Builds `file` using `build` unless it already exists and `depTrace` matches
@@ -133,10 +145,10 @@ def buildFileUnlessUpToDate
 : JobM BuildTrace := do
   let traceFile := FilePath.mk <| file.toString ++ ".trace"
   let logFile := FilePath.mk <| file.toString ++ ".log.json"
-  let build := cacheBuildLog logFile build
+  let build := cacheBuildLog logFile depTrace build
   if (← buildUnlessUpToDate? file depTrace traceFile build) then
     updateAction .replay
-    replayBuildLog logFile
+    replayBuildLog logFile depTrace
     fetchFileTrace file
   else
     return .mk (← cacheFileHash file) (← getMTime file)

src/lake/Lake/Build/Module.lean

@@ -157,7 +157,7 @@ def Module.recBuildLean (mod : Module) : FetchM (BuildJob Unit) := do
     let upToDate ← buildUnlessUpToDate? (oldTrace := srcTrace) mod modTrace mod.traceFile do
       let hasLLVM := Lean.Internal.hasLLVMBackend ()
       let bcFile? := if hasLLVM then some mod.bcFile else none
-      cacheBuildLog mod.logFile do
+      cacheBuildLog mod.logFile modTrace do
         compileLeanModule mod.leanFile mod.oleanFile mod.ileanFile mod.cFile bcFile?
           (← getLeanPath) mod.rootDir dynlibs dynlibPath (mod.weakLeanArgs ++ mod.leanArgs) (← getLean)
       discard <| cacheFileHash mod.oleanFile
@@ -167,7 +167,7 @@ def Module.recBuildLean (mod : Module) : FetchM (BuildJob Unit) := do
         discard <| cacheFileHash mod.bcFile
     if upToDate then
       updateAction .replay
-      replayBuildLog mod.logFile
+      replayBuildLog mod.logFile modTrace
     return ((), depTrace)
 
 /-- The `ModuleFacetConfig` for the builtin `leanArtsFacet`. -/

src/lake/Lake/Build/Trace.lean

@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 import Lake.Util.IO
+import Lean.Data.Json
 
-open System
+open System Lean
 
 namespace Lake
 
@@ -110,6 +111,16 @@ instance : ToString Hash := ⟨Hash.toString⟩
 @[inline] def ofByteArray (bytes : ByteArray) : Hash :=
   ⟨hash bytes⟩
 
+@[inline] protected def toJson (self : Hash) : Json :=
+  toJson self.val
+
+instance : ToJson Hash := ⟨Hash.toJson⟩
+
+@[inline] protected def fromJson? (json : Json) : Except String Hash :=
+  (⟨·⟩) <$> fromJson? json
+
+instance : FromJson Hash := ⟨Hash.fromJson?⟩
+
 end Hash
 
 class ComputeHash (α : Type u) (m : outParam $ Type → Type v)  where

src/lake/Lake/Load/Elab.lean

@@ -143,9 +143,6 @@ where
     -- IR Extension (for constant evaluation)
     |>.insert ``IR.declMapExt
 
-instance : ToJson Hash := ⟨(toJson ·.val)⟩
-instance : FromJson Hash := ⟨((⟨·⟩) <$> fromJson? ·)⟩
-
 structure ConfigTrace where
   platform : String
   leanHash : String

src/lake/tests/reversion/Hello.lean

@@ -0,0 +1 @@
+def hello := "foo"

src/lake/tests/reversion/Main.lean

@@ -0,0 +1,4 @@
+import Hello
+
+def main (args : List String) : IO Unit :=
+  IO.println s!"Hello, {hello}!"

src/lake/tests/reversion/clean.sh

@@ -0,0 +1 @@
+rm -rf .lake lake-manifest.json Hello.lean

src/lake/tests/reversion/lakefile.lean

@@ -0,0 +1,10 @@
+import Lake
+open Lake DSL
+
+package test
+
+lean_lib Hello
+
+@[default_target]
+lean_exe hello where
+  root := `Main

src/lake/tests/reversion/test.sh

@@ -0,0 +1,20 @@
+#!/usr/bin/env bash
+set -euxo pipefail
+
+LAKE=${LAKE:-../../.lake/build/bin/lake}
+
+./clean.sh
+
+# Test that introducing an error and reverting works
+# https://github.com/leanprover/lean4/issues/4303
+
+# Initial state
+echo 'def hello := "foo"' > Hello.lean
+$LAKE -q build
+# Introduce error
+echo 'error' > Hello.lean
+$LAKE build && exit 1 || true
+# Revert
+echo 'def hello := "foo"' > Hello.lean
+# Ensure error is not presevered but the warning in another file is
+$LAKE -q build | grep --color 'Replayed Main'