feat: add inputFileTarget util

Lake/BuildTarget.lean

@@ -40,8 +40,6 @@ def computeAsync (path : FilePath) : FileTarget :=
   Target.mk path do async <| try liftM <| computeTrace path catch e =>
     BuildM.logError (toString e); throw e
 
-instance : Coe FilePath FileTarget := ⟨computeAsync⟩
-
 end FileTarget
 
 -- ## Active

Lake/BuildTargets.lean

@@ -11,6 +11,9 @@ namespace Lake
 
 -- # General Utilities
 
+def inputFileTarget := FileTarget.computeAsync
+instance : Coe FilePath FileTarget := ⟨inputFileTarget⟩
+
 def buildFileUnlessUpToDate (file : FilePath)
 (trace : BuildTrace) (build : BuildM PUnit) : BuildM BuildTrace := do
   let traceFile := FilePath.mk <| file.toString ++ ".trace"

examples/ffi/lakefile.lean

@@ -7,7 +7,7 @@ def buildDir := defaultBuildDir
 
 def ffiOTarget (pkgDir : FilePath) : FileTarget :=
   let oFile := pkgDir / buildDir / cDir / "ffi.o"
-  let srcTarget : FileTarget := coe <| pkgDir / ffiSrc
+  let srcTarget := inputFileTarget <| pkgDir / ffiSrc
   fileTargetWithDep oFile srcTarget fun srcFile => do
     compileO oFile srcFile #["-I", (← getLeanIncludeDir).toString]