max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix typo in checkArtifactsExist (#13277)

Browse source 
This PR fixes a public-facing typo in a function name:
`Module.checkArtifactsExsist` -> `Module.checkArtifactsExist`.
This commit is contained in:
Jason Yuen 2026-04-04 11:56:10 -07:00 • committed by GitHub
parent 681856324f
commit 9efba691e7
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/lake/Lake/Build/Module.lean
View file

@ -705,7 +705,7 @@ private def Module.restoreAllArtifacts (mod : Module) (cached : ModuleOutputArti
where
@[inline] restoreSome file art? := art?.mapM (restoreArtifact file ·)
public def Module.checkArtifactsExsist (self : Module) (isModule : Bool) : BaseIO Bool := do
public def Module.checkArtifactsExist (self : Module) (isModule : Bool) : BaseIO Bool := do
unless (← self.oleanFile.pathExists) do return false
unless (← self.ileanFile.pathExists) do return false
unless (← self.cFile.pathExists) do return false
@ -718,7 +718,7 @@ public def Module.checkArtifactsExsist (self : Module) (isModule : Bool) : BaseI
return true
public protected def Module.checkExists (self : Module) (isModule : Bool) : BaseIO Bool := do
self.ltarFile.pathExists <||> self.checkArtifactsExsist isModule
self.ltarFile.pathExists <||> self.checkArtifactsExist isModule
@[deprecated Module.checkExists (since := "2025-03-04")]
public instance : CheckExists Module := ⟨Module.checkExists (isModule := false)⟩
@ -788,7 +788,7 @@ instance : ToOutputJson ModuleOutputArtifacts := ⟨(toJson ·.descrs)⟩
def Module.packLtar (self : Module) (arts : ModuleOutputArtifacts) : JobM Artifact := do
let arts ← id do
if (← self.checkArtifactsExsist arts.isModule) then
if (← self.checkArtifactsExist arts.isModule) then
return arts
else self.restoreAllArtifacts arts
let args ← id do
@ -941,7 +941,7 @@ where
| .inr savedTrace =>
let status ← savedTrace.replayIfUpToDate' (oldTrace := srcTrace.mtime) mod depTrace
if status.isUpToDate then
unless (← mod.checkArtifactsExsist setup.isModule) do
unless (← mod.checkArtifactsExist setup.isModule) do
mod.unpackLtar mod.ltarFile
else
discard <| mod.buildLean depTrace srcFile setup
@ -953,7 +953,7 @@ where
mod.computeArtifacts setup.isModule
else
if (← savedTrace.replayIfUpToDate (oldTrace := srcTrace.mtime) mod depTrace) then
unless (← mod.checkArtifactsExsist setup.isModule) do
unless (← mod.checkArtifactsExist setup.isModule) do
mod.unpackLtar mod.ltarFile
mod.computeArtifacts setup.isModule
else