refactor: use builtin command elaborators for configuration evaluation (#13779)

This PR makes the command elaborators for configuration evaluation
metaprogramming be builtins, to avoid bootstrapping ABI issues in core
Lean due to the interpreter evaluating large parts of the elaborator
before all builtin initializers are run. (This is part 1; #13780 will be
applied after a stage0 update.)

src/Lean/Elab.lean

@@ -69,4 +69,5 @@ public import Lean.Elab.Parallel
 public import Lean.Elab.BuiltinDo
 public import Lean.Elab.Idbg
 public import Lean.Elab.ConfigEval
+public import Lean.Elab.ConfigEval.Builtins
 public import Lean.Elab.Tactic.Config

src/Lean/Elab/ConfigEval/Builtins.lean

@@ -0,0 +1,219 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+module
+
+prelude
+public import Lean.Elab.ConfigEval.Commands
+public import Lean.Elab.ConfigEval.DeriveEvalConfigItem
+import Lean.Linter.MissingDocs
+
+/-!
+# Builtin elaborators and macros for ConfigEval commands
+
+The elaborators are builtins to avoid bootstrapping issues in core Lean.
+-/
+
+public section
+
+namespace Lean.Elab.ConfigEval
+
+open Meta Term Command
+
+@[builtin_command_elab ensureEvalTermInstance]
+def elabEnsureEvalTermInstance : CommandElab
+  | `(command| $[$vis?:visibility]? $kind:attrKind ensure_eval_term_instance%$tk $t:term) => do
+    let type ← liftTermElabM do withoutErrToSorry <| elabTermAndSynthesize t none
+    ensureEvalTerm vis? kind tk t type
+  | _ => throwUnsupportedSyntax
+
+@[builtin_command_elab ensureEvalExprInstance]
+def elabEnsureEvalExprInstance : CommandElab
+  | `(command| $[$vis?:visibility]? $kind:attrKind ensure_eval_expr_instance%$tk $t:term) => do
+    let type ← liftTermElabM do withoutErrToSorry <| elabTermAndSynthesize t none
+    ensureEvalExpr vis? kind tk t type
+  | _ => throwUnsupportedSyntax
+
+@[builtin_macro ensureEvalTermExprInstances]
+def expandEnsureEvalTermExprInstance : Macro
+  | `(command| $[$vis?:visibility]? $kind:attrKind ensure_eval_term_expr_instances%$tk $t:term) =>
+    `($[$vis?]? $kind ensure_eval_term_instance%$tk $t
+      $[$vis?]? $kind ensure_eval_expr_instance%$tk $t)
+  | _ => Macro.throwUnsupported
+
+@[builtin_command_elab deriveEvalExprUsingMeta]
+def elabDeriveEvalExprUsingMeta : CommandElab
+  | `(command| $[$vis?:visibility]? $kind:attrKind derive_eval_expr_instance_using_meta_eval%$tk $t:term) => do
+    let type ← liftTermElabM do withoutErrToSorry <| elabTermAndSynthesize t none
+    deriveEvalExprUsingMetaEval vis? kind tk t type
+  | _ => throwUnsupportedSyntax
+
+def mkEvalConfigItemView (entries? : Option (TSyntax ``configEntries)) :
+    CommandElabM EvalConfigItemView := do
+  let mut omitFields : Array (Ident × Name) := #[]
+  let mut handlers : Array EvalConfigItemHandler := #[]
+  if let some entries := entries? then
+    match entries with
+    | `(configEntries| where $[$entries:configEntry];*) =>
+      for entry in entries do
+        match entry with
+        | `(configEntry| omit $[$fields],*) =>
+          omitFields := omitFields ++ fields.map fun f => (f, f.getId.eraseMacroScopes)
+        | `(configEntry| option $key:configEntryHandlerKey := $body) =>
+          let (optName, kind) ←
+            match key with
+            | `(configEntryHandlerKey| $opt:ident) => pure (opt.getId.eraseMacroScopes, .exact)
+            | `(configEntryHandlerKey| $opt:ident.*) => pure (opt.getId.eraseMacroScopes, .wildcard)
+            | `(configEntryHandlerKey| *) => pure (.anonymous, .wildcard)
+            | _ => throwUnsupportedSyntax
+          handlers := handlers.push { ref := key, key := optName, body, kind }
+        | _ => throwUnsupportedSyntax
+    | _ => throwUnsupportedSyntax
+  return { omitFields, handlers }
+
+@[builtin_command_elab defEvalConfigItemCmd]
+def elabDefEvalConfigItemCmd : CommandElab
+  | `(command|
+        $[$doc?:docComment]? $[$vis?:visibility]? $kind:attrKind
+        def_eval_config_item%$tk $fn:ident $(binders)* for $struct:ident
+          $[$entries?:configEntries]?) => do
+    let view ← mkEvalConfigItemView entries?
+    defEvalConfigItem doc? vis? kind tk struct fn binders view
+  | _ => throwUnsupportedSyntax
+
+open Linter.MissingDocs in
+@[builtin_missing_docs_handler defEvalConfigItemCmd]
+private def checkDefEvalConfigItemCmd : SimpleHandler := mkSimpleHandler "config elab"
+
+open Lean.Parser.Term in
+private def getBracketedBinderArgs (stx : Syntax) : MacroM (Array Term) :=
+  match stx with
+  | `(bracketedBinderF|($ids:ident* $[: $ty?]? $(_annot?)?)) => return ids
+  | `(bracketedBinderF|{$ids:ident* $[: $_]?})               => return ids
+  | `(bracketedBinderF|⦃$ids:ident* : $_⦄)                    => return ids
+  | `(bracketedBinderF|[$id:ident : $_])                     => return #[id]
+  | `(bracketedBinderF|[$_])                                 => return #[mkHole stx]
+  | _                                                        => Macro.throwErrorAt stx "Unsupported binder"
+
+private def mkElabConfigCmd
+    (monad : Ident)
+    (mkMonadAdapt : Term → MacroM Term)
+    (logExceptionsDefault : Term)
+    (mkLogExceptionsTerm : Term → MacroM Term)
+    (doc? : Option (TSyntax ``Parser.Command.docComment))
+    (vis? : Option (TSyntax ``Parser.Command.visibility))
+    (tk : Syntax)
+    (elabName type : Ident)
+    (binders : TSyntaxArray ``Parser.Term.bracketedBinder)
+    (entries? : Option (TSyntax ``configEntries)) :
+    MacroM Command := do
+  let fnName := mkIdentFrom elabName (elabName.getId ++ `evalConfigItem)
+  let binderArgs ← binders.foldlM (init := #[]) fun args binder => do
+    pure <| args ++ (← getBracketedBinderArgs binder)
+  let cfgIdent := mkIdent `cfg
+  let initIdent := mkIdent `init
+  let logExceptionsIdent := mkIdent `logExceptions
+  let logExceptionsTerm ← mkLogExceptionsTerm logExceptionsIdent
+  let go ← mkMonadAdapt =<< `(EvalConfigItem.setConfig' eval $initIdent $cfgIdent (onErr := onErr) (logExceptions := $logExceptionsTerm))
+  withRef (mkNullNode #[tk, elabName, type]) do
+    `(private local def_eval_config_item $fnName $[$binders]* for $type $[$entries?:configEntries]?
+      $[$doc?:docComment]?
+      $[$vis?:visibility]? def $elabName $[$binders]* ($cfgIdent : Lean.Syntax) ($initIdent : $type := {}) ($logExceptionsIdent : Bool := $logExceptionsDefault) : $monad $type := do
+        let eval : EvalConfigItem $type := @$fnName $binderArgs*
+        let onErr := EvalConfigItem.defaultOnErr (cfgType? := mkConst ``$type)
+        $go:term)
+
+@[builtin_macro declareCoreConfigElab]
+def elabDeclareCoreConfigElab : Macro
+  | `(command|
+        $[$doc?:docComment]? $[$vis?:visibility]?
+        declare_core_config_elab%$tk $elabName:ident $type:ident $(binders)*
+          $[$entries?:configEntries]?) =>
+    mkElabConfigCmd (mkCIdent ``CoreM) pure (mkCIdent ``false)
+      (fun logExceptions => pure logExceptions)
+      doc? vis? tk elabName type binders entries?
+  | _ => Macro.throwUnsupported
+
+open Linter.MissingDocs in
+@[builtin_missing_docs_handler declareCoreConfigElab]
+private def checkDeclareCoreConfigElab : SimpleHandler := mkSimpleHandler "config elab"
+
+@[builtin_macro declareTermConfigElab]
+def elabDeclareTermConfigElab : Macro
+  | `(command|
+        $[$doc?:docComment]? $[$vis?:visibility]?
+        declare_term_config_elab%$tk $elabName:ident $type:ident $(binders)*
+          $[$entries?:configEntries]?) =>
+    mkElabConfigCmd (mkCIdent ``TermElabM) pure (mkCIdent ``true)
+      (fun logExceptions => `($logExceptions && (← read).errToSorry))
+      doc? vis? tk elabName type binders entries?
+  | _ => Macro.throwUnsupported
+
+open Linter.MissingDocs in
+@[builtin_missing_docs_handler elabDeclareTermConfigElab]
+private def checkDeclareTermConfigElab : SimpleHandler := mkSimpleHandler "config elab"
+
+@[builtin_macro declareTacticConfig]
+def elabDeclareTacticConfig : Macro
+  | `(command|
+        $[$doc?:docComment]? $[$vis?:visibility]?
+        declare_config_elab%$tk $elabName:ident $type:ident $(binders)*
+          $[$entries?:configEntries]?) =>
+    mkElabConfigCmd (mkCIdent ``Tactic.TacticM) pure (mkCIdent ``true)
+      (fun logExceptions => `($logExceptions && (← read).recover))
+      doc? vis? tk elabName type binders entries?
+  | _ => Macro.throwUnsupported
+
+open Linter.MissingDocs in
+@[builtin_missing_docs_handler elabDeclareTacticConfig]
+private def checkDeclareTacticConfig : SimpleHandler := mkSimpleHandler "config elab"
+
+@[builtin_macro declareCommandConfig]
+def elabDeclareCommandConfig : Macro
+  | `(command|
+        $[$doc?:docComment]? $[$vis?:visibility]?
+        declare_command_config_elab%$tk $elabName:ident $type:ident $(binders)*
+          $[$entries?:configEntries]?) =>
+    mkElabConfigCmd (mkCIdent ``CommandElabM) (fun eval => `(Command.liftTermElabM $eval)) (mkCIdent ``true)
+      (fun logExceptions => pure logExceptions)
+      doc? vis? tk elabName type binders entries?
+  | _ => Macro.throwUnsupported
+
+open Linter.MissingDocs in
+@[builtin_missing_docs_handler elabDeclareCommandConfig]
+private def checkCommandConfigElab : SimpleHandler := mkSimpleHandler "config elab"
+
+-- TODO(kmill) remove section after stage0 update
+section RemoveMe
+
+set_option compiler.relaxedMetaCheck true
+
+@[command_elab ensureEvalTermInstance]
+meta def elabEnsureEvalTermInstance' := elabEnsureEvalTermInstance
+
+@[command_elab ensureEvalExprInstance]
+meta def elabEnsureEvalExprInstance' := elabEnsureEvalExprInstance
+
+@[macro ensureEvalTermExprInstances]
+meta def expandEnsureEvalTermExprInstance' := expandEnsureEvalTermExprInstance
+
+@[command_elab defEvalConfigItemCmd]
+meta def elabDefEvalConfigItemCmd' := elabDefEvalConfigItemCmd
+
+@[macro declareCoreConfigElab]
+meta def elabDeclareCoreConfigElab' := elabDeclareCoreConfigElab
+
+@[macro declareTermConfigElab]
+meta def elabDeclareTermConfigElab' := elabDeclareTermConfigElab
+
+@[macro declareTacticConfig]
+meta def elabDeclareTacticConfig' := elabDeclareTacticConfig
+
+@[macro declareCommandConfig]
+meta def elabDeclareCommandConfig' := elabDeclareCommandConfig
+
+end RemoveMe
+
+end Lean.Elab.ConfigEval

src/Lean/Elab/ConfigEval/Commands.lean

@@ -6,45 +6,36 @@ Authors: Kyle Miller
 module
 
 prelude
-public import Lean.Elab.ConfigEval.DeriveEvalTerm
+public import Init.Notation
-public meta import Lean.Elab.ConfigEval.DeriveEvalTerm
+
-public import Lean.Elab.ConfigEval.DeriveEvalExpr
+/-!
-public meta import Lean.Elab.ConfigEval.DeriveEvalExpr
+# Syntax definitions for commands
-public import Lean.Elab.ConfigEval.DeriveEvalConfigItem
+
-public meta import Lean.Elab.ConfigEval.DeriveEvalConfigItem
+Elaborators and macros for these notations are defined in `ConfigEval.Builtins`.
-public import Lean.Elab.Tactic.ElabTerm
+-/
-import Lean.Linter.MissingDocs
 
 public section
 
 namespace Lean.Elab.ConfigEval
 
-open Meta Term Command
-
 /--
 `ensure_eval_term_instance t` ensures there is a `ConfigItem.EvalTerm t` instance by
 deriving one or more instances if it needs to.
 -/
-scoped elab vis?:(visibility)? kind:attrKind tk:"ensure_eval_term_instance " t:term : command => do
+scoped syntax (name := ensureEvalTermInstance) (visibility)? attrKind "ensure_eval_term_instance " term : command
-  let type ← liftTermElabM do withoutErrToSorry <| elabTermAndSynthesize t none
-  ensureEvalTerm vis? kind tk t type
 
 /--
 `ensure_eval_expr_instance t` ensures there is a `ConfigItem.EvalExpr t` instance by
 deriving one or more instances if it needs to.
 -/
-scoped elab vis?:(visibility)? kind:attrKind tk:"ensure_eval_expr_instance " t:term : command => do
+scoped syntax (name := ensureEvalExprInstance) (visibility)? attrKind "ensure_eval_expr_instance " term : command
-  let type ← liftTermElabM do withoutErrToSorry <| elabTermAndSynthesize t none
-  ensureEvalExpr vis? kind tk t type
 
 /--
 `ensure_eval_term_expr_instances t` is a macro for running both `ensure_eval_term_instance t`
 and `ensure_eval_expr_instance t`, which ensurs there are `ConfigItem.EvalTerm t` and
 `ConfigItem.EvalExpr t` instances by deriving one or more instances if it needs to.
 -/
-scoped macro vis?:(visibility)? kind:attrKind tk:"ensure_eval_term_expr_instances " t:term : command =>
+scoped syntax (name := ensureEvalTermExprInstances) (visibility)? attrKind "ensure_eval_term_expr_instances " term : command
-  `($[$vis?]? $kind ensure_eval_term_instance%$tk $t
-    $[$vis?]? $kind ensure_eval_expr_instance%$tk $t)
 
 /--
 `derive_eval_expr_instance_using_meta_eval type` defines a `ConfigItem.EvalExpr type` instance
@@ -54,27 +45,19 @@ evaluation does not work and the cost of compilation is acceptible.
 
 This should be avoided in core Lean due to the difficulties it creates for bootstrapping.
 -/
-scoped elab vis?:(visibility)? kind:attrKind tk:"derive_eval_expr_instance_using_meta_eval " t:term : command => do
+scoped syntax (name := deriveEvalExprUsingMeta) (visibility)? attrKind "derive_eval_expr_instance_using_meta_eval " term : command
-  let type ← liftTermElabM do withoutErrToSorry <| elabTermAndSynthesize t none
-  deriveEvalExprUsingMetaEval vis? kind tk t type
 
-section
-open Parser
 /-- `omit f1, f2, f3` disables generating setters for fields `f1`, `f2`, and `f3`
 of the structure. -/
-meta def configEntryOmit := leading_parser
+syntax configEntryOmit := &"omit " ident,+,?
-  nonReservedSymbol "omit " >> sepBy1 ident ", " (allowTrailingSep := true)
+syntax configEntryHandlerKeyPrefix := ident (noWs "." noWs "*")?
-meta def configEntryHandlerKeyPrefix := leading_parser
+syntax configEntryHandlerKeyWildcard := "*"
-  ident >> optional (checkNoWsBefore >> "." >> checkNoWsBefore >> "*")
-meta def configEntryHandlerKeyWildcard := leading_parser
-  "*"
 /--
 - `key` matches a specific key
 - `key.*` matches any keys for which `key` is a proper prefix
 - `*` matches all keys
 -/
-meta def configEntryHandlerKey := leading_parser
+syntax configEntryHandlerKey := configEntryHandlerKeyPrefix <|> configEntryHandlerKeyWildcard
-  configEntryHandlerKeyPrefix <|> configEntryHandlerKeyWildcard
 /--
 `option key := fun cfg item => ...` adds a configuration option named `key` with the given
 expression as its handler. The handler is only called when the key is an exact match.
@@ -83,36 +66,9 @@ The provided value is in `item.value`. Such a handler implies `omit key`.
 `option key.* := fun cfg item => ...` adds configuration options with `key` as a proper prefix.
 The most-specific `*` handler is called if no handlers for exact matches apply.
 -/
-meta def configEntryHandler := leading_parser
+syntax configEntryHandler := &"option " configEntryHandlerKey " := " term
-  nonReservedSymbol "option " >> configEntryHandlerKey >> " := " >> termParser
+syntax configEntry := ppGroup(configEntryOmit <|> configEntryHandler)
-meta def configEntry := leading_parser
+syntax configEntries := " where" sepByIndentSemicolon(configEntry)
-  ppGroup (configEntryOmit <|> configEntryHandler)
-meta def configEntries := leading_parser
-  "where" >> (sepByIndent configEntry "; " (allowTrailingSep := true))
-end
-
-meta def mkEvalConfigItemView (entries? : Option (TSyntax ``configEntries)) :
-    CommandElabM EvalConfigItemView := do
-  let mut omitFields : Array (Ident × Name) := #[]
-  let mut handlers : Array EvalConfigItemHandler := #[]
-  if let some entries := entries? then
-    match entries with
-    | `(configEntries| where $[$entries:configEntry];*) =>
-      for entry in entries do
-        match entry with
-        | `(configEntry| omit $[$fields],*) =>
-          omitFields := omitFields ++ fields.map fun f => (f, f.getId.eraseMacroScopes)
-        | `(configEntry| option $key:configEntryHandlerKey := $body) =>
-          let (optName, kind) ←
-            match key with
-            | `(configEntryHandlerKey| $opt:ident) => pure (opt.getId.eraseMacroScopes, .exact)
-            | `(configEntryHandlerKey| $opt:ident.*) => pure (opt.getId.eraseMacroScopes, .wildcard)
-            | `(configEntryHandlerKey| *) => pure (.anonymous, .wildcard)
-            | _ => throwUnsupportedSyntax
-          handlers := handlers.push { ref := key, key := optName, body, kind }
-        | _ => throwUnsupportedSyntax
-    | _ => throwUnsupportedSyntax
-  return { omitFields, handlers }
 
 /--
 `def_eval_config_item f binders* for struct` defines a `ConfigEval.EvalConfigItem struct` structure named `f`
@@ -133,53 +89,8 @@ The provided value is in `item.value`. Such a handler implies `omit key`.
 - `option key* := fun cfg item => ...` adds configuration options with `key` as a proper prefix.
 The most-specific `*` handler is called if no handlers for exact matches apply.
 -/
-elab (name := defEvalConfigItemCmd)
+syntax (name := defEvalConfigItemCmd) (docComment)? (visibility)? attrKind
-    doc?:(docComment)? vis?:(visibility)? kind:attrKind tk:"def_eval_config_item " fn:ident binders:(bracketedBinder)* " for " struct:ident
+  "def_eval_config_item " ident (bracketedBinder)* " for " ident (configEntries)? : command
-    entries?:(configEntries)? : command => do
-  let view ← mkEvalConfigItemView entries?
-  defEvalConfigItem doc? vis? kind tk struct fn binders view
-
-open Linter.MissingDocs in
-@[builtin_missing_docs_handler defEvalConfigItemCmd]
-private def checkDefEvalConfigItemCmd : SimpleHandler := mkSimpleHandler "config elab"
-
-open Lean.Parser.Term in
-private meta def getBracketedBinderArgs (stx : Syntax) : MacroM (Array Term) :=
-  match stx with
-  | `(bracketedBinderF|($ids:ident* $[: $ty?]? $(_annot?)?)) => return ids
-  | `(bracketedBinderF|{$ids:ident* $[: $_]?})               => return ids
-  | `(bracketedBinderF|⦃$ids:ident* : $_⦄)                    => return ids
-  | `(bracketedBinderF|[$id:ident : $_])                     => return #[id]
-  | `(bracketedBinderF|[$_])                                 => return #[mkHole stx]
-  | _                                                        => Macro.throwErrorAt stx "Unsupported binder"
-
-private meta def mkElabConfigCmd
-    (monad : Ident)
-    (mkMonadAdapt : Term → MacroM Term)
-    (logExceptionsDefault : Term)
-    (mkLogExceptionsTerm : Term → MacroM Term)
-    (doc? : Option (TSyntax ``Parser.Command.docComment))
-    (vis? : Option (TSyntax ``Parser.Command.visibility))
-    (tk : Syntax)
-    (elabName type : Ident)
-    (binders : TSyntaxArray ``Parser.Term.bracketedBinder)
-    (entries? : Option (TSyntax ``Elab.ConfigEval.configEntries)) :
-    MacroM Command := do
-  let fnName := mkIdentFrom elabName (elabName.getId ++ `evalConfigItem)
-  let binderArgs ← binders.foldlM (init := #[]) fun args binder => do
-    pure <| args ++ (← getBracketedBinderArgs binder)
-  let cfgIdent := mkIdent `cfg
-  let initIdent := mkIdent `init
-  let logExceptionsIdent := mkIdent `logExceptions
-  let logExceptionsTerm ← mkLogExceptionsTerm logExceptionsIdent
-  let go ← mkMonadAdapt =<< `(EvalConfigItem.setConfig' eval $initIdent $cfgIdent (onErr := onErr) (logExceptions := $logExceptionsTerm))
-  withRef (mkNullNode #[tk, elabName, type]) do
-    `(private local def_eval_config_item $fnName $[$binders]* for $type $[$entries?:configEntries]?
-      $[$doc?:docComment]?
-      $[$vis?:visibility]? def $elabName $[$binders]* ($cfgIdent : Lean.Syntax) ($initIdent : $type := {}) ($logExceptionsIdent : Bool := $logExceptionsDefault) : $monad $type := do
-        let eval : EvalConfigItem $type := @$fnName $binderArgs*
-        let onErr := EvalConfigItem.defaultOnErr (cfgType? := mkConst ``$type)
-        $go:term)
 
 /--
 `declare_core_config_elab f struct binders* [where ...]` defines a configuration elaborator
@@ -199,16 +110,8 @@ See `ConfigEval.defEvalConfigItemCmd` for further documentation.
 
 See also `declare_term_config_elab`, `declare_config_elab`, and `declare_command_config_elab`.
 -/
-macro (name := elabDeclareCoreConfigElab) doc?:(docComment)? vis?:(visibility)?
+syntax (name := declareCoreConfigElab) (docComment)? (visibility)?
-    tk:"declare_core_config_elab" elabName:ident type:ident binders:(bracketedBinder)*
+  "declare_core_config_elab" ident ident (bracketedBinder)* (configEntries)? : command
-    entries?:(configEntries)? : command => do
-  mkElabConfigCmd (mkCIdent ``CoreM) pure (mkCIdent ``false)
-    (fun logExceptions => pure logExceptions)
-    doc? vis? tk elabName type binders entries?
-
-open Linter.MissingDocs in
-@[builtin_missing_docs_handler elabDeclareCoreConfigElab]
-private def checkDeclareCoreConfigElab : SimpleHandler := mkSimpleHandler "config elab"
 
 /--
 `declare_term_config_elab f struct binders* [where ...]` defines a configuration elaborator
@@ -231,16 +134,8 @@ See `ConfigEval.defEvalConfigItemCmd` for further documentation.
 
 See also `declare_core_config_elab`, `declare_config_elab`, and `declare_command_config_elab`.
 -/
-macro (name := elabDeclareTermConfigElab) doc?:(docComment)? vis?:(visibility)?
+syntax (name := declareTermConfigElab) (docComment)? (visibility)?
-    tk:"declare_term_config_elab" elabName:ident type:ident binders:(bracketedBinder)*
+  "declare_term_config_elab" ident ident (bracketedBinder)* (configEntries)? : command
-    entries?:(configEntries)? : command => do
-  mkElabConfigCmd (mkCIdent ``TermElabM) pure (mkCIdent ``true)
-    (fun logExceptions => `($logExceptions && (← read).errToSorry))
-    doc? vis? tk elabName type binders entries?
-
-open Linter.MissingDocs in
-@[builtin_missing_docs_handler elabDeclareTermConfigElab]
-private def checkDeclareTermConfigElab : SimpleHandler := mkSimpleHandler "config elab"
 
 /--
 `declare_config_elab f struct binders* [where ...]` defines a configuration elaborator
@@ -263,16 +158,8 @@ See `ConfigEval.defEvalConfigItemCmd` for further documentation.
 
 See also `declare_core_config_elab`, `declare_term_config_elab`, and `declare_command_config_elab`.
 -/
-macro (name := elabDeclareTacticConfig) doc?:(docComment)? vis?:(visibility)?
+syntax (name := declareTacticConfig) (docComment)? (visibility)?
-    tk:"declare_config_elab" elabName:ident type:ident binders:(bracketedBinder)*
+  "declare_config_elab" ident ident (bracketedBinder)* (configEntries)? : command
-    entries?:(configEntries)? : command => do
-  mkElabConfigCmd (mkCIdent ``Tactic.TacticM) pure (mkCIdent ``true)
-    (fun logExceptions => `($logExceptions && (← read).recover))
-    doc? vis? tk elabName type binders entries?
-
-open Linter.MissingDocs in
-@[builtin_missing_docs_handler elabDeclareTacticConfig]
-private def checkDeclareTacticConfig : SimpleHandler := mkSimpleHandler "config elab"
 
 /--
 `declare_core_config_elab f struct binders* [where ...]` defines a configuration elaborator
@@ -292,15 +179,7 @@ See `ConfigEval.defEvalConfigItemCmd` for further documentation.
 
 See also `declare_core_config_elab`, `declare_term_config_elab`, and `declare_config_elab`.
 -/
-macro (name := elabDeclareCommandConfig) doc?:(docComment)? vis?:(visibility)?
+syntax (name := declareCommandConfig) (docComment)? (visibility)?
-    tk:"declare_command_config_elab" elabName:ident type:ident binders:(bracketedBinder)*
+  "declare_command_config_elab" ident ident (bracketedBinder)* (configEntries)? : command
-    entries?:(configEntries)? : command => do
-  mkElabConfigCmd (mkCIdent ``CommandElabM) (fun eval => `(Command.liftTermElabM $eval)) (mkCIdent ``true)
-    (fun logExceptions => pure logExceptions)
-    doc? vis? tk elabName type binders entries?
-
-open Linter.MissingDocs in
-@[builtin_missing_docs_handler elabDeclareCommandConfig]
-private def checkCommandConfigElab : SimpleHandler := mkSimpleHandler "config elab"
 
 end Lean.Elab.ConfigEval

src/Lean/Elab/ConfigEval/MetaInstances.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Lean.Elab.ConfigEval.Commands
+public import Lean.Elab.ConfigEval.Builtins -- TODO(kmill): remove after stage0 update
 public import Lean.Elab.ConfigEval.Instances
 public import Lean.Elab.DeprecatedSyntax  -- shake: skip (workaround for command elaborators failing to interpret `deprecatedSyntaxExt`, to be fixed #13108)