refactor: BuildTagret -> ActiveBuildTarget
This commit is contained in:
tydeu
parent
0dfd07ed9d
commit
b730aacbc8
5 changed files with 58 additions and 83 deletions
|
|
@ -33,17 +33,17 @@ abbrev ModuleTarget := LeanTarget ModuleArtifact
|
|||
namespace ModuleTarget
|
||||
|
||||
def mk (olean c : FilePath) (hash : Hash) (mtime : IO.FS.SystemTime) (task : BuildTask) : ModuleTarget :=
|
||||
BuildTarget.mk ⟨olean, c⟩ ⟨hash, mtime⟩ task
|
||||
ActiveBuildTarget.mk ⟨olean, c⟩ ⟨hash, mtime⟩ task
|
||||
|
||||
def pure (olean c : FilePath) (hash : Hash) (mtime : IO.FS.SystemTime) : ModuleTarget :=
|
||||
BuildTarget.pure ⟨olean, c⟩ ⟨hash, mtime⟩
|
||||
ActiveBuildTarget.pure ⟨olean, c⟩ ⟨hash, mtime⟩
|
||||
|
||||
def oleanFile (self : ModuleTarget) := self.artifact.oleanFile
|
||||
def oleanTarget (self : ModuleTarget) : FileTarget :=
|
||||
def oleanTarget (self : ModuleTarget) : ActiveFileTarget :=
|
||||
{self with artifact := self.oleanFile, trace := self.mtime}
|
||||
|
||||
def cFile (self : ModuleTarget) := self.artifact.cFile
|
||||
def cTarget (self : ModuleTarget) : FileTarget :=
|
||||
def cTarget (self : ModuleTarget) : ActiveFileTarget :=
|
||||
{self with artifact := self.cFile, trace := self.mtime}
|
||||
|
||||
end ModuleTarget
|
||||
|
|
@ -85,8 +85,8 @@ def skipIf [Pure m] (cond : Bool) (build : m BuildTask) : m BuildTask := do
|
|||
def skipIfNewer [GetMTime a]
|
||||
(artifact : a) (depMTime : MTime)
|
||||
{m} [Monad m] [MonadLiftT IO m] [MonadExceptOf IO.Error m]
|
||||
(build : m BuildTask) : m (MTimeBuildTarget a) := do
|
||||
MTimeBuildTarget.mk artifact depMTime <| ←
|
||||
(build : m BuildTask) : m (ActiveBuildTarget MTime a) := do
|
||||
ActiveBuildTarget.mk artifact depMTime <| ←
|
||||
skipIf (← checkIfNewer artifact depMTime) build
|
||||
|
||||
-- # Build Modules
|
||||
|
|
@ -126,7 +126,7 @@ def fetchAfterDirectLocalImports
|
|||
let cFile := pkg.modToC mod
|
||||
let oleanFile := pkg.modToOlean mod
|
||||
let importTasks := importTargets.map (·.buildTask)
|
||||
BuildTarget.mk ⟨oleanFile, cFile⟩ ⟨fullHash, mtime⟩ <| ←
|
||||
ActiveBuildTarget.mk ⟨oleanFile, cFile⟩ ⟨fullHash, mtime⟩ <| ←
|
||||
skipIf sameHash <| afterTaskList (depsTarget.buildTask :: importTasks) do
|
||||
compileOleanAndC leanFile oleanFile cFile leanPath pkg.dir pkg.leanArgs
|
||||
IO.FS.writeFile hashFile (toString fullHash)
|
||||
|
|
|
|||
|
|
@ -11,17 +11,17 @@ namespace Lake
|
|||
-- # Build `.o` Files
|
||||
|
||||
def buildLeanO (oFile : FilePath)
|
||||
(cTarget : BuildTarget t FilePath) (leancArgs : Array String := #[]) : IO BuildTask :=
|
||||
(cTarget : ActiveBuildTarget t FilePath) (leancArgs : Array String := #[]) : IO BuildTask :=
|
||||
afterTarget cTarget <| compileLeanO oFile cTarget.artifact leancArgs
|
||||
|
||||
def fetchLeanOFileTarget (oFile : FilePath)
|
||||
(cTarget : FileTarget) (leancArgs : Array String := #[]) : IO FileTarget :=
|
||||
(cTarget : ActiveFileTarget) (leancArgs : Array String := #[]) : IO ActiveFileTarget :=
|
||||
skipIfNewer oFile cTarget.mtime <| buildLeanO oFile cTarget leancArgs
|
||||
|
||||
-- # Build Package Lib
|
||||
|
||||
def PackageTarget.fetchOFileTargets
|
||||
(self : PackageTarget) : IO (List FileTarget) := do
|
||||
(self : PackageTarget) : IO (List ActiveFileTarget) := do
|
||||
self.moduleTargets.toList.mapM fun (mod, target) => do
|
||||
let oFile := self.package.modToO mod
|
||||
fetchLeanOFileTarget (oFile) target.cTarget self.package.leancArgs
|
||||
|
|
@ -32,10 +32,10 @@ def PackageTarget.buildStaticLib
|
|||
let oFiles := oFileTargets.map (·.artifact) |>.toArray
|
||||
oFileTargets >> compileStaticLib self.package.staticLibFile oFiles
|
||||
|
||||
def PackageTarget.fetchStaticLibTarget (self : PackageTarget) : IO FileTarget := do
|
||||
def PackageTarget.fetchStaticLibTarget (self : PackageTarget) : IO ActiveFileTarget := do
|
||||
skipIfNewer self.package.staticLibFile self.mtime self.buildStaticLib
|
||||
|
||||
def Package.fetchStaticLibTarget (self : Package) : IO FileTarget := do
|
||||
def Package.fetchStaticLibTarget (self : Package) : IO ActiveFileTarget := do
|
||||
(← self.buildTarget).fetchStaticLibTarget
|
||||
|
||||
def Package.fetchStaticLib (self : Package) : IO FilePath := do
|
||||
|
|
@ -60,10 +60,10 @@ def PackageTarget.buildBin
|
|||
linkTargets >> compileLeanBin self.package.binFile linkFiles self.package.linkArgs
|
||||
|
||||
def PackageTarget.fetchBinTarget
|
||||
(depTargets : List PackageTarget) (self : PackageTarget) : IO FileTarget :=
|
||||
(depTargets : List PackageTarget) (self : PackageTarget) : IO ActiveFileTarget :=
|
||||
skipIfNewer self.package.binFile self.mtime <| self.buildBin depTargets
|
||||
|
||||
def Package.fetchBinTarget (self : Package) : IO FileTarget := do
|
||||
def Package.fetchBinTarget (self : Package) : IO ActiveFileTarget := do
|
||||
let depTargets ← self.buildDepTargets
|
||||
let pkgTarget ← self.buildTargetWithDepTargets depTargets
|
||||
pkgTarget.fetchBinTarget depTargets
|
||||
|
|
|
|||
|
|
@ -8,104 +8,79 @@ import Lake.BuildTrace
|
|||
|
||||
namespace Lake
|
||||
|
||||
-- # Build Target
|
||||
-- # Active Build Target
|
||||
|
||||
structure BuildTarget (t : Type) (a : Type) where
|
||||
structure ActiveBuildTarget (t : Type) (a : Type) where
|
||||
artifact : a
|
||||
trace : t
|
||||
buildTask : BuildTask
|
||||
|
||||
-- manually derive `Inhabited` instance because automatic deriving fails
|
||||
instance [Inhabited t] [Inhabited a] : Inhabited (BuildTarget t a) :=
|
||||
instance [Inhabited t] [Inhabited a] : Inhabited (ActiveBuildTarget t a) :=
|
||||
⟨Inhabited.default, Inhabited.default, BuildTask.nop⟩
|
||||
|
||||
namespace BuildTarget
|
||||
namespace ActiveBuildTarget
|
||||
|
||||
def nil [Inhabited t] : BuildTarget t PUnit :=
|
||||
def nil [Inhabited t] : ActiveBuildTarget t PUnit :=
|
||||
⟨(), Inhabited.default, BuildTask.nop⟩
|
||||
|
||||
def pure (artifact : a) (trace : t) : BuildTarget t a :=
|
||||
{artifact, trace, buildTask := BuildTask.nop}
|
||||
def pure (artifact : a) (trace : t) : ActiveBuildTarget t a :=
|
||||
⟨artifact, trace, BuildTask.nop⟩
|
||||
|
||||
def opaque (trace : t) (task : BuildTask) : BuildTarget t PUnit :=
|
||||
def opaque (trace : t) (task : BuildTask) : ActiveBuildTarget t PUnit :=
|
||||
⟨(), trace, task⟩
|
||||
|
||||
def withTrace (trace : t) (self : BuildTarget r a) : BuildTarget t a :=
|
||||
def withTrace (trace : t) (self : ActiveBuildTarget r a) : ActiveBuildTarget t a :=
|
||||
{self with trace := trace}
|
||||
|
||||
def discardTrace (self : BuildTarget t a) : BuildTarget PUnit a :=
|
||||
def discardTrace (self : ActiveBuildTarget t a) : ActiveBuildTarget PUnit a :=
|
||||
self.withTrace ()
|
||||
|
||||
def withArtifact (artifact : a) (self : BuildTarget t b) : BuildTarget t a :=
|
||||
{self with artifact := artifact}
|
||||
|
||||
def discardArtifact (self : BuildTarget t α) : BuildTarget t PUnit :=
|
||||
self.withArtifact ()
|
||||
|
||||
def materialize (self : BuildTarget t α) : IO PUnit :=
|
||||
self.buildTask.await
|
||||
|
||||
end BuildTarget
|
||||
|
||||
def afterTarget (target : BuildTarget t a) (act : IO PUnit) : IO BuildTask :=
|
||||
afterTask target.buildTask act
|
||||
|
||||
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⟩
|
||||
|
||||
instance : HAndThen (List (BuildTarget t a)) (IO PUnit) (IO BuildTask) :=
|
||||
⟨afterTargetList⟩
|
||||
|
||||
-- # MTIme Build Target
|
||||
|
||||
abbrev MTimeBuildTarget := BuildTarget MTime
|
||||
|
||||
namespace MTimeBuildTarget
|
||||
|
||||
def mtime (self : MTimeBuildTarget a) :=
|
||||
def mtime (self : ActiveBuildTarget MTime a) : MTime :=
|
||||
self.trace
|
||||
|
||||
def mk (artifact : a) (mtime : MTime := 0) (buildTask : BuildTask) : MTimeBuildTarget a :=
|
||||
{artifact, trace := mtime, buildTask}
|
||||
def withArtifact (artifact : a) (self : ActiveBuildTarget t b) : ActiveBuildTarget t a :=
|
||||
{self with artifact := artifact}
|
||||
|
||||
def pure (artifact : a) (mtime : MTime := 0) : MTimeBuildTarget a :=
|
||||
{artifact, trace := mtime, buildTask := BuildTask.nop}
|
||||
def discardArtifact (self : ActiveBuildTarget t α) : ActiveBuildTarget t PUnit :=
|
||||
self.withArtifact ()
|
||||
|
||||
def all (targets : List (MTimeBuildTarget a)) : IO (MTimeBuildTarget PUnit) := do
|
||||
let depsMTime := MTime.listMax <| targets.map (·.mtime)
|
||||
let task ← BuildTask.all <| targets.map (·.buildTask)
|
||||
return MTimeBuildTarget.mk () depsMTime task
|
||||
def materialize (self : ActiveBuildTarget t α) : IO PUnit :=
|
||||
self.buildTask.await
|
||||
|
||||
def collectAll (targets : List (MTimeBuildTarget a)) : IO (MTimeBuildTarget (List a)) := do
|
||||
let artifacts := targets.map (·.artifact)
|
||||
let depsMTime := MTime.listMax <| targets.map (·.mtime)
|
||||
let task ← BuildTask.all <| targets.map (·.buildTask)
|
||||
return MTimeBuildTarget.mk artifacts depsMTime task
|
||||
end ActiveBuildTarget
|
||||
|
||||
end MTimeBuildTarget
|
||||
def afterTarget (target : ActiveBuildTarget t a) (act : IO PUnit) : IO BuildTask :=
|
||||
afterTask target.buildTask act
|
||||
|
||||
def afterTargetList (targets : List (ActiveBuildTarget t a)) (act : IO PUnit) : IO BuildTask :=
|
||||
afterTaskList (targets.map (·.buildTask)) act
|
||||
|
||||
instance : HAndThen (ActiveBuildTarget t a) (IO PUnit) (IO BuildTask) :=
|
||||
⟨afterTarget⟩
|
||||
|
||||
instance : HAndThen (List (ActiveBuildTarget t a)) (IO PUnit) (IO BuildTask) :=
|
||||
⟨afterTargetList⟩
|
||||
|
||||
-- # File Target
|
||||
|
||||
open System
|
||||
|
||||
abbrev FileTarget := MTimeBuildTarget FilePath
|
||||
abbrev ActiveFileTarget := ActiveBuildTarget MTime FilePath
|
||||
|
||||
namespace FileTarget
|
||||
namespace ActiveFileTarget
|
||||
|
||||
def mk (file : FilePath) (maxMTime : MTime) (task : BuildTask) :=
|
||||
BuildTarget.mk file maxMTime task
|
||||
def mk (file : FilePath) (depMTime : MTime) (task : BuildTask) :=
|
||||
ActiveBuildTarget.mk file depMTime task
|
||||
|
||||
def pure (file : FilePath) (maxMTime : MTime) :=
|
||||
BuildTarget.pure file maxMTime
|
||||
def pure (file : FilePath) (depMTime : MTime) :=
|
||||
ActiveBuildTarget.pure file depMTime
|
||||
|
||||
end FileTarget
|
||||
end ActiveFileTarget
|
||||
|
||||
-- # Lean Target
|
||||
|
||||
abbrev LeanTarget a := BuildTarget LeanTrace a
|
||||
abbrev LeanTarget a := ActiveBuildTarget LeanTrace a
|
||||
|
||||
namespace LeanTarget
|
||||
|
||||
|
|
@ -116,9 +91,9 @@ 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)
|
||||
return BuildTarget.mk () ⟨hash, mtime⟩ task
|
||||
return ActiveBuildTarget.mk () ⟨hash, mtime⟩ task
|
||||
|
||||
def fromMTimeTarget (target : MTimeBuildTarget a) : LeanTarget a :=
|
||||
{target with trace := LeanTrace.fromMTime target.mtime}
|
||||
def fromMTimeTarget (target : ActiveBuildTarget MTime a) : LeanTarget a :=
|
||||
{target with trace := LeanTrace.fromMTime target.trace}
|
||||
|
||||
end LeanTarget
|
||||
|
|
|
|||
|
|
@ -49,7 +49,7 @@ structure PackageConfig where
|
|||
libName : String := moduleRoot.toString (escape := false)
|
||||
depsDir : FilePath := defaultDepsDir
|
||||
dependencies : List Dependency := []
|
||||
buildMoreDepsTarget : IO (BuildTarget LeanTrace PUnit) := BuildTarget.nil
|
||||
buildMoreDepsTarget : IO (ActiveBuildTarget LeanTrace PUnit) := ActiveBuildTarget.nil
|
||||
scripts : HashMap String Script := HashMap.empty
|
||||
deriving Inhabited
|
||||
|
||||
|
|
@ -83,7 +83,7 @@ def moduleRootName (self : Package) : String :=
|
|||
def dependencies (self : Package) : List Dependency :=
|
||||
self.config.dependencies
|
||||
|
||||
def buildMoreDepsTarget (self : Package) : IO (BuildTarget LeanTrace PUnit) :=
|
||||
def buildMoreDepsTarget (self : Package) : IO (ActiveBuildTarget LeanTrace PUnit) :=
|
||||
self.config.buildMoreDepsTarget
|
||||
|
||||
def leanArgs (self : Package) : Array String :=
|
||||
|
|
|
|||
|
|
@ -9,11 +9,11 @@ def buildDir := defaultBuildDir
|
|||
def addO := buildDir / extDir / "add.o"
|
||||
def extLib := buildDir / extDir / "libext.a"
|
||||
|
||||
def fetchAddOTarget : IO FileTarget := do
|
||||
def fetchAddOTarget : IO ActiveFileTarget := do
|
||||
skipIfNewer addO (← getMTime addSrc) <|
|
||||
BuildTask.spawn <| compileO addO addSrc (cmd := "c++")
|
||||
|
||||
def fetchExtLibTarget : IO FileTarget := do
|
||||
def fetchExtLibTarget : IO ActiveFileTarget := do
|
||||
let oTarget ← fetchAddOTarget
|
||||
skipIfNewer extLib oTarget.mtime <|
|
||||
oTarget >> compileStaticLib extLib #[addO]
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue