refactor: remove FilesTarget

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

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

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"