refactor: realizeConst: do not set declPrefix (#8107)

This PR makes `realizeConst` to not set a `declPrefix`. This allows the
realization of both `foo.eq_def` and `bar.eq_def`, where `foo` and `bar`
are mutually recursive, all attached to the same function's environment.

src/Lean/Environment.lean

@@ -855,15 +855,20 @@ structure PromiseCheckedResult where
   asyncEnv : Environment
   private checkedEnvPromise : IO.Promise Kernel.Environment
 
+def realizingStack (env : Environment) : List Name :=
+  env.asyncCtx?.map (·.realizingStack) |>.getD []
+
 /-- Creates an async context for the given declaration name, normalizing it for use as a prefix. -/
-private def enterAsync (declName : Name) (realizing? : Option Name := none) (env : Environment) : Environment :=
+private def enterAsync (declName : Name) (env : Environment) : Environment :=
   { env with asyncCtx? := some {
     declPrefix := privateToUserName declName.eraseMacroScopes
-    realizingStack :=
-      let s := env.asyncCtx?.map (·.realizingStack) |>.getD []
-      match realizing? with
-      | none   => s
-      | some n => n :: s } }
+    realizingStack := env.realizingStack } }
+
+/-- Creates an async context when realizing `declName` -/
+private def enterAsyncRealizing (declName : Name) (env : Environment) : Environment :=
+  { env with asyncCtx? := some {
+    declPrefix := .anonymous
+    realizingStack := declName :: env.realizingStack } }
 
 /--
 Starts an asynchronous modification of the kernel environment. The environment is split into a
@@ -2166,9 +2171,8 @@ def realizeConst (env : Environment) (forConst : Name) (constName : Name)
         realizedLocalConsts := realizeEnv.realizedLocalConsts.insert forConst ctx
         realizedImportedConsts? := env.realizedImportedConsts?
       }
-      -- ensure realized constants are nested below `forConst` and that environment extension
-      -- modifications know they are in an async context
-      let realizeEnv := realizeEnv.enterAsync (realizing? := constName) forConst
+      -- ensure that environment extension modifications know they are in an async context
+      let realizeEnv := realizeEnv.enterAsyncRealizing constName
       -- skip kernel in `realize`, we'll re-typecheck anyway
       let realizeOpts := debug.skipKernelTC.set ctx.opts true
       let (realizeEnv', dyn) ← realize realizeEnv realizeOpts

tests/lean/run/issue8107.lean

@@ -0,0 +1,35 @@
+import Lean.Meta
+/-!
+This test checks that within ```realizeConst ``foo `foo.test``` we are not restricted
+to adding declarations with a name scoped under `foo`, but can add any names
+to the environment. This is important for constructions that add names to each 
+function in a mutual recursive group.
+-/
+def foo := True
+def bar := True
+
+open Lean Meta
+
+-- NOTE: declaring and running a `realizeConst` invocation isn't usually done in the same file, so
+-- changing the closure below may require a server restart to see the changes.
+
+run_meta  do
+  realizeConst ``foo `foo.test do
+    addDecl <| Declaration.thmDecl {
+      name := `foo.test
+      type := mkConst ``True
+      value := mkConst ``True.intro
+      levelParams := [] }
+    addDecl <| Declaration.thmDecl {
+      name := `bar.test
+      type := mkConst ``True
+      value := mkConst ``True.intro
+      levelParams := [] }
+
+/-- info: foo.test : True -/
+#guard_msgs in
+#check foo.test
+
+/-- info: bar.test : True -/
+#guard_msgs in
+#check bar.test