fix: keep findOLean's root cache valid across withImportModules

src/Lean/Util/Path.lean

@@ -130,6 +130,9 @@ invalidates the cache.
 `findOLean` is not called concurrently by Lean itself. If a client does so, calls may overwrite
 each other's entries, so some packages are probed again; every stored root was resolved against
 the search path stored next to it, so results are unaffected.
+
+The keys are deep copies of the package names: a name read from an import list lives in that
+`.olean`'s region, which `withImportModules` frees after use.
 -/
 private builtin_initialize oleanRootCacheRef : IO.Ref (SearchPath × List (Name × FilePath)) ←
   IO.mkRef ([], [])
@@ -143,7 +146,7 @@ partial def findOLean (mod : Name) : IO FilePath := do
   if let some root := cache.lookup pkg then
     return modToFilePath root mod "olean"
   if let some root ← sp.findRootWithExt "olean" mod then
-    oleanRootCacheRef.set (sp, (pkg, root) :: cache)
+    oleanRootCacheRef.set (sp, (← Runtime.deepCopy pkg, root) :: cache)
     return modToFilePath root mod "olean"
   else
     let pkg := FilePath.mk <| mod.getRoot.toString (escape := false)

tests/elab/issue16267.lean

@@ -0,0 +1,22 @@
+import Lean.Environment
+open Lean
+
+/-!
+Regression test for #16267: `findOLean`'s package root cache must not keep names that live in the
+`.olean` regions freed by `withImportModules`.
+-/
+
+unsafe def importTwice : IO Unit := do
+  -- A new search path empties the cache, so the roots cached during the first import (`Init`,
+  -- reached through `Lean.Data.Json`'s imports) are names from the regions freed afterwards.
+  searchPathRef.modify (· ++ [System.FilePath.mk "_tmp_issue16267"])
+  for i in [0:2] do
+    withImportModules #[{ module := `Lean.Data.Json }] {} fun env =>
+      IO.println s!"import {i}: {(env.find? `Lean.Json.compress).isSome}"
+
+/--
+info: import 0: true
+import 1: true
+-/
+#guard_msgs in
+#eval importTwice