From f31f50836d032d6c237272a3b2e733a92a3ee619 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= <wojciech@lean-fro.org>
Date: Tue, 24 Feb 2026 15:24:58 +0000
Subject: [PATCH] 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 |  9 ++++---
 tests/lean/run/issue12630.lean    | 45 +++++++++++++++++++++++++++++++
 2 files changed, 50 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/run/issue12630.lean

diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index ea85d6bf79..c1f80b79af 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/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
diff --git a/tests/lean/run/issue12630.lean b/tests/lean/run/issue12630.lean
new file mode 100644
index 0000000000..6c1dfe0a34
--- /dev/null
+++ b/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"