fix: withNamespace now correctly calls popScopes after running (#12647)

This PR adds the missing `popScopes` call to `withNamespace`, which
previously
only dropped scopes from the elaborator's `Command.State` but did not
pop the
environment's `ScopedEnvExtension` state stacks. This caused scoped
syntax
declarations to leak keywords outside their namespace when
`withNamespace` had
been called.

Closes #12630

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

src/Lean/Elab/BuiltinCommand.lean

@@ -70,16 +70,17 @@ where go
 private def addNamespace (header : Name) : CommandElabM Unit :=
   addScopes (isNewNamespace := true) (isNoncomputable := false) (attrs := []) header
 
+private def popScopes (numScopes : Nat) : CommandElabM Unit :=
+  for _ in *...numScopes do
+    popScope
+
 def withNamespace {α} (ns : Name) (elabFn : CommandElabM α) : CommandElabM α := do
   addNamespace ns
   let a ← elabFn
   modify fun s => { s with scopes := s.scopes.drop ns.getNumParts }
+  popScopes ns.getNumParts
   pure a
 
-private def popScopes (numScopes : Nat) : CommandElabM Unit :=
-  for _ in *...numScopes do
-    popScope
-
 private def innermostScopeName? : List Scope → Option Name
   | { header := "", .. } :: _ => none
   | { header := h, .. }  :: _ => some <| .mkSimple h

tests/lean/run/issue12630.lean

@@ -0,0 +1,45 @@
+import Lean
+open Lean Meta Elab Command
+
+/-!
+# `withNamespace` should correctly pop scopes after running
+
+Issue: https://github.com/leanprover/lean4/issues/12630
+
+`withNamespace` was not calling `popScopes` on the environment extensions,
+causing `scoped syntax` declarations to leak keywords outside their scope.
+-/
+
+-- Test 1: `withNamespace` inside namespace shouldn't leak scoped syntax
+namespace outer1
+
+#eval do
+  withNamespace `inner do
+    logInfo "shouldn't affect anything"
+
+scoped syntax "myterm1" : term
+
+end outer1
+
+-- Outside the namespace, `myterm1` should parse as an identifier, not a keyword.
+#eval do
+  let stx ← `(term|myterm1)
+  unless stx.raw.isIdent do
+    throwError "expected identifier, got keyword"
+
+-- Test 2: `withNamespace` before namespace shouldn't leak scoped syntax
+#eval do
+  withNamespace `outer2 do
+    logInfo "shouldn't affect anything"
+
+namespace outer2
+
+scoped syntax "myterm2" : term
+
+end outer2
+
+-- Outside the namespace, `myterm2` should parse as an identifier, not a keyword.
+#eval do
+  let stx ← `(term|myterm2)
+  unless stx.raw.isIdent do
+    throwError "expected identifier, got keyword"