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
This commit is contained in:
Mac Malone 2025-11-17 17:27:19 -05:00 committed by GitHub
parent 033fa8c585
commit 81d716069c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 4 additions and 3 deletions

View file

@ -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

View file

@ -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