From d4a5a2c632842fce7c884d5b1a3c1a7730aef871 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 31 Jul 2025 18:21:53 +0200
Subject: [PATCH] fix: local syntax should create private definitions

---
 src/Lean/Elab/AuxDef.lean                     |  6 +-
 src/Lean/Elab/BinderPredicates.lean           | 12 ++--
 src/Lean/Elab/ElabRules.lean                  | 21 +++---
 src/Lean/Elab/Macro.lean                      | 25 ++++---
 src/Lean/Elab/MacroRules.lean                 |  7 +-
 src/Lean/Elab/Notation.lean                   | 69 ++++++++-----------
 src/Lean/Elab/Syntax.lean                     | 33 +++++++--
 src/Lean/Elab/Util.lean                       |  9 ++-
 src/Lean/Parser/Command.lean                  |  6 ++
 tests/lean/run/localGlobalNotation.lean       |  5 ++
 ...InstanceOutsideNamespace.lean.expected.out |  2 +
 tests/lean/syntaxPrec.lean.expected.out       |  2 +-
 tests/pkg/misc/Misc/Foo.lean                  |  7 +-
 tests/pkg/misc/lean-toolchain                 |  1 +
 14 files changed, 113 insertions(+), 92 deletions(-)
 create mode 100644 tests/lean/run/localGlobalNotation.lean
 create mode 100644 tests/pkg/misc/lean-toolchain

diff --git a/src/Lean/Elab/AuxDef.lean b/src/Lean/Elab/AuxDef.lean
index d40d8cc565..5f11582263 100644
--- a/src/Lean/Elab/AuxDef.lean
+++ b/src/Lean/Elab/AuxDef.lean
@@ -20,11 +20,11 @@ Declares an auxiliary definition with an automatically generated name.
 For example, `aux_def foo : Nat := 42` creates a definition
 with an internal, unused name based on the suggestion `foo`.
 -/
-scoped syntax (name := aux_def) docComment ? attributes ? "aux_def" ident+ ":" term ":=" term : command
+scoped syntax (name := aux_def) docComment ? attributes ? visibility "aux_def" ident+ ":" term ":=" term : command
 
 @[builtin_command_elab «aux_def»]
 def elabAuxDef : CommandElab
-  | `($[$doc?:docComment]? $[$attrs?:attributes]? aux_def $suggestion* : $ty := $body) => do
+  | `($[$doc?:docComment]? $[$attrs?:attributes]? $vis:visibility aux_def $suggestion* : $ty := $body) => do
     let id := suggestion.map (·.getId.eraseMacroScopes) |>.foldl (· ++ ·) Name.anonymous
     let id := `_aux ++ (← getMainModule) ++ `_ ++ id
     let id := String.intercalate "_" <| id.components.map (·.toString (escape := false))
@@ -36,6 +36,6 @@ def elabAuxDef : CommandElab
     let (id, _) := DeclNameGenerator.ofPrefix ns |>.mkUniqueName env («infix» := Name.mkSimple id)
     let id := id.replacePrefix ns Name.anonymous -- TODO: replace with def _root_.id
     elabCommand <|
-      ← `($[$doc?:docComment]? $[$attrs?:attributes]?
+      ← `($[$doc?:docComment]? $[$attrs?:attributes]? $vis:visibility
           meta def $(mkIdentFrom (mkNullNode suggestion) id (canonical := true)):ident : $ty := $body)
   | _ => throwUnsupportedSyntax
diff --git a/src/Lean/Elab/BinderPredicates.lean b/src/Lean/Elab/BinderPredicates.lean
index a5a9b327d0..8ab9267042 100644
--- a/src/Lean/Elab/BinderPredicates.lean
+++ b/src/Lean/Elab/BinderPredicates.lean
@@ -21,18 +21,14 @@ namespace Lean.Elab.Command
       $[(name := $name?)]? $[(priority := $prio?)]? $x $args:macroArg* => $rhs) => do
     let prio ← liftMacroM do evalOptPrio prio?
     let (stxParts, patArgs) := (← args.mapM expandMacroArg).unzip
-    let name ← match name? with
-      | some name => pure name.getId
-      | none => liftMacroM do mkNameFromParserSyntax `binderTerm (mkNullNode stxParts)
-    let nameTk := name?.getD (mkIdentFrom tk name)
+    let kind ← elabSyntax (← `($[$doc?:docComment]? $[@[$attrs?,*]]? $attrKind:attrKind syntax%$tk
+        $[(name := $name?)]? (priority := $(quote prio)) $[$stxParts]* : binderPred))
     /- The command `syntax [<kind>] ...` adds the current namespace to the syntax node kind.
     So, we must include current namespace when we create a pattern for the following
     `macro_rules` commands. -/
-    let pat : TSyntax `binderPred := ⟨(mkNode ((← getCurrNamespace) ++ name) patArgs).1⟩
+    let pat : TSyntax `binderPred := ⟨(mkNode kind patArgs).1⟩
     elabCommand <|<-
-    `($[$doc?:docComment]? $[@[$attrs?,*]]? $attrKind:attrKind syntax%$tk
-        (name := $nameTk) (priority := $(quote prio)) $[$stxParts]* : binderPred
-      $[$doc?:docComment]? macro_rules%$tk
+    `($[$doc?:docComment]? macro_rules%$tk
         | `(satisfies_binder_pred% $$($x):term $pat:binderPred) => $rhs)
   | _ => throwUnsupportedSyntax
 
diff --git a/src/Lean/Elab/ElabRules.lean b/src/Lean/Elab/ElabRules.lean
index e6b54c0827..cc70c578ca 100644
--- a/src/Lean/Elab/ElabRules.lean
+++ b/src/Lean/Elab/ElabRules.lean
@@ -50,25 +50,26 @@ def elabElabRulesAux (doc? : Option (TSyntax ``docComment))
     pure <| match attrs? with
       | some attrs => attrs.getElems.push attr
       | none => #[attr]
+  let vis := Parser.Command.visibility.ofAttrKind attrKind
   if let some expId := expty? then
     if catName == `term then
-      `($[$doc?:docComment]? @[$(← mkAttrs `term_elab),*]
+      `($[$doc?:docComment]? @[$(← mkAttrs `term_elab),*] $vis:visibility
         aux_def elabRules $(mkIdent k) : Lean.Elab.Term.TermElab :=
         fun stx expectedType? => Lean.Elab.Term.withExpectedType expectedType? fun $expId => match stx with
           $alts:matchAlt* | _ => no_error_if_unused% throwUnsupportedSyntax)
     else
       throwErrorAt expId "syntax category '{catName}' does not support expected type specification"
   else if catName == `term then
-    `($[$doc?:docComment]? @[$(← mkAttrs `term_elab),*]
+    `($[$doc?:docComment]? @[$(← mkAttrs `term_elab),*] $vis:visibility
       aux_def elabRules $(mkIdent k) : Lean.Elab.Term.TermElab :=
       fun stx _ => match stx with
         $alts:matchAlt* | _ => no_error_if_unused% throwUnsupportedSyntax)
   else if catName == `command then
-    `($[$doc?:docComment]? @[$(← mkAttrs `command_elab),*]
+    `($[$doc?:docComment]? @[$(← mkAttrs `command_elab),*] $vis:visibility
       aux_def elabRules $(mkIdent k) : Lean.Elab.Command.CommandElab :=
       fun $alts:matchAlt* | _ => no_error_if_unused% throwUnsupportedSyntax)
   else if catName == `tactic || catName == `conv then
-    `($[$doc?:docComment]? @[$(← mkAttrs `tactic),*]
+    `($[$doc?:docComment]? @[$(← mkAttrs `tactic),*] $vis:visibility
       aux_def elabRules $(mkIdent k) : Lean.Elab.Tactic.Tactic :=
       fun $alts:matchAlt* | _ => no_error_if_unused% throwUnsupportedSyntax)
   else
@@ -92,15 +93,11 @@ def elabElab : CommandElab
       $cat $[<= $expectedType?]? => $rhs) => do
     let prio    ← liftMacroM <| evalOptPrio prio?
     let (stxParts, patArgs) := (← args.mapM expandMacroArg).unzip
-    -- name
-    let name ← match name? with
-      | some name => pure name.getId
-      | none => addMacroScopeIfLocal (← liftMacroM <| mkNameFromParserSyntax cat.getId (mkNullNode stxParts)) attrKind
-    let nameId := name?.getD (mkIdentFrom tk name (canonical := true))
-    let pat := ⟨mkNode ((← getCurrNamespace) ++ name) patArgs⟩
-    elabCommand <|← `(
+    let kind ← elabSyntax <|← `(
       $[$doc?:docComment]? $[@[$attrs?,*]]? $attrKind:attrKind
-      syntax%$tk$[:$prec?]? (name := $nameId) (priority := $(quote prio):num) $[$stxParts]* : $cat
+      syntax%$tk$[:$prec?]? $[(name := $name?)]? (priority := $(quote prio):num) $[$stxParts]* : $cat)
+    let pat := ⟨mkNode kind patArgs⟩
+    elabCommand <|← `(
       $[$doc?:docComment]? elab_rules : $cat $[<= $expectedType?]? | `($pat) => $rhs)
   | _ => throwUnsupportedSyntax
 
diff --git a/src/Lean/Elab/Macro.lean b/src/Lean/Elab/Macro.lean
index 94004b726f..654f5dca66 100644
--- a/src/Lean/Elab/Macro.lean
+++ b/src/Lean/Elab/Macro.lean
@@ -23,29 +23,28 @@ open Lean.Parser.Command
     withRef (mkNullNode #[tk, rhs]) do
       let prio  ← liftMacroM <| evalOptPrio prio?
       let (stxParts, patArgs) := (← args.mapM expandMacroArg).unzip
-      -- name
-      let name ← match name? with
-        | some name => pure name.getId
-        | none => addMacroScopeIfLocal (← liftMacroM <| mkNameFromParserSyntax cat.getId (mkNullNode stxParts)) attrKind
-      /- The command `syntax [<kind>] ...` adds the current namespace to the syntax node kind.
-        So, we must include current namespace when we create a pattern for the following `macro_rules` commands. -/
-      let pat := ⟨mkNode ((← getCurrNamespace) ++ name) patArgs⟩
-      let stxCmd ← `($[$doc?:docComment]? $[@[$attrs?,*]]? $attrKind:attrKind
+      let kind ← elabSyntax (← `($[$doc?:docComment]? $[@[$attrs?,*]]? $attrKind:attrKind
         syntax$[:$prec?]?
-          (name := $(name?.getD (mkIdentFrom tk name (canonical := true))))
+          $[(name := $name?)]?
           (priority := $(quote prio):num)
-          $[$stxParts]* : $cat)
+          $[$stxParts]* : $cat))
+      let pat := ⟨mkNode kind patArgs⟩
       let rhs := rhs.raw
+      -- Elide `scoped` for `macro_rules`; this allows for using scoped macros in unscoped macros
+      -- for back-compat and unlike with `local`, there would be no benefit to enforcing `scoped`.
+      let mut rulesKind := attrKind
+      if rulesKind matches `(attrKind| scoped) then
+        rulesKind ← `(attrKind| )
       let macroRulesCmd ← if rhs.getArgs.size == 1 then
         -- `rhs` is a `term`
         let rhs := ⟨rhs[0]⟩
-        `($[$doc?:docComment]? macro_rules | `($pat) => Functor.map (@TSyntax.raw $(quote cat.getId.eraseMacroScopes)) $rhs)
+        `($[$doc?:docComment]? $rulesKind:attrKind macro_rules | `($pat) => Functor.map (@TSyntax.raw $(quote cat.getId.eraseMacroScopes)) $rhs)
       else
         -- TODO(gabriel): remove after bootstrap
         -- `rhs` is of the form `` `( $body ) ``
         let rhsBody := ⟨rhs[1]⟩
-        `($[$doc?:docComment]? macro_rules | `($pat) => `($rhsBody))
-      elabCommand <| mkNullNode #[stxCmd, macroRulesCmd]
+        `($[$doc?:docComment]? $rulesKind:attrKind macro_rules | `($pat) => `($rhsBody))
+      elabCommand macroRulesCmd
   | _ => throwUnsupportedSyntax
 
 end Lean.Elab.Command
diff --git a/src/Lean/Elab/MacroRules.lean b/src/Lean/Elab/MacroRules.lean
index 64da1c98f4..ecb4aebb2e 100644
--- a/src/Lean/Elab/MacroRules.lean
+++ b/src/Lean/Elab/MacroRules.lean
@@ -47,7 +47,8 @@ def elabMacroRulesAux (doc? : Option (TSyntax ``docComment))
   let attrs := match attrs? with
     | some attrs => attrs.getElems.push attr
     | none => #[attr]
-  `($[$doc?:docComment]? @[$attrs,*]
+  let vis := Parser.Command.visibility.ofAttrKind attrKind
+  `($[$doc?:docComment]? @[$attrs,*] $vis:visibility
     aux_def macroRules $(mkIdentFrom tk k (canonical := true)) : Macro :=
      fun $alts:matchAlt* | _ => no_error_if_unused% throw Lean.Macro.Exception.unsupportedSyntax)
 
@@ -64,9 +65,11 @@ def elabMacroRulesAux (doc? : Option (TSyntax ``docComment))
       let attrs := match attrs? with
         | some attrs => attrs.getElems.push attr
         | none => #[attr]
-      `($[$doc?:docComment]? @[$attrs,*]
+      let vis := Parser.Command.visibility.ofAttrKind attrKind
+      `($[$doc?:docComment]? @[$attrs,*] $vis:visibility
         aux_def $(mkIdentFrom tk kind.getId (canonical := true)) $kind : Macro := fun $x:ident => $rhs)
   | `($[$doc?:docComment]? $[@[$attrs?,*]]? $attrKind:attrKind macro_rules%$tk (kind := $kind) $alts:matchAlt*) =>
+    withExporting (isExporting := !attrKind matches `(attrKind| local)) do
     withRef (mkNullNode #[tk, mkNullNode alts]) do
       elabMacroRulesAux doc? attrs? attrKind tk (← resolveSyntaxKind kind.getId) alts
   | _  => throwUnsupportedSyntax
diff --git a/src/Lean/Elab/Notation.lean b/src/Lean/Elab/Notation.lean
index e3e9d596b3..ba067c46aa 100644
--- a/src/Lean/Elab/Notation.lean
+++ b/src/Lean/Elab/Notation.lean
@@ -112,54 +112,39 @@ def mkUnexpander (attrKind : TSyntax ``attrKind) (pat qrhs : Term) : OptionT Mac
   -- The reference is attached to the syntactic representation of the called function itself, not the entire function application
   let lhs ← `($$f:ident)
   let lhs := Syntax.mkApp lhs (.mk args)
-  `(@[$attrKind app_unexpander $(mkIdent c)]
+  let vis := Parser.Command.visibility.ofAttrKind attrKind
+  `(@[$attrKind app_unexpander $(mkIdent c)] $vis:visibility
     aux_def unexpand $(mkIdent c) : Lean.PrettyPrinter.Unexpander := fun
       | `($lhs)             => withRef f `($pat)
       | _                   => throw ())
 
-private def expandNotationAux (ref : Syntax) (currNamespace : Name)
-    (doc? : Option (TSyntax ``docComment))
-    (attrs? : Option (TSepArray ``attrInstance ","))
-    (attrKind : TSyntax ``attrKind)
-    (prec? : Option Prec) (name? : Option Ident) (prio? : Option Prio)
-    (items : Array (TSyntax ``notationItem)) (rhs : Term) : MacroM Syntax := do
-  let prio ← evalOptPrio prio?
-  -- build parser
-  let syntaxParts ← items.mapM expandNotationItemIntoSyntaxItem
-  let cat := mkIdentFrom ref `term
-  let name ←
-    match name? with
-    | some name => pure name.getId
-    | none => addMacroScopeIfLocal (← mkNameFromParserSyntax `term (mkNullNode syntaxParts)) attrKind
-  -- build macro rules
-  let vars := items.filter fun item => item.raw.getKind == ``identPrec
-  let vars := vars.map fun var => var.raw[0]
-  let qrhs := ⟨antiquote vars rhs⟩
-  let attrs? := addInheritDocDefault rhs attrs?
-  let patArgs ← items.mapM expandNotationItemIntoPattern
-  /- The command `syntax [<kind>] ...` adds the current namespace to the syntax node kind.
-     So, we must include current namespace when we create a pattern for the following `macro_rules` commands. -/
-  let fullName := currNamespace ++ name
-  let pat : Term := ⟨mkNode fullName patArgs⟩
-  let stxDecl ← `($[$doc?:docComment]? $[@[$attrs?,*]]? $attrKind:attrKind
-    syntax $[: $prec?]? (name := $(name?.getD (mkIdent name))) (priority := $(quote prio)) $[$syntaxParts]* : $cat)
-  let macroDecl ← `(macro_rules | `($pat) => ``($qrhs))
-  let macroDecls ←
+@[builtin_command_elab Lean.Parser.Command.notation] def elabNotation : CommandElab
+  | ref@`($[$doc?:docComment]? $[@[$attrs?,*]]? $attrKind:attrKind
+      notation $[: $prec?]? $[(name := $name?)]? $[(priority := $prio?)]? $items* => $rhs) => do
+    let attrs? := addInheritDocDefault rhs attrs?
+    let prio ← liftMacroM <| evalOptPrio prio?
+    -- build parser
+    let syntaxParts ← liftMacroM <| items.mapM expandNotationItemIntoSyntaxItem
+    let cat := mkIdentFrom ref `term
+    let kind ← elabSyntax (← `($[$doc?:docComment]? $[@[$attrs?,*]]? $attrKind:attrKind
+      syntax $[: $prec?]? $[(name := $name?)]? (priority := $(quote prio)) $[$syntaxParts]* : $cat))
+    -- build macro rules
+    let vars := items.filter fun item => item.raw.getKind == ``identPrec
+    let vars := vars.map fun var => var.raw[0]
+    let qrhs := ⟨antiquote vars rhs⟩
+    let patArgs ← liftMacroM <| items.mapM expandNotationItemIntoPattern
+    let pat : Term := ⟨mkNode kind patArgs⟩
+    let macroDecl ← `($attrKind:attrKind macro_rules | `($pat) => ``($qrhs))
     if isLocalAttrKind attrKind then
       -- Make sure the quotation pre-checker takes section variables into account for local notation.
-      `(section set_option quotPrecheck.allowSectionVars true $macroDecl end)
+      let opts ← getOptions
+      let opts := Term.Quotation.quotPrecheck.allowSectionVars.set opts true
+      withScope (fun sc => { sc with opts }) do
+        elabCommand macroDecl
     else
-      pure ⟨mkNullNode #[macroDecl]⟩
-  match (← mkUnexpander attrKind pat qrhs |>.run) with
-  | some delabDecl => return mkNullNode #[stxDecl, macroDecls, delabDecl]
-  | none           => return mkNullNode #[stxDecl, macroDecls]
-
-@[builtin_macro Lean.Parser.Command.notation] def expandNotation : Macro
-  | stx@`($[$doc?:docComment]? $[@[$attrs?,*]]? $attrKind:attrKind
-      notation $[: $prec?]? $[(name := $name?)]? $[(priority := $prio?)]? $items* => $rhs) => do
-    -- trigger scoped checks early and only once
-    let _ ← toAttributeKind attrKind
-    expandNotationAux stx (← Macro.getCurrNamespace) doc? attrs? attrKind prec? name? prio? items rhs
-  | _ => Macro.throwUnsupported
+      elabCommand macroDecl
+    if let some delabDecl := (← liftMacroM <| mkUnexpander attrKind pat qrhs |>.run) then
+      elabCommand delabDecl
+  | _ => throwUnsupportedSyntax
 
 end Lean.Elab.Command
diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index 05ce2287c7..23be3efb60 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -314,7 +314,7 @@ private def declareSyntaxCatQuotParser (catName : Name) : CommandElabM Unit := d
   ```
   It generates the names `term_+_` and `term[_,]`
 -/
-partial def mkNameFromParserSyntax (catName : Name) (stx : Syntax) : MacroM Name := do
+private partial def mkNameFromParserSyntax (catName : Name) (stx : Syntax) : MacroM Name := do
   mkUnusedBaseName <| Name.mkSimple <| appendCatName <| visit stx ""
 where
   visit (stx : Syntax) (acc : String) : String :=
@@ -368,13 +368,14 @@ def isLocalAttrKind (attrKind : Syntax) : Bool :=
 /--
 Add macro scope to `name` if it does not already have them, and `attrKind` is `local`.
 -/
-def addMacroScopeIfLocal [MonadQuotation m] [Monad m] (name : Name) (attrKind : Syntax) : m Name := do
+private def addMacroScopeIfLocal [MonadQuotation m] [Monad m] (name : Name) (attrKind : Syntax) : m Name := do
   if isLocalAttrKind attrKind && !name.hasMacroScopes then
     MonadQuotation.addMacroScope name
   else
     return name
 
-@[builtin_command_elab «syntax»] def elabSyntax : CommandElab := fun stx => do
+/-- Elaborates the given `syntax` command and returns the new node kind. -/
+def elabSyntax (stx : Syntax) : CommandElabM Name := do
   let `($[$doc?:docComment]? $[ @[ $attrInstances:attrInstance,* ] ]? $attrKind:attrKind
       syntax%$tk $[: $prec? ]? $[(name := $name?)]? $[(priority := $prio?)]? $[$ps:stx]* : $catStx) := stx
     | throwUnsupportedSyntax
@@ -390,24 +391,42 @@ def addMacroScopeIfLocal [MonadQuotation m] [Monad m] (name : Name) (attrKind :
     | none      => pure precDefault
   let name ← match name? with
     | some name => pure name.getId
-    | none => addMacroScopeIfLocal (← liftMacroM <| mkNameFromParserSyntax cat syntaxParser) attrKind
+    | none =>
+      let base ← liftMacroM <| mkNameFromParserSyntax cat syntaxParser
+      let mut name := base
+      let mut i := 1
+      -- Avoid name conflicts, for which we have to check both public and private name
+      while (←
+        let fullName := (← getCurrNamespace) ++ name
+        hasConst fullName <||>
+          (withoutExporting <| hasConst (mkPrivateName (← getEnv) fullName))) do
+        name := base.appendIndexAfter i
+        i := i + 1
+      pure name
   let prio ← liftMacroM <| evalOptPrio prio?
   let idRef := (name?.map (·.raw)).getD tk
-  let stxNodeKind := (← getCurrNamespace) ++ name
+  let mut stxNodeKind := (← getCurrNamespace) ++ name
+  if attrKind matches `(attrKind| local) then
+    stxNodeKind := mkPrivateName (← getEnv) stxNodeKind
   let catParserId := mkIdentFrom idRef (cat.appendAfter "_parser")
   let (val, lhsPrec?) ← runTermElabM fun _ => Term.toParserDescr syntaxParser cat
   let declName := name?.getD (mkIdentFrom idRef name (canonical := true))
   let attrInstance ← `(attrInstance| $attrKind:attrKind $catParserId:ident $(quote prio):num)
   let attrInstances := attrInstances.getD { elemsAndSeps := #[] }
   let attrInstances := attrInstances.push attrInstance
+  let vis := Parser.Command.visibility.ofAttrKind attrKind
   let d ← if let some lhsPrec := lhsPrec? then
-    `($[$doc?:docComment]? @[$attrInstances,*] meta def $declName:ident : Lean.TrailingParserDescr :=
+    `($[$doc?:docComment]? @[$attrInstances,*] $vis:visibility meta def $declName:ident : Lean.TrailingParserDescr :=
         ParserDescr.trailingNode $(quote stxNodeKind) $(quote prec) $(quote lhsPrec) $val)
   else
-    `($[$doc?:docComment]? @[$attrInstances,*] meta def $declName:ident : Lean.ParserDescr :=
+    `($[$doc?:docComment]? @[$attrInstances,*] $vis:visibility meta def $declName:ident : Lean.ParserDescr :=
         ParserDescr.node $(quote stxNodeKind) $(quote prec) $val)
   trace `Elab fun _ => d
   withMacroExpansion stx d <| elabCommand d
+  return stxNodeKind
+
+@[builtin_command_elab «syntax»] private def elabSyntaxAux : CommandElab := fun stx =>
+  discard <| elabSyntax stx
 
 @[builtin_command_elab «syntaxAbbrev»] def elabSyntaxAbbrev : CommandElab := fun stx => do
   let `($[$doc?:docComment]? syntax $declName:ident := $[$ps:stx]*) ← pure stx | throwUnsupportedSyntax
diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean
index 715274821d..1058bbe212 100644
--- a/src/Lean/Elab/Util.lean
+++ b/src/Lean/Elab/Util.lean
@@ -79,8 +79,13 @@ def addMacroStack {m} [Monad m] [MonadOptions m] (msgData : MessageData) (macroS
       msgData
 
 def checkSyntaxNodeKind [Monad m] [MonadEnv m] [MonadError m] (k : Name) : m Name := do
-  if Parser.isValidSyntaxNodeKind (← getEnv) k then pure k
-  else throwError "failed"
+  if Parser.isValidSyntaxNodeKind (← getEnv) k then
+    return k
+  if !(← getEnv).isExporting && !isPrivateName k then
+    let k := mkPrivateName (← getEnv) k
+    if Parser.isValidSyntaxNodeKind (← getEnv) k then
+      return k
+  throwError "failed"
 
 def checkSyntaxNodeKindAtNamespaces [Monad m] [MonadEnv m] [MonadError m] (k : Name) : Name → m Name
   | n@(.str p _) => checkSyntaxNodeKind (n ++ k) <|> checkSyntaxNodeKindAtNamespaces k p
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index ddbecce413..df424d613d 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -885,6 +885,12 @@ used to generate visibility syntax for declarations that is independent of the p
 def visibility.ofBool (isPublic : Bool) : TSyntax ``visibility :=
   Unhygienic.run <| if isPublic then `(visibility| public) else `(visibility| private)
 
+/--
+Returns syntax for `private` if `attrKind` is `local` and `public` otherwise.
+-/
+def visibility.ofAttrKind (attrKind : TSyntax ``Term.attrKind) : TSyntax ``visibility :=
+  visibility.ofBool <| !attrKind matches `(attrKind| local)
+
 end Command
 
 namespace Term
diff --git a/tests/lean/run/localGlobalNotation.lean b/tests/lean/run/localGlobalNotation.lean
new file mode 100644
index 0000000000..2b5eebf176
--- /dev/null
+++ b/tests/lean/run/localGlobalNotation.lean
@@ -0,0 +1,5 @@
+/-! `notation` should avoid name conflicts, also between local/global. -/
+namespace Foo
+
+local notation "foo" => 1
+notation "foo" => 1
diff --git a/tests/lean/scopedInstanceOutsideNamespace.lean.expected.out b/tests/lean/scopedInstanceOutsideNamespace.lean.expected.out
index d5955fe479..31ec1d2cfd 100644
--- a/tests/lean/scopedInstanceOutsideNamespace.lean.expected.out
+++ b/tests/lean/scopedInstanceOutsideNamespace.lean.expected.out
@@ -1,4 +1,6 @@
 scopedInstanceOutsideNamespace.lean:1:0-2:38: error: Scoped attributes must be used inside namespaces
 "true"
 scopedInstanceOutsideNamespace.lean:6:0-6:30: error: Scoped attributes must be used inside namespaces
+scopedInstanceOutsideNamespace.lean:6:0-6:30: error: invalid syntax node kind '«term_+__1»'
+scopedInstanceOutsideNamespace.lean:6:0-6:30: error: Scoped attributes must be used inside namespaces
 scopedInstanceOutsideNamespace.lean:8:2-8:17: error: Scoped attributes must be used inside namespaces
diff --git a/tests/lean/syntaxPrec.lean.expected.out b/tests/lean/syntaxPrec.lean.expected.out
index f11da383fb..aca4eb2177 100644
--- a/tests/lean/syntaxPrec.lean.expected.out
+++ b/tests/lean/syntaxPrec.lean.expected.out
@@ -1,6 +1,6 @@
 syntaxPrec.lean:1:17-1:21: error: unexpected token '<|>'; expected ':'
 [Elab.command] @[term_parser 1000]
-    meta def «termFoo*_» : Lean.ParserDescr✝ :=
+    public meta def «termFoo*_» : Lean.ParserDescr✝ :=
       ParserDescr.node✝ `«termFoo*_» 1022
         (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "foo")
           (ParserDescr.binary✝ `orelse (ParserDescr.nodeWithAntiquot✝ "*" `token.«*» (ParserDescr.symbol✝ "*"))
diff --git a/tests/pkg/misc/Misc/Foo.lean b/tests/pkg/misc/Misc/Foo.lean
index ffc32d2397..f0fc73623b 100644
--- a/tests/pkg/misc/Misc/Foo.lean
+++ b/tests/pkg/misc/Misc/Foo.lean
@@ -8,8 +8,11 @@ local infix:50 " ≺ " => LE.le
 
 #check 1 ≺ 2
 
-local macro "my_refl" : tactic =>
-  `(tactic| rfl)
+-- It is possible to bind a local macro to a public auto param but we must opt into it explicitly by
+-- separating the `macro_rules` and removing the `local` from it.
+local syntax "my_refl" : tactic
+macro_rules
+  | `(tactic| my_refl) => `(tactic| rfl)
 
 def f (x y : Nat) (_h : x = y := by my_refl) := x
 
diff --git a/tests/pkg/misc/lean-toolchain b/tests/pkg/misc/lean-toolchain
new file mode 100644
index 0000000000..dcca6df980
--- /dev/null
+++ b/tests/pkg/misc/lean-toolchain
@@ -0,0 +1 @@
+lean4