diff --git a/Lake/BuildTargets.lean b/Lake/BuildTargets.lean index 5816fcbcdd..ad535ef99a 100644 --- a/Lake/BuildTargets.lean +++ b/Lake/BuildTargets.lean @@ -14,12 +14,13 @@ def oFileTarget (args : Array String := #[]) (cmd := "c++") : FileTarget := Target.mk oFile srcTarget.trace <| unless (← checkIfNewer oFile srcTarget.mtime) do - srcTarget.materialize - compileO oFile srcTarget.file args (cmd := "c++") + srcTarget >> compileO oFile srcTarget.file args cmd def staticLibTarget -(libFile : FilePath) (oFilesTarget : FilesTarget) : FileTarget := - Target.mk libFile oFilesTarget.trace do - unless (← checkIfNewer libFile oFilesTarget.mtime) do - oFilesTarget.materialize - compileStaticLib libFile oFilesTarget.filesAsArray +(libFile : FilePath) (oFileTargets : Array FileTarget) : FileTarget := + let linkFiles := oFileTargets.map (·.artifact) + let trace := mixTraceArray <| oFileTargets.map (·.trace) + Target.mk libFile trace do + unless (← checkIfNewer libFile trace.mtime) do + Target.materializeArray oFileTargets + compileStaticLib libFile linkFiles diff --git a/Lake/Target.lean b/Lake/Target.lean index 46a2d2c85c..705fdc5f9b 100644 --- a/Lake/Target.lean +++ b/Lake/Target.lean @@ -219,47 +219,6 @@ def compute (file : FilePath) : IO FileTarget := end FileTarget --- ## Files Target - -abbrev FilesTarget := - LakeTarget (Array FilePath) - -namespace FilesTarget - -def files (self : FilesTarget) : Array FilePath := - self.artifact - -def filesAsList (self : FilesTarget) : List FilePath := - self.artifact.toList - -def filesAsArray (self : FilesTarget) : Array FilePath := - self.artifact - -def compute (files : Array FilePath) : IO FilesTarget := - Target.compute files - -def singleton (target : FileTarget) : FilesTarget := - target.withArtifact #[target.file] - -def collectList (targets : List FileTarget) : FilesTarget := - let files := Array.mk <| targets.map (·.file) - let trace := mixTraceList <| targets.map (·.trace) - Target.mk files trace do Target.materializeList targets - -def collectArray (targets : Array FileTarget) : FilesTarget := - let files := targets.map (·.file) - let trace := mixTraceArray <| targets.map (·.trace) - Target.mk files trace do Target.materializeArray targets - -def collect (targets : Array FileTarget) : FilesTarget := - collectArray targets - -end FilesTarget - -instance : Coe FileTarget FilesTarget := ⟨FilesTarget.singleton⟩ -instance : Coe (List FileTarget) FilesTarget := ⟨FilesTarget.collectList⟩ -instance : Coe (Array FileTarget) FilesTarget := ⟨FilesTarget.collectArray⟩ - -- ## Active File Target abbrev ActiveFileTarget := diff --git a/examples/ffi/package.lean b/examples/ffi/package.lean index d17fc5607c..f4bb08370c 100644 --- a/examples/ffi/package.lean +++ b/examples/ffi/package.lean @@ -14,7 +14,7 @@ def computeAddOTarget : IO FileTarget := do oFileTarget addO <| ← FileTarget.compute addSrc def computeCLibTarget : IO FileTarget := do - staticLibTarget cLib <| ← computeAddOTarget + staticLibTarget cLib #[← computeAddOTarget] def package : PackageConfig := { name := "ffi"