fix: Thread unique name generator through library_search init

src/Lean/Meta/LazyDiscrTree.lean

@@ -700,35 +700,42 @@ private structure ImportFailure where
 
 /-- Information generation from imported modules. -/
 private structure ImportData where
-  cache : IO.Ref (Lean.Meta.Cache)
   errors : IO.Ref (Array ImportFailure)
 
 private def ImportData.new : BaseIO ImportData := do
-  let cache ← IO.mkRef {}
   let errors ← IO.mkRef #[]
-  pure { cache, errors }
+  pure { errors }
+
+structure Cache where
+  ngen : NameGenerator
+  core : Lean.Core.Cache
+  meta : Lean.Meta.Cache
+
+def Cache.empty (ngen : NameGenerator) : Cache := { ngen := ngen, core := {}, meta := {} }
 
 private def addConstImportData
     (env : Environment)
     (modName : Name)
     (d : ImportData)
+    (cacheRef : IO.Ref Cache)
     (tree : PreDiscrTree α)
     (act : Name → ConstantInfo → MetaM (Array (InitEntry α)))
     (name : Name) (constInfo : ConstantInfo) : BaseIO (PreDiscrTree α) := do
   if constInfo.isUnsafe then return tree
   if !allowCompletion env name then return tree
-  let mstate : Meta.State := { cache := ←d.cache.get }
-  d.cache.set {}
+  let { ngen, core := core_cache, meta := meta_cache } ← cacheRef.get
+  let mstate : Meta.State := { cache := meta_cache }
+  cacheRef.set (Cache.empty ngen)
   let ctx : Meta.Context := { config := { transparency := .reducible } }
   let cm := (act name constInfo).run ctx mstate
   let cctx : Core.Context := {
     fileName := default,
     fileMap := default
   }
-  let cstate : Core.State := {env}
+  let cstate : Core.State := {env, cache := core_cache, ngen}
   match ←(cm.run cctx cstate).toBaseIO with
-  | .ok ((a, ms), _) =>
-    d.cache.set ms.cache
+  | .ok ((a, ms), cs) =>
+    cacheRef.set { ngen := cs.ngen, core := cs.cache, meta := ms.cache }
     pure <| a.foldl (fun t e => t.push e.key e.entry) tree
   | .error e =>
     let i : ImportFailure := {
@@ -771,6 +778,7 @@ private def toFlat (d : ImportData) (tree : PreDiscrTree α) :
 private partial def loadImportedModule (env : Environment)
     (act : Name → ConstantInfo → MetaM (Array (InitEntry α)))
     (d : ImportData)
+    (cacheRef : IO.Ref Cache)
     (tree : PreDiscrTree α)
     (mname : Name)
     (mdata : ModuleData)
@@ -778,21 +786,22 @@ private partial def loadImportedModule (env : Environment)
   if h : i < mdata.constNames.size then
     let name := mdata.constNames[i]
     let constInfo  := mdata.constants[i]!
-    let tree ← addConstImportData env mname d tree act name constInfo
-    loadImportedModule env act d tree mname mdata (i+1)
+    let tree ← addConstImportData env mname d cacheRef tree act name constInfo
+    loadImportedModule env act d cacheRef tree mname mdata (i+1)
   else
     pure tree
 
-private def createImportedEnvironmentSeq (env : Environment)
+private def createImportedEnvironmentSeq (ngen : NameGenerator) (env : Environment)
     (act : Name → ConstantInfo → MetaM (Array (InitEntry α)))
-    (start stop : Nat) : BaseIO (InitResults α) :=
-      do go (← ImportData.new) {} start stop
-    where go d (tree : PreDiscrTree α) (start stop : Nat) : BaseIO _ := do
+    (start stop : Nat) : BaseIO (InitResults α) := do
+      let cacheRef ← IO.mkRef (Cache.empty ngen)
+      go (← ImportData.new) cacheRef {} start stop
+    where go d cacheRef (tree : PreDiscrTree α) (start stop : Nat) : BaseIO _ := do
             if start < stop then
               let mname := env.header.moduleNames[start]!
               let mdata := env.header.moduleData[start]!
-              let tree ← loadImportedModule env act d tree mname mdata
-              go d tree (start+1) stop
+              let tree ← loadImportedModule env act d cacheRef tree mname mdata
+              go d cacheRef tree (start+1) stop
             else
               toFlat d tree
     termination_by stop - start
@@ -802,29 +811,31 @@ private def combineGet [Append α] (z : α) (tasks : Array (Task α)) : α :=
   tasks.foldl (fun x t => x ++ t.get) (init := z)
 
 /-- Create an imported environment for tree. -/
-def createImportedEnvironment (env : Environment)
+def createImportedEnvironment (ngen : NameGenerator) (env : Environment)
     (act : Name → ConstantInfo → MetaM (Array (InitEntry α)))
     (constantsPerTask : Nat := 1000) :
     EIO Exception (LazyDiscrTree α) := do
   let n := env.header.moduleData.size
   let rec
     /-- Allocate constants to tasks according to `constantsPerTask`. -/
-    go tasks start cnt idx := do
+    go ngen tasks start cnt idx := do
       if h : idx < env.header.moduleData.size then
         let mdata := env.header.moduleData[idx]
         let cnt := cnt + mdata.constants.size
         if cnt > constantsPerTask then
-          let t ← createImportedEnvironmentSeq env act start (idx+1) |>.asTask
-          go (tasks.push t) (idx+1) 0 (idx+1)
+          let (childNGen, ngen) := ngen.mkChild
+          let t ← createImportedEnvironmentSeq childNGen env act start (idx+1) |>.asTask
+          go ngen (tasks.push t) (idx+1) 0 (idx+1)
         else
-          go tasks start cnt (idx+1)
+          go ngen tasks start cnt (idx+1)
       else
         if start < n then
-          tasks.push <$> (createImportedEnvironmentSeq env act start n).asTask
+          let (childNGen, _) := ngen.mkChild
+          tasks.push <$> (createImportedEnvironmentSeq childNGen env act start n).asTask
         else
           pure tasks
     termination_by env.header.moduleData.size - idx
-  let tasks ← go #[] 0 0 0
+  let tasks ← go ngen #[] 0 0 0
   let r := combineGet default tasks
   if p : r.errors.size > 0 then
     throw r.errors[0].exception

src/Lean/Meta/Tactic/LibrarySearch.lean

@@ -150,9 +150,12 @@ Candidate-finding function that uses a strict discrimination tree for resolution
 def mkImportFinder : IO CandidateFinder := do
   let ref ← IO.mkRef none
   pure fun ty => do
+    let ngen ← getNGen
+    let (childNGen, ngen) := ngen.mkChild
+    setNGen ngen
     let importTree ← (←ref.get).getDM $ do
       profileitM Exception  "librarySearch launch" (←getOptions) $
-        createImportedEnvironment (←getEnv) (constantsPerTask := constantsPerTask) addImport
+        createImportedEnvironment childNGen (←getEnv) (constantsPerTask := constantsPerTask) addImport
     let (imports, importTree) ← importTree.getMatch ty
     ref.set importTree
     pure imports