From 748eab95113febbf8fa062643d06af3db49e0a1f Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Fri, 7 Jun 2024 21:20:46 -0400
Subject: [PATCH] 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         | 22 ++++++++++++++++++++--
 src/lake/examples/ffi/lib/lakefile.lean |  2 +-
 src/lake/examples/targets/lakefile.lean |  2 +-
 3 files changed, 22 insertions(+), 4 deletions(-)

diff --git a/src/lake/Lake/Build/Common.lean b/src/lake/Lake/Build/Common.lean
index 71f1ce9947..6cbbf95400 100644
--- a/src/lake/Lake/Build/Common.lean
+++ b/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:
 
diff --git a/src/lake/examples/ffi/lib/lakefile.lean b/src/lake/examples/ffi/lib/lakefile.lean
index 4dd9f97653..7191a47304 100644
--- a/src/lake/examples/ffi/lib/lakefile.lean
+++ b/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
 
diff --git a/src/lake/examples/targets/lakefile.lean b/src/lake/examples/targets/lakefile.lean
index e069fe4bb0..432e9aa36c 100644
--- a/src/lake/examples/targets/lakefile.lean
+++ b/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