From e040804678cc536fdee91eee38f2d10def9ba9b3 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Wed, 14 Jul 2021 13:35:42 -0400
Subject: [PATCH] refactor: split task and trace from target into separate
 files

---
 Lake/BuildTarget.lean | 84 ++++---------------------------------------
 Lake/BuildTask.lean   | 58 ++++++++++++++++++++++++++++++
 Lake/BuildTrace.lean  | 43 ++++++++++++++++++++++
 Lake/Compile.lean     |  1 -
 4 files changed, 108 insertions(+), 78 deletions(-)
 create mode 100644 Lake/BuildTask.lean
 create mode 100644 Lake/BuildTrace.lean

diff --git a/Lake/BuildTarget.lean b/Lake/BuildTarget.lean
index 538a37d2c8..ae1e8287dc 100644
--- a/Lake/BuildTarget.lean
+++ b/Lake/BuildTarget.lean
@@ -3,43 +3,11 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+import Lake.BuildTask
+import Lake.BuildTrace
 
 namespace Lake
 
--- # Build Task
-
-def BuildTask := Task (Except IO.Error PUnit)
-
-namespace BuildTask
-
-def nop : BuildTask :=
-  Task.pure (Except.ok ())
-
-def spawn (action : IO PUnit) (prio := Task.Priority.dedicated) : IO BuildTask :=
-  IO.asTask action prio
-
-def await (self : BuildTask) : IO PUnit := do
-  IO.ofExcept (← IO.wait self)
-
-def all (tasks : List BuildTask) : IO BuildTask :=
-  IO.asTask (tasks.forM (·.await))
-
-end BuildTask
-
-instance : Inhabited BuildTask := ⟨BuildTask.nop⟩
-
-def afterTask (task : BuildTask) (action : IO PUnit)  : IO BuildTask :=
-  IO.mapTask (fun x => IO.ofExcept x *> action) task
-
-def afterTaskList (tasks : List BuildTask) (action : IO PUnit) : IO BuildTask :=
-  IO.mapTasks (fun xs => xs.forM IO.ofExcept *> action) <| tasks
-
-instance : HAndThen BuildTask (IO PUnit) (IO BuildTask) :=
-  ⟨afterTask⟩
-
-instance : HAndThen (List BuildTask) (IO PUnit) (IO BuildTask) :=
-  ⟨afterTaskList⟩
-
 -- # Build Target
 
 structure BuildTarget (t : Type) (a : Type) where
@@ -73,11 +41,11 @@ def materialize (self : BuildTarget t α) : IO PUnit :=
 
 end BuildTarget
 
-def afterTarget (target : BuildTarget t a) (action : IO PUnit)  : IO BuildTask :=
-  afterTask target.buildTask action
+def afterTarget (target : BuildTarget t a) (act : IO PUnit)  : IO BuildTask :=
+  afterTask target.buildTask act
 
-def afterTargetList (targets : List (BuildTarget t a)) (action : IO PUnit) : IO BuildTask :=
-  afterTaskList (targets.map (·.buildTask)) action
+def afterTargetList (targets : List (BuildTarget t a)) (act : IO PUnit) : IO BuildTask :=
+  afterTaskList (targets.map (·.buildTask)) act
 
 instance : HAndThen (BuildTarget t a) (IO PUnit) (IO BuildTask) :=
   ⟨afterTarget⟩
@@ -85,45 +53,7 @@ instance : HAndThen (BuildTarget t a) (IO PUnit) (IO BuildTask) :=
 instance : HAndThen (List (BuildTarget t a)) (IO PUnit) (IO BuildTask) :=
   ⟨afterTargetList⟩
 
--- # Hash Traces
-
-section
-def Hash := UInt64
-
-instance : OfNat Hash n := inferInstanceAs (OfNat UInt64 n)
-instance : Inhabited Hash := inferInstanceAs (Inhabited UInt64)
-instance : BEq Hash := inferInstanceAs (BEq UInt64)
-end
-
-def Hash.ofNat (n : Nat) := UInt64.ofNat n
-def Hash.foldList (init : Hash) (hashes : List Hash) :=
-  List.foldl mixHash init hashes
-
--- # MTime Traces
-
-section
-open IO.FS (SystemTime)
-
-def MTime := SystemTime
-
-instance : Inhabited MTime := ⟨⟨0,0⟩⟩
-instance : OfNat MTime (nat_lit 0) := ⟨⟨0,0⟩⟩
-instance : BEq MTime := inferInstanceAs (BEq SystemTime)
-instance : Repr MTime := inferInstanceAs (Repr SystemTime)
-instance : Ord MTime := inferInstanceAs (Ord SystemTime)
-instance : LT MTime := ltOfOrd
-instance : LE MTime := leOfOrd
-end
-
-def MTime.listMax (mtimes : List MTime) := mtimes.maximum?.getD 0
-
-class GetMTime (α) where
-  getMTime : α → IO MTime
-
-export GetMTime (getMTime)
-
-instance : GetMTime System.FilePath where
-  getMTime file := do (← file.metadata).modified
+-- # MTIme Build Target
 
 abbrev MTimeBuildTarget := BuildTarget MTime
 
diff --git a/Lake/BuildTask.lean b/Lake/BuildTask.lean
new file mode 100644
index 0000000000..5e55d90cb1
--- /dev/null
+++ b/Lake/BuildTask.lean
@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+
+namespace Lake
+
+instance : Monad Task where
+  map := Task.map
+  pure := Task.pure
+  bind := Task.bind
+
+abbrev ETask ε α := ExceptT ε Task α
+
+abbrev IOTask α := ETask IO.Error α
+
+namespace IOTask
+
+def spawn (act : IO α) (prio := Task.Priority.default) : IO (IOTask α) :=
+  IO.asTask act prio
+
+def await (self : IOTask α) : IO α := do
+  IO.ofExcept (← IO.wait self)
+
+def collectAll (tasks : List (IOTask α)) : IO (IOTask (List α)) :=
+  IO.asTask (tasks.mapM (·.await))
+
+end IOTask
+
+def BuildTask := IOTask PUnit
+
+namespace BuildTask
+
+def nop : BuildTask :=
+  pure ()
+
+def spawn (act : IO PUnit) (prio := Task.Priority.dedicated) : IO BuildTask :=
+  IO.asTask act prio
+
+def all (tasks : List BuildTask) (prio := Task.Priority.default)  : IO BuildTask :=
+  IO.asTask (tasks.forM (·.await)) prio
+
+end BuildTask
+
+instance : Inhabited BuildTask := ⟨BuildTask.nop⟩
+
+def afterTask (task : BuildTask) (act : IO PUnit)  : IO BuildTask :=
+  IO.mapTask (fun x => IO.ofExcept x *> act) task
+
+def afterTaskList (tasks : List BuildTask) (act : IO PUnit) : IO BuildTask :=
+  IO.mapTasks (fun xs => xs.forM IO.ofExcept *> act) <| tasks
+
+instance : HAndThen BuildTask (IO PUnit) (IO BuildTask) :=
+  ⟨afterTask⟩
+
+instance : HAndThen (List BuildTask) (IO PUnit) (IO BuildTask) :=
+  ⟨afterTaskList⟩
diff --git a/Lake/BuildTrace.lean b/Lake/BuildTrace.lean
new file mode 100644
index 0000000000..ea82cfa477
--- /dev/null
+++ b/Lake/BuildTrace.lean
@@ -0,0 +1,43 @@
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+
+namespace Lake
+
+-- # Hash Traces
+
+def Hash := UInt64
+
+instance : OfNat Hash n := inferInstanceAs (OfNat UInt64 n)
+instance : Inhabited Hash := inferInstanceAs (Inhabited UInt64)
+instance : BEq Hash := inferInstanceAs (BEq UInt64)
+
+def Hash.ofNat (n : Nat) := UInt64.ofNat n
+def Hash.foldList (init : Hash) (hashes : List Hash) :=
+  List.foldl mixHash init hashes
+
+-- # Modification Time Traces
+
+open IO.FS (SystemTime)
+
+def MTime := SystemTime
+
+instance : Inhabited MTime := ⟨⟨0,0⟩⟩
+instance : OfNat MTime (nat_lit 0) := ⟨⟨0,0⟩⟩
+instance : BEq MTime := inferInstanceAs (BEq SystemTime)
+instance : Repr MTime := inferInstanceAs (Repr SystemTime)
+instance : Ord MTime := inferInstanceAs (Ord SystemTime)
+instance : LT MTime := ltOfOrd
+instance : LE MTime := leOfOrd
+
+def MTime.listMax (mtimes : List MTime) := mtimes.maximum?.getD 0
+
+class GetMTime (α) where
+  getMTime : α → IO MTime
+
+export GetMTime (getMTime)
+
+instance : GetMTime System.FilePath where
+  getMTime file := do (← file.metadata).modified
diff --git a/Lake/Compile.lean b/Lake/Compile.lean
index 234bb0bd74..5e27372a84 100644
--- a/Lake/Compile.lean
+++ b/Lake/Compile.lean
@@ -3,7 +3,6 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
-import Lake.BuildTarget
 
 namespace Lake
 open System