refactor: cleanup opaque target interfaces
This commit is contained in:
tydeu
parent
c843f0b112
commit
43d1dfe72c
6 changed files with 139 additions and 55 deletions
|
|
@ -74,6 +74,9 @@ instance [SeqRightAsync m n] : SeqRightAsync (ReaderT ρ m) n where
|
|||
-- # List/Array Utilities
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
def andThenAsync [Pure m] [BindAsync m n] (ta : n α) (tb : n β) : m (n β) :=
|
||||
bindAsync ta fun _ => pure tb
|
||||
|
||||
-- ## Sequencing Lists/Arrays of Asynchronous Tasks
|
||||
|
||||
section
|
||||
|
|
|
|||
|
|
@ -62,14 +62,14 @@ def skipIf [Pure m] [Pure n] (cond : Bool) (build : m (n PUnit)) : m (n PUnit) :
|
|||
|
||||
/-
|
||||
Produces a recursive module target fetcher that
|
||||
builds the target module after waiting for `depsTarget` to materialize
|
||||
builds the target module after waiting for `depTargets` to materialize
|
||||
and recursively fetching its local imports (relative to `pkg`).
|
||||
|
||||
The module is built with the configuration from `pkg` and
|
||||
a `LEAN_PATH` that includes `oleanDirs`.
|
||||
-/
|
||||
def fetchModuleWithLocalImports
|
||||
(pkg : Package) (oleanDirs : List FilePath) (depsTarget : ActiveBuildTarget PUnit)
|
||||
(pkg : Package) (oleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget)
|
||||
{m} [Monad m] [MonadLiftT BuildM m] [MonadExceptOf IO.Error m] : RecFetch Name ModuleTarget m :=
|
||||
have : MonadLift BuildM m := ⟨liftM⟩
|
||||
let leanPath := SearchPath.toString <| pkg.oleanDir :: oleanDirs
|
||||
|
|
@ -85,8 +85,8 @@ def fetchModuleWithLocalImports
|
|||
-- calculate trace
|
||||
let leanMTime ← getMTime leanFile
|
||||
let leanHash := Hash.compute contents
|
||||
let depTrace := depsTarget.trace.mix <|
|
||||
mixTraceList <| importTargets.map (·.trace)
|
||||
let depTrace := mixTrace depTarget.trace
|
||||
(mixTraceList <| importTargets.map (·.trace))
|
||||
let maxMTime := max leanMTime depTrace.mtime
|
||||
let fullHash := Hash.mix leanHash depTrace.hash
|
||||
let hashFile := pkg.modToHashFile mod
|
||||
|
|
@ -95,9 +95,9 @@ def fetchModuleWithLocalImports
|
|||
-- construct target
|
||||
let cFile := pkg.modToC mod
|
||||
let oleanFile := pkg.modToOlean mod
|
||||
let importTasks := importTargets.map (·.task)
|
||||
let depTasks := depTarget.task :: importTargets.map (·.task)
|
||||
ActiveTarget.mk ⟨oleanFile, cFile⟩ ⟨fullHash, mtime⟩ <| ←
|
||||
skipIf sameHash <| afterTaskList (m := BuildM) (depsTarget.task :: importTasks) do
|
||||
skipIf sameHash <| afterTaskList (m := BuildM) depTasks do
|
||||
compileOleanAndC leanFile oleanFile cFile leanPath pkg.rootDir pkg.leanArgs
|
||||
IO.FS.writeFile hashFile fullHash.toString
|
||||
|
||||
|
|
|
|||
|
|
@ -35,20 +35,20 @@ end PackageTarget
|
|||
-- # Build Modules
|
||||
|
||||
def Package.buildModuleTargetDAGFor
|
||||
(mod : Name) (oleanDirs : List FilePath) (depsTarget : ActiveBuildTarget PUnit)
|
||||
(mod : Name) (oleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget)
|
||||
(self : Package) : BuildM (ModuleTarget × NameMap ModuleTarget) := do
|
||||
let fetch := fetchModuleWithLocalImports self oleanDirs depsTarget
|
||||
let fetch := fetchModuleWithLocalImports self oleanDirs depTarget
|
||||
failOnCycle <| ← buildRBTop fetch mod |>.run {}
|
||||
|
||||
def Package.buildModuleTargetDAG
|
||||
(oleanDirs : List FilePath) (depsTarget : ActiveBuildTarget PUnit) (self : Package) :=
|
||||
self.buildModuleTargetDAGFor self.moduleRoot oleanDirs depsTarget
|
||||
(oleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget) (self : Package) :=
|
||||
self.buildModuleTargetDAGFor self.moduleRoot oleanDirs depTarget
|
||||
|
||||
def Package.buildModuleTargets
|
||||
(mods : List Name) (oleanDirs : List FilePath)
|
||||
(depsTarget : ActiveBuildTarget PUnit) (self : Package)
|
||||
(depTarget : ActiveOpaqueTarget) (self : Package)
|
||||
: BuildM (List ModuleTarget) := do
|
||||
let fetch : ModuleTargetFetch := fetchModuleWithLocalImports self oleanDirs depsTarget
|
||||
let fetch : ModuleTargetFetch := fetchModuleWithLocalImports self oleanDirs depTarget
|
||||
failOnCycle <| ← mods.mapM (buildRBTop fetch) |>.run' {}
|
||||
|
||||
-- # Configure/Build Packages
|
||||
|
|
@ -56,10 +56,11 @@ def Package.buildModuleTargets
|
|||
def Package.buildTargetWithDepTargetsFor
|
||||
(mod : Name) (depTargets : List PackageTarget) (self : Package)
|
||||
: BuildM PackageTarget := do
|
||||
let depsTarget ← ActiveTarget.all <|
|
||||
(← self.buildMoreDepsTarget).withArtifact arbitrary :: depTargets
|
||||
let oLeanDirs := depTargets.map (·.package.oleanDir)
|
||||
let (target, targetMap) ← self.buildModuleTargetDAGFor mod oLeanDirs depsTarget
|
||||
let extraDepTarget ← self.buildExtraDepTarget
|
||||
let depTarget ← ActiveOpaqueTarget.collectList depTargets
|
||||
let allDepsTarget ← extraDepTarget.andThenTargetAsync depTarget
|
||||
let oleanDirs := depTargets.map (·.package.oleanDir)
|
||||
let (target, targetMap) ← self.buildModuleTargetDAGFor mod oleanDirs allDepsTarget
|
||||
return {target with artifact := ⟨self, targetMap⟩}
|
||||
|
||||
def Package.buildTargetWithDepTargets
|
||||
|
|
@ -103,9 +104,10 @@ def Package.buildModuleTargetsWithDeps
|
|||
(deps : List Package) (mods : List Name) (self : Package)
|
||||
: BuildM (List ModuleTarget) := do
|
||||
let oleanDirs := deps.map (·.oleanDir)
|
||||
let depsTarget ← ActiveTarget.all <|
|
||||
(← self.buildMoreDepsTarget).withArtifact arbitrary :: (← deps.mapM (·.buildTarget))
|
||||
self.buildModuleTargets mods oleanDirs depsTarget
|
||||
let extraDepTarget ← self.buildExtraDepTarget
|
||||
let depTarget ← ActiveOpaqueTarget.collectList <| ← deps.mapM (·.buildTarget)
|
||||
let allDepsTarget ← extraDepTarget.andThenTargetAsync depTarget
|
||||
self.buildModuleTargets mods oleanDirs allDepsTarget
|
||||
|
||||
def Package.buildModulesWithDeps
|
||||
(deps : List Package) (mods : List Name) (self : Package)
|
||||
|
|
|
|||
|
|
@ -13,33 +13,27 @@ namespace Lake
|
|||
-- # Build Targets
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
-- ## Inactive Target
|
||||
|
||||
/-- A Lake build target. -/
|
||||
abbrev BuildTarget a :=
|
||||
Target LakeTrace BuildM BuildTask a
|
||||
|
||||
namespace BuildTarget
|
||||
|
||||
def nil : BuildTarget PUnit :=
|
||||
Target.pure () LakeTrace.nil
|
||||
|
||||
def hash (self : BuildTarget a) := self.trace.hash
|
||||
def mtime (self : BuildTarget a) := self.trace.mtime
|
||||
abbrev hash (self : BuildTarget a) := self.trace.hash
|
||||
abbrev mtime (self : BuildTarget a) := self.trace.mtime
|
||||
|
||||
end BuildTarget
|
||||
|
||||
-- ## Active Target
|
||||
-- ## Active
|
||||
|
||||
/-- An active Lake build target. -/
|
||||
abbrev ActiveBuildTarget a :=
|
||||
ActiveTarget LakeTrace BuildTask a
|
||||
|
||||
namespace ActiveBuildTarget
|
||||
|
||||
def nil : ActiveBuildTarget PUnit :=
|
||||
ActiveTarget.pure () LakeTrace.nil
|
||||
|
||||
def hash (self : ActiveBuildTarget a) := self.trace.hash
|
||||
def mtime (self : ActiveBuildTarget a) := self.trace.mtime
|
||||
abbrev hash (self : ActiveBuildTarget a) := self.trace.hash
|
||||
abbrev mtime (self : ActiveBuildTarget a) := self.trace.mtime
|
||||
|
||||
end ActiveBuildTarget
|
||||
|
||||
|
|
@ -47,19 +41,70 @@ end ActiveBuildTarget
|
|||
-- # File Targets
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
-- ## File Target
|
||||
|
||||
/-- A `BuildTarget` that produces a file. -/
|
||||
abbrev FileTarget :=
|
||||
BuildTarget FilePath
|
||||
|
||||
namespace FileTarget
|
||||
|
||||
def compute (file : FilePath) : IO FileTarget :=
|
||||
abbrev compute (file : FilePath) : IO FileTarget :=
|
||||
Target.compute file
|
||||
|
||||
end FileTarget
|
||||
|
||||
-- ## Active File Target
|
||||
-- ## Active
|
||||
|
||||
/-- An `ActiveBuildTarget` that produces a file. -/
|
||||
abbrev ActiveFileTarget :=
|
||||
ActiveBuildTarget FilePath
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- # Opaque Targets
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
/-- A `BuildTarget` with no artifact information. -/
|
||||
abbrev OpaqueTarget :=
|
||||
BuildTarget PUnit
|
||||
|
||||
namespace OpaqueTarget
|
||||
|
||||
abbrev nil : OpaqueTarget :=
|
||||
Target.pure () LakeTrace.nil
|
||||
|
||||
abbrev collectList (targets : List (BuildTarget a)) : OpaqueTarget :=
|
||||
Target.collectOpaqueList targets
|
||||
|
||||
abbrev collectArray (targets : Array (BuildTarget a)) : OpaqueTarget :=
|
||||
Target.collectOpaqueArray targets
|
||||
|
||||
def andThenTargetAsync (t1 t2 : OpaqueTarget) : OpaqueTarget :=
|
||||
let trace := mixTrace t1.trace t2.trace
|
||||
Target.opaque trace do
|
||||
let tk1 ← t1.materializeAsync
|
||||
let tk2 ← t2.materializeAsync
|
||||
andThenAsync tk1 tk2
|
||||
|
||||
end OpaqueTarget
|
||||
|
||||
-- ## Active
|
||||
|
||||
/-- An `ActiveBuildTarget` with no artifact information. -/
|
||||
abbrev ActiveOpaqueTarget :=
|
||||
ActiveBuildTarget PUnit
|
||||
|
||||
namespace ActiveOpaqueTarget
|
||||
|
||||
abbrev nil : ActiveOpaqueTarget :=
|
||||
ActiveTarget.pure () LakeTrace.nil
|
||||
|
||||
abbrev collectList (targets : List (ActiveBuildTarget a)) : BuildM ActiveOpaqueTarget :=
|
||||
ActiveTarget.collectOpaqueList targets
|
||||
|
||||
abbrev collectArray (targets : Array (ActiveBuildTarget a)) : BuildM ActiveOpaqueTarget :=
|
||||
ActiveTarget.collectOpaqueArray targets
|
||||
|
||||
def andThenTargetAsync (t1 t2 : ActiveOpaqueTarget) : BuildM ActiveOpaqueTarget := do
|
||||
let trace := mixTrace t1.trace t2.trace
|
||||
ActiveTarget.opaque trace <| ← andThenAsync t1.task t2.task
|
||||
|
||||
end ActiveOpaqueTarget
|
||||
|
|
|
|||
|
|
@ -52,7 +52,7 @@ structure PackageConfig where
|
|||
buildMoreLibTargets : BuildM (Array ActiveFileTarget) := #[]
|
||||
depsDir : FilePath := defaultDepsDir
|
||||
dependencies : List Dependency := []
|
||||
buildMoreDepsTarget : BuildM (ActiveBuildTarget PUnit) := ActiveBuildTarget.nil
|
||||
buildExtraDepTarget : BuildM ActiveOpaqueTarget := ActiveOpaqueTarget.nil
|
||||
scripts : HashMap String Script := HashMap.empty
|
||||
deriving Inhabited
|
||||
|
||||
|
|
@ -86,8 +86,8 @@ def moduleRootName (self : Package) : String :=
|
|||
def dependencies (self : Package) : List Dependency :=
|
||||
self.config.dependencies
|
||||
|
||||
def buildMoreDepsTarget (self : Package) : BuildM (ActiveBuildTarget PUnit) :=
|
||||
self.config.buildMoreDepsTarget
|
||||
def buildExtraDepTarget (self : Package) : BuildM ActiveOpaqueTarget :=
|
||||
self.config.buildExtraDepTarget
|
||||
|
||||
def leanArgs (self : Package) : Array String :=
|
||||
self.config.leanArgs
|
||||
|
|
|
|||
|
|
@ -64,29 +64,42 @@ namespace ActiveTarget
|
|||
def mk (artifact : a) (trace : t) (task : m PUnit) : ActiveTarget t m a :=
|
||||
⟨artifact, trace, task⟩
|
||||
|
||||
def opaque (trace : t) (task : m PUnit) : ActiveTarget t m PUnit :=
|
||||
⟨(), trace, task⟩
|
||||
|
||||
protected def pure [Pure m] (artifact : a) (trace : t) : ActiveTarget t m a :=
|
||||
⟨artifact, trace, pure ()⟩
|
||||
|
||||
def nil [Pure m] [Inhabited t] : ActiveTarget t m PUnit :=
|
||||
ActiveTarget.pure () Inhabited.default
|
||||
|
||||
def materialize [Await n m] (self : ActiveTarget t n α) : m PUnit :=
|
||||
await self.task
|
||||
|
||||
def andThen [SeqRightAsync m n] (target : ActiveTarget t n a) (act : m PUnit) : m (n PUnit) :=
|
||||
seqRightAsync target.task act
|
||||
-- ## Opaque Active Targets
|
||||
|
||||
instance [SeqRightAsync m n] : HAndThen (ActiveTarget t n a) (m PUnit) (m (n PUnit)) :=
|
||||
⟨andThen⟩
|
||||
def opaque (trace : t) (task : m PUnit) : ActiveTarget t m PUnit :=
|
||||
⟨(), trace, task⟩
|
||||
|
||||
def all [Monad m] [Pure n] [BindAsync m n] [Async m n] [NilTrace t] [MixTrace t]
|
||||
(targets : List (ActiveTarget t n a)) : m (ActiveTarget t n PUnit) := do
|
||||
section
|
||||
variable [NilTrace t] [MixTrace t] [Monad m] [Pure n] [BindAsync m n] [Async m n]
|
||||
|
||||
def collectOpaqueList (targets : List (ActiveTarget t n a)) : m (ActiveTarget t n PUnit) := do
|
||||
let task ← joinTaskList <| targets.map (·.task)
|
||||
let trace := mixTraceList <| targets.map (·.trace)
|
||||
return ActiveTarget.mk () trace task
|
||||
ActiveTarget.opaque trace task
|
||||
|
||||
def collectOpaqueArray (targets : Array (ActiveTarget t n a)) : m (ActiveTarget t n PUnit) := do
|
||||
let task ← joinTaskArray <| targets.map (·.task)
|
||||
let trace := mixTraceArray <| targets.map (·.trace)
|
||||
ActiveTarget.opaque trace task
|
||||
|
||||
end
|
||||
|
||||
-- ## Sequencing
|
||||
|
||||
section
|
||||
variable [SeqRightAsync m n]
|
||||
|
||||
def andThen (target : ActiveTarget t n a) (act : m PUnit) : m (n PUnit) :=
|
||||
seqRightAsync target.task act
|
||||
|
||||
instance : HAndThen (ActiveTarget t n a) (m PUnit) (m (n PUnit)) := ⟨andThen⟩
|
||||
end
|
||||
|
||||
end ActiveTarget
|
||||
|
||||
|
|
@ -124,15 +137,14 @@ namespace Target
|
|||
def mk (artifact : a) (trace : t) (task : m (n PUnit)) : Target t m n a :=
|
||||
⟨artifact, trace, task⟩
|
||||
|
||||
def opaque (trace : t) (task : m (n PUnit)) : Target t m n PUnit :=
|
||||
⟨(), trace, task⟩
|
||||
|
||||
protected def pure [Pure m] [Pure n] (artifact : a) (trace : t) : Target t m n a :=
|
||||
⟨artifact, trace, pure (pure ())⟩
|
||||
|
||||
def compute [ComputeTrace a m' t] [Monad m'] [Pure m] [Pure n] (artifact : a) : m' (Target t m n a) := do
|
||||
Target.pure artifact <| ← computeTrace artifact
|
||||
|
||||
-- ## Materializing
|
||||
|
||||
def run [Monad m] (self : Target t m n a) : m (ActiveTarget t n a) := do
|
||||
self.withTask <| ← self.task
|
||||
|
||||
|
|
@ -159,6 +171,26 @@ def materializeArray [Await n m] (targets : Array (Target t m n a)) : m PUnit :
|
|||
|
||||
end
|
||||
|
||||
-- ## Opaque Targets
|
||||
|
||||
def opaque (trace : t) (task : m (n PUnit)) : Target t m n PUnit :=
|
||||
⟨(), trace, task⟩
|
||||
|
||||
section
|
||||
variable [NilTrace t] [MixTrace t] [Monad m] [Pure n] [BindAsync m n] [Async m n]
|
||||
|
||||
def collectOpaqueList (targets : List (Target t m n a)) : Target t m n PUnit :=
|
||||
let trace := mixTraceList <| targets.map (·.trace)
|
||||
Target.opaque trace do Target.materializeListAsync targets
|
||||
|
||||
def collectOpaqueArray (targets : Array (Target t m n a)) : Target t m n PUnit :=
|
||||
let trace := mixTraceArray <| targets.map (·.trace)
|
||||
Target.opaque trace do Target.materializeArrayAsync targets
|
||||
|
||||
end
|
||||
|
||||
-- ## Sequencing
|
||||
|
||||
section
|
||||
variable [SeqRightAsync m n] [Bind m]
|
||||
|
||||
|
|
@ -170,6 +202,8 @@ end
|
|||
|
||||
end Target
|
||||
|
||||
-- ## Combinators
|
||||
|
||||
section
|
||||
variable [Monad m] [BindAsync m n] [Async m n]
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue