164 lines
4.5 KiB
Text
164 lines
4.5 KiB
Text
/-
|
||
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
|
||
|
||
--------------------------------------------------------------------------------
|
||
-- # Target
|
||
--------------------------------------------------------------------------------
|
||
|
||
structure Target (t : Type) (m : Type) (a : Type) where
|
||
artifact : a
|
||
trace : t
|
||
task : m
|
||
deriving Inhabited
|
||
|
||
namespace Target
|
||
|
||
def withTrace (trace : t) (self : Target r m a) : Target t m a :=
|
||
{self with trace := trace}
|
||
|
||
def discardTrace (self : Target t m a) : Target PUnit m a :=
|
||
self.withTrace ()
|
||
|
||
def withArtifact (artifact : a) (self : Target t m b) : Target t m a :=
|
||
{self with artifact := artifact}
|
||
|
||
def discardArtifact (self : Target t m α) : Target t m PUnit :=
|
||
self.withArtifact ()
|
||
|
||
def mtime (self : Target MTime m a) : MTime :=
|
||
self.trace
|
||
|
||
end Target
|
||
|
||
--------------------------------------------------------------------------------
|
||
-- # Build Targets
|
||
--------------------------------------------------------------------------------
|
||
|
||
-- ## Build Target
|
||
|
||
abbrev BuildTarget (t : Type) (a : Type) := Target t (IO BuildTask) a
|
||
|
||
namespace BuildTarget
|
||
|
||
def mk (artifact : a) (trace : t) (task : IO BuildTask) : BuildTarget t a :=
|
||
⟨artifact, trace, task⟩
|
||
|
||
def opaque (trace : t) (task : IO BuildTask) : BuildTarget t PUnit :=
|
||
⟨(), trace, task⟩
|
||
|
||
def pure (artifact : a) (trace : t) : BuildTarget t a :=
|
||
⟨artifact, trace, BuildTask.nop⟩
|
||
|
||
def nil [Inhabited t] : BuildTarget t PUnit :=
|
||
pure () Inhabited.default
|
||
|
||
def spawn (self : BuildTarget t α) : IO BuildTask :=
|
||
self.task
|
||
|
||
def materialize (self : BuildTarget t α) : IO PUnit := do
|
||
(← self.task).await
|
||
|
||
end BuildTarget
|
||
|
||
-- ## Active Build Target
|
||
|
||
abbrev ActiveBuildTarget (t : Type) (a : Type) := Target t BuildTask a
|
||
|
||
namespace ActiveBuildTarget
|
||
|
||
def mk (artifact : a) (trace : t) (task : BuildTask) : ActiveBuildTarget t a :=
|
||
⟨artifact, trace, task⟩
|
||
|
||
def opaque (trace : t) (task : BuildTask) : ActiveBuildTarget t PUnit :=
|
||
⟨(), trace, task⟩
|
||
|
||
def pure (artifact : a) (trace : t) : ActiveBuildTarget t a :=
|
||
⟨artifact, trace, BuildTask.nop⟩
|
||
|
||
def nil [Inhabited t] : ActiveBuildTarget t PUnit :=
|
||
pure () Inhabited.default
|
||
|
||
def materialize (self : ActiveBuildTarget t α) : IO PUnit :=
|
||
self.task.await
|
||
|
||
end ActiveBuildTarget
|
||
|
||
-- ## Combinators
|
||
|
||
def afterTarget (target : ActiveBuildTarget t a) (act : IO PUnit) : IO BuildTask :=
|
||
afterTask target.task act
|
||
|
||
def afterTargetList (targets : List (ActiveBuildTarget t a)) (act : IO PUnit) : IO BuildTask :=
|
||
afterTaskList (targets.map (·.task)) act
|
||
|
||
instance : HAndThen (ActiveBuildTarget t a) (IO PUnit) (IO BuildTask) :=
|
||
⟨afterTarget⟩
|
||
|
||
instance : HAndThen (List (ActiveBuildTarget t a)) (IO PUnit) (IO BuildTask) :=
|
||
⟨afterTargetList⟩
|
||
|
||
--------------------------------------------------------------------------------
|
||
-- # File Targets
|
||
--------------------------------------------------------------------------------
|
||
|
||
section
|
||
open System
|
||
|
||
-- ## File Target
|
||
|
||
abbrev FileTarget := BuildTarget MTime FilePath
|
||
|
||
namespace FileTarget
|
||
|
||
def mk (file : FilePath) (depMTime : MTime) (task : IO BuildTask) : FileTarget :=
|
||
⟨file, depMTime, task⟩
|
||
|
||
def pure (file : FilePath) (depMTime : MTime) : FileTarget :=
|
||
BuildTarget.pure file depMTime
|
||
|
||
end FileTarget
|
||
|
||
-- ## Active File Target
|
||
|
||
abbrev ActiveFileTarget := ActiveBuildTarget MTime FilePath
|
||
|
||
namespace ActiveFileTarget
|
||
|
||
def mk (file : FilePath) (depMTime : MTime) (task : BuildTask) : ActiveFileTarget :=
|
||
ActiveBuildTarget.mk file depMTime task
|
||
|
||
def pure (file : FilePath) (depMTime : MTime) : ActiveFileTarget :=
|
||
ActiveBuildTarget.pure file depMTime
|
||
|
||
end ActiveFileTarget
|
||
|
||
end
|
||
|
||
--------------------------------------------------------------------------------
|
||
-- # Lean Target
|
||
--------------------------------------------------------------------------------
|
||
|
||
abbrev LeanTarget a := ActiveBuildTarget LeanTrace a
|
||
|
||
namespace LeanTarget
|
||
|
||
def hash (self : LeanTarget a) := self.trace.hash
|
||
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 (·.task)
|
||
return ActiveBuildTarget.mk () ⟨hash, mtime⟩ task
|
||
|
||
def fromMTimeTarget (target : ActiveBuildTarget MTime a) : LeanTarget a :=
|
||
{target with trace := LeanTrace.fromMTime target.trace}
|
||
|
||
end LeanTarget
|