From 427cb0fc7caafaa30abc79198c2f32c544fbf266 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Fri, 8 Oct 2021 15:26:07 -0400
Subject: [PATCH] feat: add `inputFileTarget` util

---
 Lake/BuildTarget.lean      | 2 --
 Lake/BuildTargets.lean     | 3 +++
 examples/ffi/lakefile.lean | 2 +-
 3 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/Lake/BuildTarget.lean b/Lake/BuildTarget.lean
index b239c6fc15..f33f37cff0 100644
--- a/Lake/BuildTarget.lean
+++ b/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
diff --git a/Lake/BuildTargets.lean b/Lake/BuildTargets.lean
index 8c65c61c37..370ba7feba 100644
--- a/Lake/BuildTargets.lean
+++ b/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"
diff --git a/examples/ffi/lakefile.lean b/examples/ffi/lakefile.lean
index f1f8a174b4..6c40bf11cc 100644
--- a/examples/ffi/lakefile.lean
+++ b/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]