chore: ensure Lake and Lean agree when .ir is needed (#9471)

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)