From 81d716069c354fe5f6f1e36ab731ff54b2b42e55 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Mon, 17 Nov 2025 17:27:19 -0500 Subject: [PATCH] fix: lake: improper uses of `computeArtifact` w/o `text` (#11216) This PR ensures that the `text` argument of `computeArtifact` is always provided in Lake code, fixing a hashing bug with `buildArtifactUnlessUpToDate` in the process. Closes #11209 --- src/lake/Lake/Build/Common.lean | 4 ++-- src/lake/Lake/Build/Module.lean | 3 ++- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/src/lake/Lake/Build/Common.lean b/src/lake/Lake/Build/Common.lean index daf256e810..264291101a 100644 --- a/src/lake/Lake/Build/Common.lean +++ b/src/lake/Lake/Build/Common.lean @@ -604,7 +604,7 @@ public def buildArtifactUnlessUpToDate else computeArtifact file ext text else if (← savedTrace.replayIfUpToDate file depTrace) then - computeArtifact file ext + computeArtifact file ext text else if let some art ← fetchArt? (restore := true) then return art else @@ -627,7 +627,7 @@ where build clearFileHash file removeFileIfExists traceFile - computeArtifact file ext + computeArtifact file ext text /-- Build `file` using `build` after `dep` completes if the dependency's diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean index 6632019f29..ee93fd8fd0 100644 --- a/src/lake/Lake/Build/Module.lean +++ b/src/lake/Lake/Build/Module.lean @@ -635,7 +635,8 @@ private def Module.computeArtifacts (mod : Module) (isModule : Bool) : FetchM Mo } where @[inline] compute file ext := do - computeArtifact file ext + -- Note: Lean produces LF-only line endings for `.c` and `.ilean`, so no normalization. + computeArtifact file ext (text := false) computeIf c file ext := do if c then return some (← compute file ext) else return none