From 83d3f51820e2a2e20a7af0861de21b7978ccccea Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Mon, 2 Dec 2024 17:00:32 -0500
Subject: [PATCH] fix: lake: properly prepend job log in `ensureJob`

---
 src/lake/Lake/Build/Fetch.lean | 10 ++++++----
 src/lake/Lake/Build/Job.lean   |  6 ++++++
 src/lake/Lake/Util/Log.lean    | 11 ++++++++++-
 3 files changed, 22 insertions(+), 5 deletions(-)

diff --git a/src/lake/Lake/Build/Fetch.lean b/src/lake/Lake/Build/Fetch.lean
index 38e9dc7a010f..08ed518ebec7 100644
--- a/src/lake/Lake/Build/Fetch.lean
+++ b/src/lake/Lake/Build/Fetch.lean
@@ -93,10 +93,12 @@ def ensureJob (x : FetchM (Job α))
   let iniPos := log.endPos
   match (← (withLoggedIO x) fetch stack ctx log store) with
   | (.ok job log, store) =>
-    let (log, jobLog) := log.split iniPos
-    let job := if jobLog.isEmpty then job else job.mapResult (sync := true)
-      (·.modifyState (.modifyLog (jobLog ++  ·)))
-    return (.ok job log, store)
+    if iniPos < log.endPos then
+      let (log, jobLog) := log.split iniPos
+      let job := job.mapResult (sync := true) (·.prependLog jobLog)
+      return (.ok job log, store)
+    else
+      return (.ok job log, store)
   | (.error _ log, store) =>
     let (log, jobLog) := log.split iniPos
     return (.ok (.error jobLog) log, store)
diff --git a/src/lake/Lake/Build/Job.lean b/src/lake/Lake/Build/Job.lean
index bcff6b3ea010..be3d1fbc33fa 100644
--- a/src/lake/Lake/Build/Job.lean
+++ b/src/lake/Lake/Build/Job.lean
@@ -64,6 +64,12 @@ def JobState.merge (a b : JobState) : JobState where
 /-- The result of a Lake job. -/
 abbrev JobResult α := EResult Log.Pos JobState α
 
+/-- Add log entries to the beginning of the job's log. -/
+def JobResult.prependLog (log : Log) (self : JobResult α) : JobResult α :=
+  match self with
+  | .ok a s => .ok a <| s.modifyLog (log ++ ·)
+  | .error e s => .error ⟨log.size + e.val⟩ <| s.modifyLog (log ++ ·)
+
 /-- The `Task` of a Lake job. -/
 abbrev JobTask α := BaseIOTask (JobResult α)
 
diff --git a/src/lake/Lake/Util/Log.lean b/src/lake/Lake/Util/Log.lean
index cb08f050d9bc..27103a0a3e2d 100644
--- a/src/lake/Lake/Util/Log.lean
+++ b/src/lake/Lake/Util/Log.lean
@@ -262,9 +262,18 @@ instance : FromJson Log := ⟨(Log.mk <$> fromJson? ·)⟩
 /-- A position in a `Log` (i.e., an array index). Can be past the log's end. -/
 structure Log.Pos where
   val : Nat
-  deriving Inhabited
+  deriving Inhabited, DecidableEq
 
 instance : OfNat Log.Pos (nat_lit 0) := ⟨⟨0⟩⟩
+instance : Ord Log.Pos := ⟨(compare ·.val ·.val)⟩
+instance : LT Log.Pos := ⟨(·.val < ·.val)⟩
+instance : DecidableRel (LT.lt (α := Log.Pos)) :=
+  inferInstanceAs (DecidableRel (α := Log.Pos) (·.val < ·.val))
+instance : LE Log.Pos := ⟨(·.val ≤ ·.val)⟩
+instance : DecidableRel (LE.le (α := Log.Pos)) :=
+  inferInstanceAs (DecidableRel (α := Log.Pos) (·.val ≤ ·.val))
+instance : Min Log.Pos := minOfLe
+instance : Max Log.Pos := maxOfLe
 
 namespace Log