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