refactor: split task and trace from target into separate files
This commit is contained in:
tydeu
parent
3ef381bb6c
commit
e040804678
4 changed files with 108 additions and 78 deletions
|
|
@ -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
|
||||
|
||||
|
|
|
|||
58
Lake/BuildTask.lean
Normal file
58
Lake/BuildTask.lean
Normal file
|
|
@ -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⟩
|
||||
43
Lake/BuildTrace.lean
Normal file
43
Lake/BuildTrace.lean
Normal file
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue