diff --git a/src/Lean/Util/Path.lean b/src/Lean/Util/Path.lean index cccecd7d360d..4800ee406865 100644 --- a/src/Lean/Util/Path.lean +++ b/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) diff --git a/tests/elab/issue16267.lean b/tests/elab/issue16267.lean new file mode 100644 index 000000000000..13998bef612c --- /dev/null +++ b/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