refactor: lake: more robust trace reading (#4518)

The recent change of the trace format exposed some unexpected issues
with Lake's tracing handling. This aims to fix that.

Lake will now perform a rebuild if the trace file is invalid/unreadable.
However, it will still fall back to modification times if the trace file
is missing. Also, Lake is now backwards compatible with the previous
pure numeric traces (and tolerates the absence of a `log` field in the
JSON trace).

(cherry picked from commit f32780d)

src/lake/Lake/Build/Common.lean

@@ -5,6 +5,7 @@ Authors: Mac Malone
 -/
 import Lake.Config.Monad
 import Lake.Build.Actions
+import Lake.Util.JsonObject
 
 /-! # Common Build Tools
 This file defines general utilities that abstract common
@@ -31,15 +32,29 @@ which stores information about a (successful) build.
 structure BuildMetadata where
   depHash : Hash
   log : Log
-  deriving ToJson, FromJson
+  deriving ToJson
+
+def BuildMetadata.ofHash (h : Hash) : BuildMetadata :=
+  {depHash := h, log := {}}
+
+def BuildMetadata.fromJson? (json : Json) : Except String BuildMetadata := do
+  let obj ← JsonObject.fromJson? json
+  let depHash ← obj.get "depHash"
+  let log ← obj.getD "log" {}
+  return {depHash, log}
+
+instance : FromJson BuildMetadata := ⟨BuildMetadata.fromJson?⟩
 
 /-- Read persistent trace data from a file. -/
 def readTraceFile? (path : FilePath) : LogIO (Option BuildMetadata) := OptionT.run do
   match (← IO.FS.readFile path |>.toBaseIO) with
   | .ok contents =>
-    match Json.parse contents >>= fromJson? with
-    | .ok contents => return contents
-    | .error e => logVerbose s!"{path}: invalid trace file: {e}"; failure
+    if let some hash := Hash.ofString? contents.trim then
+      return .ofHash hash
+    else
+      match Json.parse contents >>= fromJson? with
+      | .ok contents => return contents
+      | .error e => logVerbose s!"{path}: invalid trace file: {e}"; failure
   | .error (.noFileOrDirectory ..) => failure
   | .error e => logWarning s!"{path}: read failed: {e}"; failure
 
@@ -86,25 +101,34 @@ then `depTrace` / `oldTrace`. No log will be replayed.
   (depTrace : BuildTrace) (traceFile : FilePath) (build : JobM PUnit)
   (action : JobAction := .build) (oldTrace := depTrace.mtime)
 : JobM Bool := do
-  if let some data ← readTraceFile? traceFile then
-    if (← checkHashUpToDate info depTrace data.depHash oldTrace) then
-      updateAction .replay
-      data.log.replay
-      return true
-  else if (← getIsOldMode) then
-    if (← oldTrace.checkUpToDate info) then
+  if (← traceFile.pathExists) then
+    if let some data ← readTraceFile? traceFile then
+      if (← checkHashUpToDate info depTrace data.depHash oldTrace) then
+        updateAction .replay
+        data.log.replay
+        return true
+      else
+        go
+    else if (← getIsOldMode) && (← oldTrace.checkUpToDate info) then
       return true
-  else if (← depTrace.checkAgainstTime info) then
-    return true
-  if (← getNoBuild) then
-    IO.Process.exit noBuildCode.toUInt8
+    else
+      go
   else
-    updateAction action
-    let iniPos ← getLogPos
-    build -- fatal errors will not produce a trace (or cache their log)
-    let log := (← getLog).takeFrom iniPos
-    writeTraceFile traceFile depTrace log
-    return false
+    if (← depTrace.checkAgainstTime info) then
+      return true
+    else
+      go
+where
+  go := do
+    if (← getNoBuild) then
+      IO.Process.exit noBuildCode.toUInt8
+    else
+      updateAction action
+      let iniPos ← getLogPos
+      build -- fatal errors will not produce a trace (or cache their log)
+      let log := (← getLog).takeFrom iniPos
+      writeTraceFile traceFile depTrace log
+      return false
 
 /--
 Checks whether `info` is up-to-date, and runs `build` to recreate it if not.

src/lake/Lake/Build/Trace.lean

@@ -87,8 +87,11 @@ namespace Hash
 @[inline] def ofNat (n : Nat) :=
   mk n.toUInt64
 
+def ofString? (s : String) : Option Hash :=
+  (inline s.toNat?).map ofNat
+
 def load? (hashFile : FilePath) : BaseIO (Option Hash) :=
-  (·.toNat?.map ofNat) <$> IO.FS.readFile hashFile |>.catchExceptions fun _ => pure none
+  ofString? <$> IO.FS.readFile hashFile |>.catchExceptions fun _ => pure none
 
 def nil : Hash :=
   mk <| 1723 -- same as Name.anonymous

src/lake/Lake/Util/JsonObject.lean

@@ -20,6 +20,9 @@ abbrev JsonObject :=
 
 namespace JsonObject
 
+@[inline] def mk (val : RBNode String (fun _ => Json)) : JsonObject :=
+  val
+
 @[inline] protected def toJson (obj : JsonObject) : Json :=
   .obj obj
 

src/lake/tests/trace/clean.sh

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

src/lake/tests/trace/lakefile.toml

@@ -0,0 +1,5 @@
+name = "test"
+defaultTargets = ["Foo"]
+
+[[lean_lib]]
+name = "Foo"

src/lake/tests/trace/test.sh

@@ -0,0 +1,35 @@
+#!/usr/bin/env bash
+set -euxo pipefail
+
+LAKE=${LAKE:-../../.lake/build/bin/lake}
+
+./clean.sh
+
+# ---
+# Tests aspects of Lake tracing
+# ---
+
+# Tests that a build produces a trace
+test ! -f .lake/build/lib/Foo.trace
+$LAKE build | grep --color "Built Foo"
+test -f .lake/build/lib/Foo.trace
+
+# Tests that a proper trace prevents a rebuild
+$LAKE build --no-build
+
+# Tests that Lake accepts pure numerical traces
+if command -v jq > /dev/null; then # skip if no jq found
+  jq -r '.depHash' .lake/build/lib/Foo.trace > .lake/build/lib/Foo.trace.hash
+  mv .lake/build/lib/Foo.trace.hash .lake/build/lib/Foo.trace
+  $LAKE build --no-build
+fi
+
+# Tests that removal of the trace does not cause a rebuild
+# (if the modification time of the artifact is still newer than the inputs)
+rm .lake/build/lib/Foo.trace
+$LAKE build --no-build
+
+# Tests that an invalid trace does cause a rebuild
+touch .lake/build/lib/Foo.trace
+$LAKE build | grep --color "Built Foo"
+$LAKE build --no-build