From 4dbe84dc987d2acaf310be724735940d4cfffefd Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 22 Jul 2025 19:34:41 +0200 Subject: [PATCH] chore: ensure Lake and Lean agree when `.ir` is needed (#9471) --- src/Lean/Environment.lean | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index cf265a57a4..27117d0d6e 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -1908,10 +1908,13 @@ private def ImportedModule.loadIRData? (self : ImportedModule) (arts : NameMap M IO (Option (ModuleData × Option CompactedRegion)) := do if (level < .server && self.irPhases == .runtime) || !self.mainModule?.any (·.isModule) then return self.mainModule?.map (·, none) - let fname ← - arts.find? self.module |>.bind (·.ir?) |>.getDM do + let fname ← match arts.find? self.module with + | some { ir? := some ir } => pure ir + -- If Lake tells us we don't need IR, we should not look for it ourselves + | some _ => return none + | none => do let mFile ← findOLean self.module - return mFile.withExtension "ir" + pure <| mFile.withExtension "ir" let (data, region) ← readModuleData fname return some (data, some region)