`withNamespace` doesn't correctly call `popScopes` after running

[taterowney]

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Lean.Elab.Command.withNamespace does not call popScopes after running (the way Lean.Elab.Command.elabEnd does). This causes scoped syntax declarations to reserve keywords outside of their scope if withNamespace has been called.

Context

Was trying to programmatically declare scoped syntax declarations (so they don't reserve keywords outside of a certain namespace). Briefly discussed on Zulip here.

Steps to Reproduce

import Lean
open Lean Meta Elab Command

namespace outer

#eval do
  withNamespace `inner do
    logInfo "shouldn't affect anything"

scoped syntax "myterm" : term

end outer

#eval `(term|myterm) -- parses as a keyword (`outer.termMyterm) instead of an identifier

...and...

import Lean
open Lean Meta Elab Command

#eval do
  withNamespace `outer do
    logInfo "shouldn't affect anything"

namespace outer

scoped syntax "myterm" : term

end outer

#eval `(term|myterm) -- parses as a keyword (`outer.termMyterm) instead of an identifier

Expected behavior: Outside of the outer namespace, myterm should be parsed as an identifier, not a keyword

Actual behavior: Parses as an identifier outside theouter namespace (as happens when withNamespace isn't used anywhere)

Versions

Lean 4.30.0-nightly-2026-02-20
(on live.lean-lang.org)

Additional Information

It appears that this is due to withNamespace not calling Lean.popScope after running and removing the scopes from the Command.State; the end keyword does this and doesn't suffer from this problem. A one-line fix -- adding for _ in *...ns.getNumParts do popScope as the second-to-last line of withNamespace -- fixes the issue. If it would be helpful for me to make a PR I'd be happy to do so!

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[nomeata]

@wkrozowski, you may have that scope stuff paged in from your work on weak scopes and local attributes. Can you comment on this?

[wkrozowski]

@nomeata - The proposed fix here is orthogonal to the work on weak scopes and local attributes (#9968).

My #9968 was about popScope running but discarding local entries it shouldn't have - implicit section/end blocks from macro expansion were unnecessarily popping local attribute entries. The fix was about making popScope a bit smarter about what it discards (the delimitsLocal flag) and essentially do not discard things from such implicit scopes.

The issue here is a bit simpler. We don't even have popScope ever running. Basically, we call pushScope (due to calling addNamespace) and never call popScope/popScopes on cleanup, but we are just modifying the state used by the elaborator. For example elabEnd does both:

  modify fun s => {s with scopes := s.scopes.drop endSize }
  popScopes endSize

I have made a PR and added the tests that capture this issue btw - #12647.

[nomeata]

Thanks!