feat: change delimiting of local attributes in implicit sections (#9968)

This PR modifies macros, which implement non-atomic definitions and
```$cmd1 in $cmd2``` syntax. These macros involve implicit scopes,
introduced through ```section``` and ```namespace``` commands. Since
sections or namespaces are designed to delimit local attributes, this
has led to unintuitive behaviour when applying local attributes to
definitions appearing in the above-mentioned contexts. This has been
causing the following examples to fail:
```lean4
axiom A : Prop

namespace ex1
open Nat in
@[local simp] axiom a : A ↔ True
example : A := by simp
end ex1

namespace ex2
@[local simp] axiom Foo.a : A ↔ True
example : A := by simp
end ex2
```
This PR adds an internal-only piece of syntax,
```InternalSyntax.end_local_scope```, that influences the
```ScopedEnvExtension.addLocalEntry``` used in implementing local
attributes, to avoid delimiting local entries in the current scope. This
command is used in the above-mentioned macros.

Closes [#9445](https://github.com/leanprover/lean4/issues/9445).

---------

Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>

src/Lean/Elab/BuiltinCommand.lean

@@ -16,6 +16,7 @@ public import Lean.Elab.Open
 public import Lean.Elab.SetOption
 public import Init.System.Platform
 public import Lean.Meta.Hint
+public import Lean.Parser.Command
 
 public section
 
@@ -103,6 +104,9 @@ private def checkEndHeader : Name → List Scope → Option Name
       addScope (isNewNamespace := false) (isNoncomputable := ncTk.isSome) (isPublic := publicTk.isSome) (attrs := attrs) "" (← getCurrNamespace)
   | _                        => throwUnsupportedSyntax
 
+@[builtin_command_elab InternalSyntax.end_local_scope] def elabEndLocalScope : CommandElab := fun _ => do
+  setDelimitsLocal
+
 /--
 Produces a `Name` composed of the names of at most the innermost `n` scopes in `ss`, truncating if an
 empty scope is reached (so that we do not suggest names like `Foo.«».Bar`).
@@ -484,10 +488,11 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
   modify fun s => { s with maxRecDepth := maxRecDepth.get options }
   modifyScope fun scope => { scope with opts := options }
 
+open Lean.Parser.Command.InternalSyntax in
 @[builtin_macro Lean.Parser.Command.«in»] def expandInCmd : Macro
   | `($cmd₁ in%$tk $cmd₂) =>
     -- Limit ref variability for incrementality; see Note [Incremental Macros]
-    withRef tk `(section $cmd₁:command $cmd₂ end)
+    withRef tk `(section $cmd₁:command $endLocalScopeSyntax:command $cmd₂ end)
   | _                 => Macro.throwUnsupported
 
 @[builtin_command_elab Parser.Command.addDocString] def elabAddDeclDoc : CommandElab := fun stx => do

src/Lean/Elab/Declaration.lean

@@ -12,6 +12,7 @@ public import Lean.Elab.DefView
 public import Lean.Elab.MutualDef
 public import Lean.Elab.MutualInductive
 public import Lean.Elab.DeclarationRange
+public import Lean.Parser.Command
 import Lean.Parser.Command
 
 public section
@@ -141,7 +142,7 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
         if isExtern (← getEnv) declName then
           compileDecl decl
         Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.afterCompilation
-
+open Lean.Parser.Command.InternalSyntax in
 /--
 Macro that expands a declaration with a complex name into an explicit `namespace` block.
 Implementing this step as a macro means that reuse checking is handled by `elabCommand`.
@@ -153,7 +154,7 @@ def expandNamespacedDeclaration : Macro := fun stx => do
     -- Limit ref variability for incrementality; see Note [Incremental Macros]
     let declTk := stx[1][0]
     let ns := mkIdentFrom declTk ns
-    withRef declTk `(namespace $ns $(⟨newStx⟩) end $ns)
+    withRef declTk `(namespace $ns $endLocalScopeSyntax:command $(⟨newStx⟩) end $ns)
   | none => Macro.throwUnsupported
 
 @[builtin_command_elab declaration, builtin_incremental]

src/Lean/Parser/Command.lean

@@ -292,6 +292,18 @@ with `end <id>`. The `end` command is optional at the end of a file.
 -/
 @[builtin_command_parser] def «end»          := leading_parser
   "end" >> optional (ppSpace >> checkColGt >> ident)
+
+namespace InternalSyntax
+  /-- Disable delimiting of local entries in ScopedEnvExtension within the current scope.
+  This command is for internal use only. It is intended for macros that implicitly introduce new
+  scopes, such as `expandInCmd` and `expandNamespacedDeclaration`. It allows local attributes to remain
+  accessible beyond those implicit scopes, even though they would normally be hidden from the user.
+  -/
+  scoped syntax (name := end_local_scope) "end_local_scope" : command
+
+  def endLocalScopeSyntax : Command := Unhygienic.run `(end_local_scope)
+end InternalSyntax
+
 /-- Declares one or more typed variables, or modifies whether already-declared variables are
   implicit.
 

src/Lean/ScopedEnvExtension.lean

@@ -23,11 +23,11 @@ inductive Entry (α : Type) where
 structure State (σ : Type) where
   state        : σ
   activeScopes : NameSet := {}
+  delimitsLocal : Bool := true -- used for implementing `end_local_scope`.
 
 structure ScopedEntries (β : Type) where
   map : SMap Name (PArray β) := {}
   deriving Inhabited
-
 structure StateStack (α : Type) (β : Type) (σ : Type) where
   stateStack    : List (State σ) := {}
   scopedEntries : ScopedEntries β := {}
@@ -136,7 +136,7 @@ def ScopedEnvExtension.pushScope (ext : ScopedEnvExtension α β σ) (env : Envi
   ext.ext.modifyState (asyncMode := .local) env fun s =>
     match s.stateStack with
     | [] => s
-    | state :: stack => { s with stateStack := state :: state :: stack }
+    | state :: stack => { s with stateStack := { state with delimitsLocal := true } :: state :: stack }
 
 def ScopedEnvExtension.popScope (ext : ScopedEnvExtension α β σ) (env : Environment) : Environment :=
   ext.ext.modifyState (asyncMode := .local) env fun s =>
@@ -144,19 +144,37 @@ def ScopedEnvExtension.popScope (ext : ScopedEnvExtension α β σ) (env : Envir
     | _      :: state₂ :: stack => { s with stateStack := state₂ :: stack }
     | _ => s
 
+/-- Modifies `delimitsLocal` flag to `false` to turn off delimiting of local entries.
+-/
+def ScopedEnvExtension.setDelimitsLocal (ext : ScopedEnvExtension α β σ) (env : Environment)  : Environment :=
+  ext.ext.modifyState (asyncMode := .local) env fun s =>
+    match s.stateStack with
+    | [] => s
+    | state :: stack => {s with stateStack := {state with delimitsLocal := false} :: stack}
+
 def ScopedEnvExtension.addEntry (ext : ScopedEnvExtension α β σ) (env : Environment) (b : β) : Environment :=
   ext.ext.addEntry env (Entry.global b)
 
 def ScopedEnvExtension.addScopedEntry (ext : ScopedEnvExtension α β σ) (env : Environment) (namespaceName : Name) (b : β) : Environment :=
   ext.ext.addEntry env (Entry.«scoped» namespaceName b)
 
+/-- The following function is used to implement `end_local_scope` command.
+
+By default, all states have `delimitsLocal` set to `true`, and the following code modifies only the top element of the stack.
+If the top element’s `delimitsLocal` is `false`, the function instead traverses down the stack until it reaches the first state where `delimitsLocal` is `true`.
+Intuitively, `delimitsLocal` of each `State` determines whether local entries are delimited. When set to false, it allows traversal through implicit scopes where local entries are not delimited.
+-/
+def stateStackModify (ext : ScopedEnvExtension α β σ) (states : List (State σ)) (b : β) : List (State σ) :=
+  match states with
+  | [] => states
+  | top :: states =>
+    let top := { top with state := ext.descr.addEntry top.state b }
+    let bot := if top.delimitsLocal then states else stateStackModify ext states b
+    top :: bot
+
 def ScopedEnvExtension.addLocalEntry (ext : ScopedEnvExtension α β σ) (env : Environment) (b : β) : Environment :=
   ext.ext.modifyState (asyncMode := .local) env fun s =>
-    match s.stateStack with
-    | [] => s
-    | top :: states =>
-      let top := { top with state := ext.descr.addEntry top.state b }
-      { s with stateStack := top :: states }
+    {s with stateStack := stateStackModify ext s.stateStack b}
 
 def ScopedEnvExtension.addCore (env : Environment) (ext : ScopedEnvExtension α β σ) (b : β) (kind : AttributeKind) (namespaceName : Name) : Environment :=
   match kind with
@@ -208,6 +226,12 @@ def popScope [Monad m] [MonadEnv m] [MonadLiftT (ST IO.RealWorld) m] : m Unit :=
   for ext in (← scopedEnvExtensionsRef.get) do
     modifyEnv ext.popScope
 
+/-- Used to implement `end_local_scope` command, that disables delimiting local entries of ScopedEnvExtension in a current scope.
+-/
+def setDelimitsLocal [Monad m] [MonadEnv m] [MonadLiftT (ST IO.RealWorld) m] : m Unit := do
+  for ext in (← scopedEnvExtensionsRef.get) do
+    modifyEnv (ext.setDelimitsLocal ·)
+
 def activateScoped [Monad m] [MonadEnv m] [MonadLiftT (ST IO.RealWorld) m] (namespaceName : Name) : m Unit := do
   for ext in (← scopedEnvExtensionsRef.get) do
     modifyEnv (ext.activateScoped · namespaceName)

tests/lean/run/9445.lean

@@ -0,0 +1,53 @@
+axiom A : Prop
+
+namespace ex0
+@[local simp] axiom a : A ↔ True
+example : A := by simp
+end ex0
+
+namespace ex1
+set_option linter.unusedVariables false in
+@[local simp] axiom a : A ↔ True
+example : A := by simp
+end ex1
+
+namespace ex2
+open Nat in
+@[local simp] axiom a : A ↔ True
+example : A := by simp
+end ex2
+
+namespace ex3
+@[local simp] axiom Foo.a : A ↔ True
+example : A := by simp
+end ex3
+
+namespace ex4
+axiom test.a : A ↔ True
+set_option pp.mvars true in
+attribute [local simp] test.a
+example : A := by simp
+end ex4
+
+namespace ex5
+section
+@[local simp] axiom Foo.a : A ↔ True
+end
+/--
+  error: `simp` made no progress
+-/
+#guard_msgs in
+example : A := by simp
+end ex5
+
+namespace ex6
+namespace Foo
+axiom a : A ↔ True
+attribute [local simp] a
+end Foo
+/--
+  error: `simp` made no progress
+-/
+#guard_msgs in
+example : A := by simp
+end ex6