From a52d95b5759a05ec4263bb5cbf2c0d88ec009e97 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Sun, 1 Aug 2021 14:27:11 -0400
Subject: [PATCH] refactor: `ActiveBuildTarget.buildTask` -> `task`

---
 Lake/Build.lean       |  4 ++--
 Lake/BuildTarget.lean | 14 +++++++-------
 2 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/Lake/Build.lean b/Lake/Build.lean
index 555aa26d8a..06125728ca 100644
--- a/Lake/Build.lean
+++ b/Lake/Build.lean
@@ -125,9 +125,9 @@ def fetchAfterDirectLocalImports
     -- construct target
     let cFile := pkg.modToC mod
     let oleanFile := pkg.modToOlean mod
-    let importTasks := importTargets.map (·.buildTask)
+    let importTasks := importTargets.map (·.task)
     ActiveBuildTarget.mk ⟨oleanFile, cFile⟩ ⟨fullHash, mtime⟩ <| ←
-      skipIf sameHash <| afterTaskList (depsTarget.buildTask :: importTasks) do
+      skipIf sameHash <| afterTaskList (depsTarget.task :: importTasks) do
         compileOleanAndC leanFile oleanFile cFile leanPath pkg.rootDir pkg.leanArgs
         IO.FS.writeFile hashFile (toString fullHash)
 
diff --git a/Lake/BuildTarget.lean b/Lake/BuildTarget.lean
index 95b3469bc8..8730ba69a6 100644
--- a/Lake/BuildTarget.lean
+++ b/Lake/BuildTarget.lean
@@ -11,9 +11,9 @@ namespace Lake
 -- # Active Build Target
 
 structure ActiveBuildTarget (t : Type) (a : Type) where
-  artifact    : a
-  trace       : t
-  buildTask   : BuildTask
+  artifact  : a
+  trace     : t
+  task      : BuildTask
 
 -- manually derive `Inhabited` instance because automatic deriving fails
 instance [Inhabited t] [Inhabited a] : Inhabited (ActiveBuildTarget t a) :=
@@ -46,15 +46,15 @@ def discardArtifact (self : ActiveBuildTarget t α) : ActiveBuildTarget t PUnit
   self.withArtifact ()
 
 def materialize (self : ActiveBuildTarget t α) : IO PUnit :=
-  self.buildTask.await
+  self.task.await
 
 end ActiveBuildTarget
 
 def afterTarget (target : ActiveBuildTarget t a) (act : IO PUnit)  : IO BuildTask :=
-  afterTask target.buildTask act
+  afterTask target.task act
 
 def afterTargetList (targets : List (ActiveBuildTarget t a)) (act : IO PUnit) : IO BuildTask :=
-  afterTaskList (targets.map (·.buildTask)) act
+  afterTaskList (targets.map (·.task)) act
 
 instance : HAndThen (ActiveBuildTarget t a) (IO PUnit) (IO BuildTask) :=
   ⟨afterTarget⟩
@@ -90,7 +90,7 @@ def mtime (self : LeanTarget a) := self.trace.mtime
 def all (targets : List (LeanTarget a)) : IO (LeanTarget PUnit) := do
   let hash := Hash.foldList 0 <| targets.map (·.hash)
   let mtime := MTime.listMax <| targets.map (·.mtime)
-  let task ← BuildTask.all <| targets.map (·.buildTask)
+  let task ← BuildTask.all <| targets.map (·.task)
   return ActiveBuildTarget.mk () ⟨hash, mtime⟩ task
 
 def fromMTimeTarget (target : ActiveBuildTarget MTime a) : LeanTarget a :=