fix: Thread unique name generator through library_search init

Backport 37450d47e2 from #3595.

Co-authored-by: Leonardo de Moura <leomoura@amazon.com>

RELEASES.md

@@ -8,7 +8,7 @@ This file contains work-in-progress notes for the upcoming release, as well as p
 Please check the [releases](https://github.com/leanprover/lean4/releases) page for the current status
 of each version.
 
-v4.7.0 (development in progress)
+v4.7.0
 ---------
 
 * `simp` and `rw` now use instance arguments found by unification,
@@ -126,7 +126,7 @@ v4.7.0 (development in progress)
   There is now kernel support for these functions.
   [#3376](https://github.com/leanprover/lean4/pull/3376).
 
-* `omega`, our integer linear arithmetic tactic, is now availabe in the core langauge.
+* `omega`, our integer linear arithmetic tactic, is now available in the core langauge.
   * It is supplemented by a preprocessing tactic `bv_omega` which can solve goals about `BitVec`
     which naturally translate into linear arithmetic problems.
     [#3435](https://github.com/leanprover/lean4/pull/3435).
@@ -172,23 +172,23 @@ Breaking changes:
 
 
 Other improvements:
-* several bug fixes for `simp`:
+* Several bug fixes for `simp`:
   * we should not crash when `simp` loops [#3269](https://github.com/leanprover/lean4/pull/3269)
   * `simp` gets stuck on `autoParam` [#3315](https://github.com/leanprover/lean4/pull/3315)
   * `simp` fails when custom discharger makes no progress [#3317](https://github.com/leanprover/lean4/pull/3317)
   * `simp` fails to discharge `autoParam` premises even when it can reduce them to `True` [#3314](https://github.com/leanprover/lean4/pull/3314)
   * `simp?` suggests generated equations lemma names, fixes [#3547](https://github.com/leanprover/lean4/pull/3547) [#3573](https://github.com/leanprover/lean4/pull/3573)
-* fixes for `match` expressions:
+* Fixes for `match` expressions:
   * fix regression with builtin literals [#3521](https://github.com/leanprover/lean4/pull/3521)
   * accept `match` when patterns cover all cases of a `BitVec` finite type [#3538](https://github.com/leanprover/lean4/pull/3538)
   * fix matching `Int` literals [#3504](https://github.com/leanprover/lean4/pull/3504)
   * patterns containing int values and constructors [#3496](https://github.com/leanprover/lean4/pull/3496)
-* improve `termination_by` error messages [#3255](https://github.com/leanprover/lean4/pull/3255)
-* fix `rename_i` in macros, fixes [#3553](https://github.com/leanprover/lean4/pull/3553) [#3581](https://github.com/leanprover/lean4/pull/3581)
-* fix excessive resource usage in `generalize`, fixes [#3524](https://github.com/leanprover/lean4/pull/3524) [#3575](https://github.com/leanprover/lean4/pull/3575)
-* an equation lemma with autoParam arguments fails to rewrite, fixing [#2243](https://github.com/leanprover/lean4/pull/2243) [#3316](https://github.com/leanprover/lean4/pull/3316)
+* Improve `termination_by` error messages [#3255](https://github.com/leanprover/lean4/pull/3255)
+* Fix `rename_i` in macros, fixes [#3553](https://github.com/leanprover/lean4/pull/3553) [#3581](https://github.com/leanprover/lean4/pull/3581)
+* Fix excessive resource usage in `generalize`, fixes [#3524](https://github.com/leanprover/lean4/pull/3524) [#3575](https://github.com/leanprover/lean4/pull/3575)
+* An equation lemma with autoParam arguments fails to rewrite, fixing [#2243](https://github.com/leanprover/lean4/pull/2243) [#3316](https://github.com/leanprover/lean4/pull/3316)
 * `add_decl_doc` should check that declarations are local [#3311](https://github.com/leanprover/lean4/pull/3311)
-* instantiate the types of inductives with the right parameters, closing [#3242](https://github.com/leanprover/lean4/pull/3242) [#3246](https://github.com/leanprover/lean4/pull/3246)
+* Instantiate the types of inductives with the right parameters, closing [#3242](https://github.com/leanprover/lean4/pull/3242) [#3246](https://github.com/leanprover/lean4/pull/3246)
 * New simprocs for many basic types. [#3407](https://github.com/leanprover/lean4/pull/3407)
 
 Lake fixes:

src/CMakeLists.txt

@@ -11,7 +11,7 @@ project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
 set(LEAN_VERSION_MINOR 7)
 set(LEAN_VERSION_PATCH 0)
-set(LEAN_VERSION_IS_RELEASE 0)  # This number is 1 in the release revision, and 0 otherwise.
+set(LEAN_VERSION_IS_RELEASE 1)  # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")
 set(LEAN_VERSION_STRING "${LEAN_VERSION_MAJOR}.${LEAN_VERSION_MINOR}.${LEAN_VERSION_PATCH}")
 if (LEAN_SPECIAL_VERSION_DESC)

src/Lean/Meta/Injective.lean

@@ -26,8 +26,10 @@ private def mkAnd? (args : Array Expr) : Option Expr := Id.run do
 
 def elimOptParam (type : Expr) : CoreM Expr := do
   Core.transform type fun e =>
-    let_expr optParam _ a := e | return .continue
-    return TransformStep.visit a
+    if e.isAppOfArity ``optParam 2 then
+      return TransformStep.visit (e.getArg! 0)
+    else
+      return .continue
 
 private partial def mkInjectiveTheoremTypeCore? (ctorVal : ConstructorVal) (useEq : Bool) : MetaM (Option Expr) := do
   let us := ctorVal.levelParams.map mkLevelParam

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

tests/lean/run/elimOptParam.lean

@@ -0,0 +1,14 @@
+import Lean
+
+def f (x := 0) (y := 1) : Nat :=
+  x + y
+
+open Lean Meta
+
+/--
+info: Nat → Nat → Nat
+-/
+#guard_msgs in
+run_meta do
+  let info ← getConstInfo ``f
+  logInfo (← elimOptParam info.type)