From ce67d6ef9ea598d5bc7b7dd84985342ca3559db9 Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Tue, 4 Jun 2024 20:35:09 -0400
Subject: [PATCH] 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        | 26 +++++++++++++++++++-------
 src/lake/Lake/Build/Module.lean        |  4 ++--
 src/lake/Lake/Build/Trace.lean         | 13 ++++++++++++-
 src/lake/Lake/Load/Elab.lean           |  3 ---
 src/lake/tests/reversion/Hello.lean    |  1 +
 src/lake/tests/reversion/Main.lean     |  4 ++++
 src/lake/tests/reversion/clean.sh      |  1 +
 src/lake/tests/reversion/lakefile.lean | 10 ++++++++++
 src/lake/tests/reversion/test.sh       | 20 ++++++++++++++++++++
 9 files changed, 69 insertions(+), 13 deletions(-)
 create mode 100644 src/lake/tests/reversion/Hello.lean
 create mode 100644 src/lake/tests/reversion/Main.lean
 create mode 100755 src/lake/tests/reversion/clean.sh
 create mode 100644 src/lake/tests/reversion/lakefile.lean
 create mode 100755 src/lake/tests/reversion/test.sh

diff --git a/src/lake/Lake/Build/Common.lean b/src/lake/Lake/Build/Common.lean
index 8e740a39e1..c3d0c2bbfc 100644
--- a/src/lake/Lake/Build/Common.lean
+++ b/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)
diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean
index d79ee7de3b..63a99af92d 100644
--- a/src/lake/Lake/Build/Module.lean
+++ b/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`. -/
diff --git a/src/lake/Lake/Build/Trace.lean b/src/lake/Lake/Build/Trace.lean
index 43e841a2f6..eaa7123ed6 100644
--- a/src/lake/Lake/Build/Trace.lean
+++ b/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
diff --git a/src/lake/Lake/Load/Elab.lean b/src/lake/Lake/Load/Elab.lean
index 86358388c0..67cc4cb2b0 100644
--- a/src/lake/Lake/Load/Elab.lean
+++ b/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
diff --git a/src/lake/tests/reversion/Hello.lean b/src/lake/tests/reversion/Hello.lean
new file mode 100644
index 0000000000..e6be7b5ab6
--- /dev/null
+++ b/src/lake/tests/reversion/Hello.lean
@@ -0,0 +1 @@
+def hello := "foo"
diff --git a/src/lake/tests/reversion/Main.lean b/src/lake/tests/reversion/Main.lean
new file mode 100644
index 0000000000..8b0717ccc6
--- /dev/null
+++ b/src/lake/tests/reversion/Main.lean
@@ -0,0 +1,4 @@
+import Hello
+
+def main (args : List String) : IO Unit :=
+  IO.println s!"Hello, {hello}!"
diff --git a/src/lake/tests/reversion/clean.sh b/src/lake/tests/reversion/clean.sh
new file mode 100755
index 0000000000..b17e778db0
--- /dev/null
+++ b/src/lake/tests/reversion/clean.sh
@@ -0,0 +1 @@
+rm -rf .lake lake-manifest.json Hello.lean
diff --git a/src/lake/tests/reversion/lakefile.lean b/src/lake/tests/reversion/lakefile.lean
new file mode 100644
index 0000000000..28934dca06
--- /dev/null
+++ b/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
diff --git a/src/lake/tests/reversion/test.sh b/src/lake/tests/reversion/test.sh
new file mode 100755
index 0000000000..d4e8d877d2
--- /dev/null
+++ b/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'