Skip to content

Commit 13b9985

Browse files
tydeukim-em
authored andcommitted
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
1 parent 91db6ab commit 13b9985

File tree

2 files changed

+4
-3
lines changed

2 files changed

+4
-3
lines changed

src/lake/Lake/Build/Common.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -604,7 +604,7 @@ public def buildArtifactUnlessUpToDate
604604
else
605605
computeArtifact file ext text
606606
else if (← savedTrace.replayIfUpToDate file depTrace) then
607-
computeArtifact file ext
607+
computeArtifact file ext text
608608
else if let some art ← fetchArt? (restore := true) then
609609
return art
610610
else
@@ -627,7 +627,7 @@ where
627627
build
628628
clearFileHash file
629629
removeFileIfExists traceFile
630-
computeArtifact file ext
630+
computeArtifact file ext text
631631

632632
/--
633633
Build `file` using `build` after `dep` completes if the dependency's

src/lake/Lake/Build/Module.lean

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -635,7 +635,8 @@ private def Module.computeArtifacts (mod : Module) (isModule : Bool) : FetchM Mo
635635
}
636636
where
637637
@[inline] compute file ext := do
638-
computeArtifact file ext
638+
-- Note: Lean produces LF-only line endings for `.c` and `.ilean`, so no normalization.
639+
computeArtifact file ext (text := false)
639640
computeIf c file ext := do
640641
if c then return some (← compute file ext) else return none
641642

0 commit comments

Comments
 (0)