From dba37698c829c25f455cbc78d46b76de16c0e7e9 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Sat, 4 Sep 2021 17:49:08 -0400
Subject: [PATCH] refactor: rename `LakeTrace` to `BuildTrace`

---
 Lake/BuildModule.lean |  4 ++--
 Lake/BuildTarget.lean |  8 ++++----
 Lake/Trace.lean       | 22 +++++++++++-----------
 3 files changed, 17 insertions(+), 17 deletions(-)

diff --git a/Lake/BuildModule.lean b/Lake/BuildModule.lean
index 8250967912..44d9c9bbf5 100644
--- a/Lake/BuildModule.lean
+++ b/Lake/BuildModule.lean
@@ -70,8 +70,8 @@ def skipIf [Pure m] [Pure n] (cond : Bool) (build : m (n PUnit)) : m (n PUnit) :
   if cond then pure (pure ()) else build
 
 def checkModuleTrace [GetMTime i] (info : i)
-(leanFile hashFile : FilePath) (contents : String) (depTrace : LakeTrace)
-: IO (Bool × LakeTrace) := do
+(leanFile hashFile : FilePath) (contents : String) (depTrace : BuildTrace)
+: IO (Bool × BuildTrace) := do
   let leanMTime ← getMTime leanFile
   let leanHash := Hash.compute contents
   let maxMTime := max leanMTime depTrace.mtime
diff --git a/Lake/BuildTarget.lean b/Lake/BuildTarget.lean
index 3e5cf95c89..84073a66fa 100644
--- a/Lake/BuildTarget.lean
+++ b/Lake/BuildTarget.lean
@@ -14,12 +14,12 @@ namespace Lake
 --------------------------------------------------------------------------------
 
 /-- A Lake build target. -/
-abbrev BuildTarget i := Target i BuildM BuildTask LakeTrace
+abbrev BuildTarget i := Target i BuildM BuildTask BuildTrace
 
 -- ## Active
 
 /-- An active Lake build target. -/
-abbrev ActiveBuildTarget i := ActiveTarget i BuildTask LakeTrace
+abbrev ActiveBuildTarget i := ActiveTarget i BuildTask BuildTrace
 
 --------------------------------------------------------------------------------
 -- # File Targets
@@ -44,7 +44,7 @@ abbrev OpaqueTarget := BuildTarget PUnit
 namespace OpaqueTarget
 
 abbrev nil : OpaqueTarget :=
-  Target.pure () LakeTrace.nil
+  Target.pure () BuildTrace.nil
 
 def mixAsync (t1 t2 : OpaqueTarget) : OpaqueTarget :=
   Target.opaque do
@@ -66,7 +66,7 @@ abbrev ActiveOpaqueTarget := ActiveBuildTarget PUnit
 namespace ActiveOpaqueTarget
 
 abbrev nil : ActiveOpaqueTarget :=
-  ActiveTarget.pure () LakeTrace.nil
+  ActiveTarget.pure () BuildTrace.nil
 
 def mixAsync (t1 t2 : ActiveOpaqueTarget) : BuildM ActiveOpaqueTarget := do
   ActiveTarget.opaque <| ←
diff --git a/Lake/Trace.lean b/Lake/Trace.lean
index 9ae28ffb48..47e377364c 100644
--- a/Lake/Trace.lean
+++ b/Lake/Trace.lean
@@ -150,31 +150,31 @@ def checkIfNewer [GetMTime a] (artifact : a) (depMTime : MTime) : IO Bool := do
 --------------------------------------------------------------------------------
 
 /-- Trace used for common Lake targets. Combines `Hash` and `MTime`. -/
-structure LakeTrace where
+structure BuildTrace where
   hash : Hash
   mtime : MTime
 
-namespace LakeTrace
+namespace BuildTrace
 
-def fromHash (hash : Hash) : LakeTrace :=
+def fromHash (hash : Hash) : BuildTrace :=
   mk hash 0
 
-def fromMTime (mtime : MTime) : LakeTrace :=
+def fromMTime (mtime : MTime) : BuildTrace :=
   mk Hash.nil mtime
 
-def nil : LakeTrace :=
+def nil : BuildTrace :=
   mk Hash.nil 0
 
-instance : NilTrace LakeTrace := ⟨nil⟩
+instance : NilTrace BuildTrace := ⟨nil⟩
 
-def compute [ComputeHash a] [GetMTime a] (artifact : a) : IO LakeTrace := do
+def compute [ComputeHash a] [GetMTime a] (artifact : a) : IO BuildTrace := do
   mk (← computeHash artifact) (← getMTime artifact)
 
-instance [ComputeHash a] [GetMTime a] : ComputeTrace a IO LakeTrace := ⟨compute⟩
+instance [ComputeHash a] [GetMTime a] : ComputeTrace a IO BuildTrace := ⟨compute⟩
 
-def mix (t1 t2 : LakeTrace) : LakeTrace :=
+def mix (t1 t2 : BuildTrace) : BuildTrace :=
   mk (Hash.mix t1.hash t2.hash) (max t1.mtime t2.mtime)
 
-instance : MixTrace LakeTrace := ⟨mix⟩
+instance : MixTrace BuildTrace := ⟨mix⟩
 
-end LakeTrace
+end BuildTrace