refactor: lake: inputBinFile / inputTextFile (#4384)

Deprecates `inputFile` and replaces it with `inputBinFile` and
`inputTextFile`. `inputTextFile` normalizes line endings, which helps
ensure text file traces are platform-independent.

src/lake/Lake/Build/Common.lean

@@ -182,10 +182,28 @@ trace (and/or `extraDepTrace`) has changed.
 
 /-! ## Common Builds -/
 
-/-- A build job for file that is expected to already exist (e.g., a source file). -/
-def inputFile (path : FilePath) : SpawnM (BuildJob FilePath) :=
+/--
+A build job for binary file that is expected to already exist (e.g., a data blob).
+Any byte difference in the file will trigger a rebuild of dependents.
+-/
+def inputBinFile (path : FilePath) : SpawnM (BuildJob FilePath) :=
   Job.async <| (path, ·) <$> computeTrace path
 
+/--
+A build job for text file that is expected to already exist (e.g., a source file).
+Normalizes line endings (converts CRLF to LF) to produce platform-independent traces.
+-/
+def inputTextFile (path : FilePath) : SpawnM (BuildJob FilePath) :=
+  Job.async <| (path, ·) <$> computeTrace (TextFilePath.mk path)
+
+/--
+A build job for file that is expected to already exist.
+
+**Deprecated:** Use either `inputTextFile` or `inputBinFile`.
+`inputTextFile` normalizes line endings to produce platform-independent traces.
+-/
+@[deprecated] abbrev inputFile := @inputBinFile
+
 /--
 Build an object file from a source file job using `compiler`. The invocation is:
 

src/lake/examples/ffi/lib/lakefile.lean

@@ -13,7 +13,7 @@ lean_lib FFI
 
 target ffi.o pkg : FilePath := do
   let oFile := pkg.buildDir / "c" / "ffi.o"
-  let srcJob ← inputFile <| pkg.dir / "c" / "ffi.cpp"
+  let srcJob ← inputTextFile <| pkg.dir / "c" / "ffi.cpp"
   let weakArgs := #["-I", (← getLeanIncludeDir).toString]
   buildO oFile srcJob weakArgs #["-fPIC"] "c++" getLeanTrace
 

src/lake/examples/targets/lakefile.lean

@@ -41,7 +41,7 @@ package_facet print_name pkg : Unit := Job.async do
   return ((), .nil)
 
 module_facet get_src mod : FilePath := do
-  inputFile mod.leanFile
+  inputTextFile mod.leanFile
 
 module_facet print_src mod : Unit := do
   (← fetch <| mod.facet `get_src).bindSync fun src trace => do