named `local syntax` can only have two name components

[Rob23oba]

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

local syntax (name := nm) ... declarations don't work (i.e. the syntax can't be used later) when nm consists of more than two name components.

Context

Writing a do elaborator.

Steps to Reproduce

local macro (name := hi) "test1" : term => `(42)
local macro (name := hi.there) "test2" : term => `(42)
local macro (name := hi.there.more) "test3" : term => `(42)
local macro (name := hi.there.more.yes) "test4" : term => `(42)

#check test1 -- works
#check test2 -- works
#check test3 -- fails
#check test4 -- fails

Expected behavior: All macros work equally, the name doesn't matter.

Actual behavior: The name does matter, only test1 and test2 work.

Versions

Lean 4.31.0-nightly-2026-04-03

Impact

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

[Rob23oba]

Okay, it seems like the problem is that we have

namespace hi.there
end_local_scope
attribute [local attr] myDecl
end hi.there

and the hi scope doesn't have an end_local_scope associated with it. So maybe the solution is to have a special namespace command that does setDelimitsLocal for every scope or to have a special namespace command that doesn't do pushScope and another special end command that doesn't do popScope.

@wkrozowski since you implemented end_local_scope.