refactor: merge build target into lake target
This commit is contained in:
tydeu
parent
23dd052dc9
commit
ddf02cb339
6 changed files with 143 additions and 110 deletions
|
|
@ -28,21 +28,21 @@ protected def ModuleArtifact.getMTime (self : ModuleArtifact) : IO MTime := do
|
|||
|
||||
instance : GetMTime ModuleArtifact := ⟨ModuleArtifact.getMTime⟩
|
||||
|
||||
abbrev ModuleTarget := LakeTarget ModuleArtifact
|
||||
abbrev ModuleTarget := ActiveLakeTarget ModuleArtifact
|
||||
|
||||
namespace ModuleTarget
|
||||
|
||||
def oleanFile (self : ModuleTarget) := self.artifact.oleanFile
|
||||
def oleanTarget (self : ModuleTarget) : ActiveFileTarget :=
|
||||
{self with artifact := self.oleanFile, trace := self.mtime}
|
||||
{self with artifact := self.oleanFile}
|
||||
|
||||
def cFile (self : ModuleTarget) := self.artifact.cFile
|
||||
def cTarget (self : ModuleTarget) : ActiveFileTarget :=
|
||||
{self with artifact := self.cFile, trace := self.mtime}
|
||||
{self with artifact := self.cFile}
|
||||
|
||||
end ModuleTarget
|
||||
|
||||
abbrev PackageTarget := LakeTarget (Package × NameMap ModuleTarget)
|
||||
abbrev PackageTarget := ActiveLakeTarget (Package × NameMap ModuleTarget)
|
||||
|
||||
namespace PackageTarget
|
||||
|
||||
|
|
@ -73,16 +73,6 @@ def checkIfSameHash (hash : Hash) (file : FilePath) : IO Bool :=
|
|||
def skipIf [Pure m] [Pure n] (cond : Bool) (build : m (n PUnit)) : m (n PUnit) := do
|
||||
if cond then pure (pure ()) else build
|
||||
|
||||
/--
|
||||
Construct a no-op target if the given artifact is up-to-date.
|
||||
Otherwise, construct a target with the given build task.
|
||||
-/
|
||||
def skipIfNewer [GetMTime a] (artifact : a) (depMTime : MTime)
|
||||
[Pure n] [Monad m] [MonadLiftT IO m] [MonadExceptOf IO.Error m] (build : m (n PUnit))
|
||||
: m (ActiveTarget MTime n a) := do
|
||||
ActiveTarget.mk artifact depMTime <| ←
|
||||
skipIf (← checkIfNewer artifact depMTime) build
|
||||
|
||||
-- # Build Modules
|
||||
|
||||
/-
|
||||
|
|
@ -94,7 +84,7 @@ def skipIfNewer [GetMTime a] (artifact : a) (depMTime : MTime)
|
|||
a `LEAN_PATH` that includes `oleanDirs`.
|
||||
-/
|
||||
def fetchAfterDirectLocalImports
|
||||
(pkg : Package) (oleanDirs : List FilePath) (depsTarget : LakeTarget PUnit)
|
||||
(pkg : Package) (oleanDirs : List FilePath) (depsTarget : ActiveLakeTarget PUnit)
|
||||
{m} [Monad m] [MonadLiftT IO m] [MonadExceptOf IO.Error m] : RecFetch Name ModuleTarget m :=
|
||||
let leanPath := SearchPath.toString <| pkg.oleanDir :: oleanDirs
|
||||
fun mod fetch => do
|
||||
|
|
@ -109,10 +99,10 @@ def fetchAfterDirectLocalImports
|
|||
-- calculate trace
|
||||
let leanMTime ← getMTime leanFile
|
||||
let leanHash := Hash.compute contents
|
||||
let importHashes ← importTargets.map (·.hash)
|
||||
let importMTimes ← importTargets.map (·.mtime)
|
||||
let fullHash := Hash.mixList (leanHash :: depsTarget.hash :: importHashes)
|
||||
let maxMTime := MTime.listMax (leanMTime :: depsTarget.mtime :: importMTimes)
|
||||
let depTrace := depsTarget.trace.mix <|
|
||||
LakeTrace.mixList <| importTargets.map (·.trace)
|
||||
let maxMTime := max leanMTime depTrace.mtime
|
||||
let fullHash := Hash.mix leanHash depTrace.hash
|
||||
let hashFile := pkg.modToHashFile mod
|
||||
let sameHash ← checkIfSameHash fullHash hashFile
|
||||
let mtime := ite sameHash 0 maxMTime
|
||||
|
|
@ -143,18 +133,18 @@ def throwOnCycle (mx : IO (Except (List Name) α)) : IO α :=
|
|||
throw <| IO.userError s!"import cycle detected:\n{"\n".intercalate cycle}"
|
||||
|
||||
def Package.buildModuleTargetDAGFor
|
||||
(mod : Name) (oleanDirs : List FilePath) (depsTarget : LakeTarget PUnit)
|
||||
(mod : Name) (oleanDirs : List FilePath) (depsTarget : ActiveLakeTarget PUnit)
|
||||
(self : Package) : IO (ModuleTarget × NameMap ModuleTarget) := do
|
||||
let fetch := fetchAfterDirectLocalImports self oleanDirs depsTarget
|
||||
throwOnCycle <| buildRBTop fetch mod |>.run {}
|
||||
|
||||
def Package.buildModuleTargetDAG
|
||||
(oleanDirs : List FilePath) (depsTarget : LakeTarget PUnit) (self : Package) :=
|
||||
(oleanDirs : List FilePath) (depsTarget : ActiveLakeTarget PUnit) (self : Package) :=
|
||||
self.buildModuleTargetDAGFor self.moduleRoot oleanDirs depsTarget
|
||||
|
||||
def Package.buildModuleTargets
|
||||
(mods : List Name) (oleanDirs : List FilePath)
|
||||
(depsTarget : LakeTarget PUnit) (self : Package)
|
||||
(depsTarget : ActiveLakeTarget PUnit) (self : Package)
|
||||
: IO (List ModuleTarget) := do
|
||||
let fetch : ModuleTargetFetch :=
|
||||
fetchAfterDirectLocalImports self oleanDirs depsTarget
|
||||
|
|
@ -165,7 +155,7 @@ def Package.buildModuleTargets
|
|||
def Package.buildTargetWithDepTargetsFor
|
||||
(mod : Name) (depTargets : List PackageTarget) (self : Package)
|
||||
: IO PackageTarget := do
|
||||
let depsTarget ← LakeTarget.all <|
|
||||
let depsTarget ← ActiveLakeTarget.all <|
|
||||
(← self.buildMoreDepsTarget).withArtifact arbitrary :: depTargets
|
||||
let oLeanDirs := depTargets.map (·.package.oleanDir)
|
||||
let (target, targetMap) ← self.buildModuleTargetDAGFor mod oLeanDirs depsTarget
|
||||
|
|
@ -212,7 +202,7 @@ def Package.buildModuleTargetsWithDeps
|
|||
(deps : List Package) (mods : List Name) (self : Package)
|
||||
: IO (List ModuleTarget) := do
|
||||
let oleanDirs := deps.map (·.oleanDir)
|
||||
let depsTarget ← LakeTarget.all <|
|
||||
let depsTarget ← ActiveLakeTarget.all <|
|
||||
(← self.buildMoreDepsTarget).withArtifact arbitrary :: (← deps.mapM (·.buildTarget))
|
||||
self.buildModuleTargets mods oleanDirs depsTarget
|
||||
|
||||
|
|
|
|||
|
|
@ -8,15 +8,25 @@ import Lake.Build
|
|||
open System
|
||||
namespace Lake
|
||||
|
||||
/--
|
||||
Construct a no-op target if the given artifact is up-to-date.
|
||||
Otherwise, construct a target with the given build task.
|
||||
-/
|
||||
def skipIfNewer
|
||||
[GetMTime a] (artifact : a) (trace : LakeTrace)
|
||||
(build : IO (IOTask PUnit)) : IO (ActiveLakeTarget a) := do
|
||||
ActiveTarget.mk artifact trace <| ←
|
||||
skipIf (← checkIfNewer artifact trace.mtime) build
|
||||
|
||||
-- # Build `.o` Files
|
||||
|
||||
def buildLeanO (oFile : FilePath)
|
||||
(cTarget : ActiveBuildTarget t FilePath) (leancArgs : Array String := #[]) : IO (IOTask PUnit) :=
|
||||
(cTarget : ActiveFileTarget) (leancArgs : Array String := #[]) : IO (IOTask PUnit) :=
|
||||
cTarget >> compileLeanO oFile cTarget.artifact leancArgs
|
||||
|
||||
def fetchLeanOFileTarget (oFile : FilePath)
|
||||
(cTarget : ActiveFileTarget) (leancArgs : Array String := #[]) : IO ActiveFileTarget :=
|
||||
skipIfNewer oFile cTarget.mtime <| buildLeanO oFile cTarget leancArgs
|
||||
skipIfNewer oFile cTarget.trace <| buildLeanO oFile cTarget leancArgs
|
||||
|
||||
-- # Build Package Lib
|
||||
|
||||
|
|
@ -33,7 +43,7 @@ def PackageTarget.buildStaticLib
|
|||
oFileTargets >> compileStaticLib self.package.staticLibFile oFiles
|
||||
|
||||
def PackageTarget.fetchStaticLibTarget (self : PackageTarget) : IO ActiveFileTarget := do
|
||||
skipIfNewer self.package.staticLibFile self.mtime self.buildStaticLib
|
||||
skipIfNewer self.package.staticLibFile self.trace self.buildStaticLib
|
||||
|
||||
def Package.fetchStaticLibTarget (self : Package) : IO ActiveFileTarget := do
|
||||
(← self.buildTarget).fetchStaticLibTarget
|
||||
|
|
@ -62,7 +72,7 @@ def PackageTarget.buildBin
|
|||
|
||||
def PackageTarget.fetchBinTarget
|
||||
(depTargets : List PackageTarget) (self : PackageTarget) : IO ActiveFileTarget :=
|
||||
skipIfNewer self.package.binFile self.mtime <| self.buildBin depTargets
|
||||
skipIfNewer self.package.binFile self.trace <| self.buildBin depTargets
|
||||
|
||||
def Package.fetchBinTarget (self : Package) : IO ActiveFileTarget := do
|
||||
let depTargets ← self.buildDepTargets
|
||||
|
|
|
|||
|
|
@ -79,36 +79,32 @@ def nil [Pure m] [Inhabited t] : ActiveTarget t m PUnit :=
|
|||
def materialize [Await m n] (self : ActiveTarget t n α) : m PUnit :=
|
||||
await self.task
|
||||
|
||||
def andThen [Monad m] [MonadAsync m n] (target : ActiveTarget t n a) (act : m PUnit) : m (n PUnit) :=
|
||||
mapAsync (fun _ => act) target.task
|
||||
|
||||
instance [Monad m] [MonadAsync m n] : HAndThen (ActiveTarget t n a) (m PUnit) (m (n PUnit)) :=
|
||||
⟨andThen⟩
|
||||
|
||||
end ActiveTarget
|
||||
|
||||
-- ## Active Build Target
|
||||
-- ## Combinators
|
||||
|
||||
abbrev ActiveBuildTarget t a :=
|
||||
ActiveTarget t IOTask a
|
||||
section
|
||||
variable [Monad m] [MonadAsync m n]
|
||||
|
||||
namespace ActiveBuildTarget
|
||||
|
||||
-- ### Combinators
|
||||
|
||||
def after (target : ActiveBuildTarget t a) (act : IO PUnit) : IO (IOTask PUnit) :=
|
||||
target.task.andThen act
|
||||
|
||||
def afterList (targets : List (ActiveBuildTarget t a)) (act : IO PUnit) : IO (IOTask PUnit) :=
|
||||
def afterActiveList (targets : List (ActiveTarget t n a)) (act : m PUnit) : m (n PUnit) :=
|
||||
afterTaskList (targets.map (·.task)) act
|
||||
|
||||
def afterArray (targets : Array (ActiveBuildTarget t a)) (act : IO PUnit) : IO (IOTask PUnit) :=
|
||||
def afterActiveArray (targets : Array (ActiveTarget t n a)) (act : m PUnit) : m (n PUnit) :=
|
||||
afterTaskArray (targets.map (·.task)) act
|
||||
|
||||
instance : HAndThen (ActiveBuildTarget t a) (IO PUnit) (IO (IOTask PUnit)) :=
|
||||
⟨ActiveBuildTarget.after⟩
|
||||
instance : HAndThen (List (ActiveTarget t n a)) (m PUnit) (m (n PUnit)) :=
|
||||
⟨afterActiveList⟩
|
||||
|
||||
instance : HAndThen (List (ActiveBuildTarget t a)) (IO PUnit) (IO (IOTask PUnit)) :=
|
||||
⟨ActiveBuildTarget.afterList⟩
|
||||
instance : HAndThen (Array (ActiveTarget t n a)) (m PUnit) (m (n PUnit)) :=
|
||||
⟨afterActiveArray⟩
|
||||
|
||||
instance : HAndThen (Array (ActiveBuildTarget t a)) (IO PUnit) (IO (IOTask PUnit)) :=
|
||||
⟨ActiveBuildTarget.afterArray⟩
|
||||
|
||||
end ActiveBuildTarget
|
||||
end
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- # Inactive Target
|
||||
|
|
@ -152,36 +148,76 @@ def materializeArrayAsync [Monad m] [Pure n] [MonadAsync m n] (targets : Array (
|
|||
def materializeArray [Monad m] [Pure n] [MonadAsync m n] (targets : Array (Target t m a)) : m PUnit := do
|
||||
await <| ← materializeArrayAsync targets
|
||||
|
||||
def andThen [SeqRight m] (target : Target t m a) (act : m β) : m β :=
|
||||
target.task *> act
|
||||
|
||||
instance [SeqRight m] : HAndThen (Target t m a) (m β) (m β) := ⟨andThen⟩
|
||||
|
||||
end Target
|
||||
|
||||
-- ## BuildTarget
|
||||
--------------------------------------------------------------------------------
|
||||
-- # Build Targets
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
abbrev BuildTarget t a :=
|
||||
Target t IO a
|
||||
-- ## Inactive Target
|
||||
|
||||
abbrev LakeTarget a :=
|
||||
Target LakeTrace IO a
|
||||
|
||||
namespace LakeTarget
|
||||
|
||||
def nil : LakeTarget PUnit :=
|
||||
Target.pure () LakeTrace.nil
|
||||
|
||||
def pure (artifact : a) (hash : Hash) (mtime : MTime) : LakeTarget a :=
|
||||
Target.pure artifact ⟨hash, mtime⟩
|
||||
|
||||
def hash (self : LakeTarget a) := self.trace.hash
|
||||
def mtime (self : LakeTarget a) := self.trace.mtime
|
||||
|
||||
end LakeTarget
|
||||
|
||||
-- ## Active Target
|
||||
|
||||
abbrev ActiveLakeTarget a :=
|
||||
ActiveTarget LakeTrace IOTask a
|
||||
|
||||
namespace ActiveLakeTarget
|
||||
|
||||
def nil : ActiveLakeTarget PUnit :=
|
||||
ActiveTarget.pure () LakeTrace.nil
|
||||
|
||||
def hash (self : ActiveLakeTarget a) := self.trace.hash
|
||||
def mtime (self : ActiveLakeTarget a) := self.trace.mtime
|
||||
|
||||
def all (targets : List (ActiveLakeTarget a)) : IO (ActiveLakeTarget PUnit) := do
|
||||
let hash := Hash.mixList <| targets.map (·.hash)
|
||||
let mtime := MTime.listMax <| targets.map (·.mtime)
|
||||
let task ← seqListAsync <| targets.map (·.task)
|
||||
return ActiveTarget.mk () ⟨hash, mtime⟩ task
|
||||
|
||||
end ActiveLakeTarget
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- # File Targets
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
-- ## File BaseTarget
|
||||
-- ## File Target
|
||||
|
||||
abbrev FileTarget :=
|
||||
BuildTarget MTime FilePath
|
||||
LakeTarget FilePath
|
||||
|
||||
namespace FileTarget
|
||||
|
||||
def mk (file : FilePath) (depMTime : MTime) (task : IO PUnit) : FileTarget :=
|
||||
⟨file, depMTime, task⟩
|
||||
|
||||
def compute (file : FilePath) : IO FileTarget := do
|
||||
Target.pure file (← getMTime file)
|
||||
Target.pure file <| ← LakeTrace.compute file
|
||||
|
||||
end FileTarget
|
||||
|
||||
-- ## Files BaseTarget
|
||||
-- ## Files Target
|
||||
|
||||
abbrev FilesTarget :=
|
||||
BuildTarget MTime (Array FilePath)
|
||||
LakeTarget (Array FilePath)
|
||||
|
||||
namespace FilesTarget
|
||||
|
||||
|
|
@ -195,20 +231,20 @@ def filesAsArray (self : FilesTarget) : Array FilePath :=
|
|||
self.artifact
|
||||
|
||||
def compute (files : Array FilePath) : IO FilesTarget := do
|
||||
Target.pure files (MTime.arrayMax <| ← files.mapM getMTime)
|
||||
Target.pure files <| LakeTrace.mixArray <| ← files.mapM LakeTrace.compute
|
||||
|
||||
def singleton (target : FileTarget) : FilesTarget :=
|
||||
target.withArtifact #[target.file]
|
||||
|
||||
def collectList (targets : List FileTarget) : FilesTarget :=
|
||||
let files := Array.mk <| targets.map (·.file)
|
||||
let mtime := MTime.listMax <| targets.map (·.mtime)
|
||||
Target.mk files mtime do Target.materializeList targets
|
||||
let trace := LakeTrace.mixList <| targets.map (·.trace)
|
||||
Target.mk files trace do Target.materializeList targets
|
||||
|
||||
def collectArray (targets : Array FileTarget) : FilesTarget :=
|
||||
let files := targets.map (·.file)
|
||||
let mtime := MTime.arrayMax <| targets.map (·.mtime)
|
||||
Target.mk files mtime do Target.materializeArray targets
|
||||
let trace := LakeTrace.mixArray <| targets.map (·.trace)
|
||||
Target.mk files trace do Target.materializeArray targets
|
||||
|
||||
def collect (targets : Array FileTarget) : FilesTarget :=
|
||||
collectArray targets
|
||||
|
|
@ -222,40 +258,4 @@ instance : Coe (Array FileTarget) FilesTarget := ⟨FilesTarget.collectArray⟩
|
|||
-- ## Active File Target
|
||||
|
||||
abbrev ActiveFileTarget :=
|
||||
ActiveBuildTarget MTime FilePath
|
||||
|
||||
namespace ActiveFileTarget
|
||||
|
||||
def mk (file : FilePath) (depMTime : MTime) (task : IOTask PUnit) : ActiveFileTarget :=
|
||||
ActiveTarget.mk file depMTime task
|
||||
|
||||
end ActiveFileTarget
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- # Lake Target
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
abbrev LakeTarget a :=
|
||||
ActiveBuildTarget LakeTrace a
|
||||
|
||||
namespace LakeTarget
|
||||
|
||||
def nil : LakeTarget PUnit :=
|
||||
ActiveTarget.pure () Inhabited.default
|
||||
|
||||
def hash (self : LakeTarget a) := self.trace.hash
|
||||
def mtime (self : LakeTarget a) := self.trace.mtime
|
||||
|
||||
def all (targets : List (LakeTarget a)) : IO (LakeTarget PUnit) := do
|
||||
let hash := Hash.mixList <| targets.map (·.hash)
|
||||
let mtime := MTime.listMax <| targets.map (·.mtime)
|
||||
let task ← seqListAsync <| targets.map (·.task)
|
||||
return ActiveTarget.mk () ⟨hash, mtime⟩ task
|
||||
|
||||
def fromMTimeTarget (target : ActiveBuildTarget MTime a) : LakeTarget a :=
|
||||
{target with trace := LakeTrace.fromMTime target.trace}
|
||||
|
||||
def buildOpaqueFromFileTarget (target : FileTarget) : IO (LakeTarget PUnit) := do
|
||||
LakeTarget.fromMTimeTarget <| ← Target.runAsync target.withoutArtifact
|
||||
|
||||
end LakeTarget
|
||||
ActiveLakeTarget FilePath
|
||||
|
|
|
|||
|
|
@ -12,14 +12,14 @@ namespace Lake
|
|||
def oFileTarget
|
||||
(oFile : FilePath) (srcTarget : FileTarget)
|
||||
(args : Array String := #[]) (cmd := "c++") : FileTarget :=
|
||||
FileTarget.mk oFile srcTarget.trace <|
|
||||
Target.mk oFile srcTarget.trace <|
|
||||
unless (← checkIfNewer oFile srcTarget.mtime) do
|
||||
srcTarget.materialize
|
||||
compileO oFile srcTarget.file args (cmd := "c++")
|
||||
|
||||
def staticLibTarget
|
||||
(libFile : FilePath) (oFilesTarget : FilesTarget) : FileTarget :=
|
||||
FileTarget.mk libFile oFilesTarget.trace do
|
||||
Target.mk libFile oFilesTarget.trace do
|
||||
unless (← checkIfNewer libFile oFilesTarget.mtime) do
|
||||
oFilesTarget.materialize
|
||||
compileStaticLib libFile oFilesTarget.filesAsArray
|
||||
|
|
|
|||
|
|
@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Mac Malone
|
||||
-/
|
||||
|
||||
open System
|
||||
namespace Lake
|
||||
|
||||
-- # Hash Traces
|
||||
|
|
@ -28,6 +29,9 @@ def mix (h1 h2 : Hash) : Hash :=
|
|||
def mixList (hashes : List Hash) : Hash :=
|
||||
hashes.foldl mix nil
|
||||
|
||||
def mixArray (hashes : Array Hash) : Hash :=
|
||||
hashes.foldl mix nil
|
||||
|
||||
protected def toString (self : Hash) : String :=
|
||||
toString self.val
|
||||
|
||||
|
|
@ -35,6 +39,17 @@ instance : ToString Hash := ⟨Hash.toString⟩
|
|||
|
||||
end Hash
|
||||
|
||||
class ComputeHash (α) where
|
||||
computeHash : α → IO Hash
|
||||
|
||||
export ComputeHash (computeHash)
|
||||
|
||||
def getFileHash (file : FilePath) : IO Hash :=
|
||||
Hash.compute <$> IO.FS.readFile file
|
||||
|
||||
instance : ComputeHash FilePath := ⟨getFileHash⟩
|
||||
instance : ComputeHash String := ⟨pure ∘ Hash.compute⟩
|
||||
|
||||
-- # Modification Time Traces
|
||||
|
||||
open IO.FS (SystemTime)
|
||||
|
|
@ -61,8 +76,10 @@ class GetMTime (α) where
|
|||
|
||||
export GetMTime (getMTime)
|
||||
|
||||
instance : GetMTime System.FilePath where
|
||||
getMTime file := do (← file.metadata).modified
|
||||
def getFileMTime (file : FilePath) : IO MTime := do
|
||||
(← file.metadata).modified
|
||||
|
||||
instance : GetMTime FilePath := ⟨getFileMTime⟩
|
||||
|
||||
/-- Check if the artifact's `MTIme` is at least `depMTime`. -/
|
||||
def checkIfNewer [GetMTime a] (artifact : a) (depMTime : MTime) : IO Bool := do
|
||||
|
|
@ -73,14 +90,30 @@ def checkIfNewer [GetMTime a] (artifact : a) (depMTime : MTime) : IO Bool := do
|
|||
structure LakeTrace where
|
||||
hash : Hash
|
||||
mtime : MTime
|
||||
deriving Inhabited
|
||||
|
||||
namespace LakeTrace
|
||||
|
||||
def nil : LakeTrace :=
|
||||
mk Hash.nil 0
|
||||
|
||||
instance : Inhabited LakeTrace := ⟨nil⟩
|
||||
|
||||
def compute [ComputeHash a] [GetMTime a] (artifact : a) : IO LakeTrace := do
|
||||
mk (← computeHash artifact) (← getMTime artifact)
|
||||
|
||||
def fromHash (hash : Hash) : LakeTrace :=
|
||||
LakeTrace.mk hash 0
|
||||
mk hash 0
|
||||
|
||||
def fromMTime (mtime : MTime) : LakeTrace :=
|
||||
LakeTrace.mk Hash.nil mtime
|
||||
mk Hash.nil mtime
|
||||
|
||||
def mix (t1 t2 : LakeTrace) : LakeTrace :=
|
||||
mk (Hash.mix t1.hash t2.hash) (max t1.mtime t2.mtime)
|
||||
|
||||
def mixList (traces : List LakeTrace) : LakeTrace :=
|
||||
traces.foldl mix nil
|
||||
|
||||
def mixArray (traces : Array LakeTrace) : LakeTrace :=
|
||||
traces.foldl mix nil
|
||||
|
||||
end LakeTrace
|
||||
|
|
|
|||
|
|
@ -52,7 +52,7 @@ structure PackageConfig where
|
|||
buildMoreLibTargets : IO (Array ActiveFileTarget) := #[]
|
||||
depsDir : FilePath := defaultDepsDir
|
||||
dependencies : List Dependency := []
|
||||
buildMoreDepsTarget : IO (LakeTarget PUnit) := LakeTarget.nil
|
||||
buildMoreDepsTarget : IO (ActiveLakeTarget PUnit) := ActiveLakeTarget.nil
|
||||
scripts : HashMap String Script := HashMap.empty
|
||||
deriving Inhabited
|
||||
|
||||
|
|
@ -86,7 +86,7 @@ def moduleRootName (self : Package) : String :=
|
|||
def dependencies (self : Package) : List Dependency :=
|
||||
self.config.dependencies
|
||||
|
||||
def buildMoreDepsTarget (self : Package) : IO (LakeTarget PUnit) :=
|
||||
def buildMoreDepsTarget (self : Package) : IO (ActiveLakeTarget PUnit) :=
|
||||
self.config.buildMoreDepsTarget
|
||||
|
||||
def leanArgs (self : Package) : Array String :=
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue