feat: support all sensible modifiers on (builtin_)initialize

Resolves #1324

src/Init/Meta.lean

@@ -1067,6 +1067,12 @@ def TSepArray.push (sa : TSepArray k sep) (e : TSyntax k) : TSepArray k sep :=
   else 
     { elemsAndSeps := sa.elemsAndSeps.push (mkAtom sep) |>.push e }
 
+instance : EmptyCollection (SepArray sep) where
+  emptyCollection := ⟨∅⟩
+
+instance : EmptyCollection (TSepArray sep k) where
+  emptyCollection := ⟨∅⟩
+
 /-
 We use `CoeTail` here instead of `Coe` to avoid a "loop" when computing `CoeTC`.
 The "loop" is interrupted using the maximum instance size threshold, but it is a performance bottleneck.

src/Lean/Elab/Declaration.lean

@@ -327,35 +327,21 @@ def elabMutual : CommandElab := fun stx => do
     for attrName in toErase do
       Attribute.erase declName attrName
 
-def expandInitCmd (builtin : Bool) : Macro := fun stx => do
-  let optVisibility := stx[0]
-  let optHeader     := stx[2]
-  let doSeq         := stx[3]
-  let attrId        := mkIdentFrom stx <| if builtin then `builtinInit else `init
-  if optHeader.isNone then
-    unless optVisibility.isNone do
-      Macro.throwError "invalid initialization command, 'visibility' modifer is not allowed"
-    `(@[$attrId:ident]def initFn : IO Unit := do $doSeq)
-  else
-    let id   := optHeader[0]
-    let type := optHeader[1][1]
-    if optVisibility.isNone then
+@[builtinMacro Lean.Parser.Command.«initialize»] def expandInitialize : Macro
+  | stx@`($declModifiers:declModifiers $kw:initializeKeyword $[$id? : $type? ←]? $doSeq) => do
+    let attrId := mkIdentFrom stx <| if kw.raw.isToken "initialize" then `init else `builtinInit
+    if let (some id, some type) := (id?, type?) then
+      let `(Parser.Command.declModifiersT| $[$doc?:docComment]? $[@[$attrs?,*]]? $(vis?)? $[unsafe%$unsafe?]?) := stx[0]
+        | Macro.throwErrorAt declModifiers "invalid initialization command, unexpected modifiers"
+      let declModifiers ← `(Parser.Command.declModifiersT| $[$doc?:docComment]? @[$attrId:ident initFn, $(attrs?.getD ∅),*] $(vis?)? $[unsafe%$unsafe?]?)
       `(def initFn : IO $type := do $doSeq
-        @[$attrId:ident initFn] opaque $id : $type)
-    else if optVisibility[0].getKind == ``Parser.Command.private then
-      `(def initFn : IO $type := do $doSeq
-        @[$attrId:ident initFn] private opaque $id : $type)
-    else if optVisibility[0].getKind == ``Parser.Command.protected then
-      `(def initFn : IO $type := do $doSeq
-        @[$attrId:ident initFn] protected opaque $id : $type)
+        $(⟨declModifiers⟩):declModifiers opaque $id : $type)
     else
-      Macro.throwError "unexpected visibility annotation"
-
-@[builtinMacro Lean.Parser.Command.«initialize»] def expandInitialize : Macro :=
-  expandInitCmd (builtin := false)
-
-@[builtinMacro Lean.Parser.Command.«builtin_initialize»] def expandBuiltinInitialize : Macro :=
-  expandInitCmd (builtin := true)
+      if let `(Parser.Command.declModifiersT| ) := declModifiers then
+        `(@[$attrId:ident] def initFn : IO Unit := do $doSeq)
+      else
+        Macro.throwErrorAt declModifiers "invalid initialization command, unexpected modifiers"
+  | _ => Macro.throwUnsupported
 
 builtin_initialize
   registerTraceClass `Elab.axiom

src/Lean/Parser/Command.lean

@@ -132,8 +132,8 @@ def openDecl         := openHiding <|> openRenaming <|> openOnly <|> openSimple
 @[builtinCommandParser] def «open»    := leading_parser withPosition ("open " >> openDecl)
 
 @[builtinCommandParser] def «mutual» := leading_parser "mutual " >> many1 (ppLine >> notSymbol "end" >> commandParser) >> ppDedent (ppLine >> "end") >> terminationSuffix
-@[builtinCommandParser] def «initialize» := leading_parser optional visibility >> "initialize " >> optional (atomic (ident >> Term.typeSpec >> Term.leftArrow)) >> Term.doSeq
-@[builtinCommandParser] def «builtin_initialize» := leading_parser optional visibility >> "builtin_initialize " >> optional (atomic (ident >> Term.typeSpec >> Term.leftArrow)) >> Term.doSeq
+def initializeKeyword := leading_parser "initialize " <|> "builtin_initialize "
+@[builtinCommandParser] def «initialize» := leading_parser declModifiers false >> initializeKeyword >> optional (atomic (ident >> Term.typeSpec >> Term.leftArrow)) >> Term.doSeq
 
 @[builtinCommandParser] def «in»  := trailing_parser withOpen (" in " >> commandParser)
 

stage0/src/stdlib_flags.h

@@ -8,7 +8,7 @@ options get_default_options() {
     // switch to `true` for ABI-breaking changes affecting meta code
     opts = opts.update({"interpreter", "prefer_native"}, false);
     // switch to `true` for changing built-in parsers used in quotations
-    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
+    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
     opts = opts.update({"pp", "rawOnError"}, true);
 #endif
     return opts;