max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: ActiveBuildTarget.buildTask -> task

Browse source
This commit is contained in:
tydeu 2021-08-01 14:27:11 -04:00
parent 1f51241a8e
commit a52d95b575
2 changed files with 9 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
Lake/Build.lean
View file

@ -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)

14
Lake/BuildTarget.lean
View file

@ -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 :=