From e38c6983924919aa4f9d04f9ce294407d94538a6 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Tue, 19 May 2026 09:08:11 -0700 Subject: [PATCH] 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 | 1 + src/Lean/Elab/ConfigEval/Builtins.lean | 219 ++++++++++++++++++++ src/Lean/Elab/ConfigEval/Commands.lean | 177 +++------------- src/Lean/Elab/ConfigEval/MetaInstances.lean | 1 + 4 files changed, 249 insertions(+), 149 deletions(-) create mode 100644 src/Lean/Elab/ConfigEval/Builtins.lean diff --git a/src/Lean/Elab.lean b/src/Lean/Elab.lean index 4dbee43305..4d73863fff 100644 --- a/src/Lean/Elab.lean +++ b/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 diff --git a/src/Lean/Elab/ConfigEval/Builtins.lean b/src/Lean/Elab/ConfigEval/Builtins.lean new file mode 100644 index 0000000000..a9fa3765d6 --- /dev/null +++ b/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 diff --git a/src/Lean/Elab/ConfigEval/Commands.lean b/src/Lean/Elab/ConfigEval/Commands.lean index fdc7e708f1..9d84e7d268 100644 --- a/src/Lean/Elab/ConfigEval/Commands.lean +++ b/src/Lean/Elab/ConfigEval/Commands.lean @@ -6,45 +6,36 @@ Authors: Kyle Miller module prelude -public import Lean.Elab.ConfigEval.DeriveEvalTerm -public meta import Lean.Elab.ConfigEval.DeriveEvalTerm -public import Lean.Elab.ConfigEval.DeriveEvalExpr -public meta import Lean.Elab.ConfigEval.DeriveEvalExpr -public import Lean.Elab.ConfigEval.DeriveEvalConfigItem -public meta import Lean.Elab.ConfigEval.DeriveEvalConfigItem -public import Lean.Elab.Tactic.ElabTerm -import Lean.Linter.MissingDocs +public import Init.Notation + +/-! +# Syntax definitions for commands + +Elaborators and macros for these notations are defined in `ConfigEval.Builtins`. +-/ 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 - let type ← liftTermElabM do withoutErrToSorry <| elabTermAndSynthesize t none - ensureEvalTerm vis? kind tk t type +scoped syntax (name := ensureEvalTermInstance) (visibility)? attrKind "ensure_eval_term_instance " term : command /-- `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 - let type ← liftTermElabM do withoutErrToSorry <| elabTermAndSynthesize t none - ensureEvalExpr vis? kind tk t type +scoped syntax (name := ensureEvalExprInstance) (visibility)? attrKind "ensure_eval_expr_instance " term : command /-- `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 => - `($[$vis?]? $kind ensure_eval_term_instance%$tk $t - $[$vis?]? $kind ensure_eval_expr_instance%$tk $t) +scoped syntax (name := ensureEvalTermExprInstances) (visibility)? attrKind "ensure_eval_term_expr_instances " term : command /-- `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 - let type ← liftTermElabM do withoutErrToSorry <| elabTermAndSynthesize t none - deriveEvalExprUsingMetaEval vis? kind tk t type +scoped syntax (name := deriveEvalExprUsingMeta) (visibility)? attrKind "derive_eval_expr_instance_using_meta_eval " term : command -section -open Parser /-- `omit f1, f2, f3` disables generating setters for fields `f1`, `f2`, and `f3` of the structure. -/ -meta def configEntryOmit := leading_parser - nonReservedSymbol "omit " >> sepBy1 ident ", " (allowTrailingSep := true) -meta def configEntryHandlerKeyPrefix := leading_parser - ident >> optional (checkNoWsBefore >> "." >> checkNoWsBefore >> "*") -meta def configEntryHandlerKeyWildcard := leading_parser - "*" +syntax configEntryOmit := &"omit " ident,+,? +syntax configEntryHandlerKeyPrefix := ident (noWs "." noWs "*")? +syntax configEntryHandlerKeyWildcard := "*" /-- - `key` matches a specific key - `key.*` matches any keys for which `key` is a proper prefix - `*` matches all keys -/ -meta def configEntryHandlerKey := leading_parser - configEntryHandlerKeyPrefix <|> configEntryHandlerKeyWildcard +syntax configEntryHandlerKey := 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 - nonReservedSymbol "option " >> configEntryHandlerKey >> " := " >> termParser -meta def configEntry := leading_parser - 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 } +syntax configEntryHandler := &"option " configEntryHandlerKey " := " term +syntax configEntry := ppGroup(configEntryOmit <|> configEntryHandler) +syntax configEntries := " where" sepByIndentSemicolon(configEntry) /-- `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) - doc?:(docComment)? vis?:(visibility)? kind:attrKind tk:"def_eval_config_item " fn:ident binders:(bracketedBinder)* " for " struct:ident - 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) +syntax (name := defEvalConfigItemCmd) (docComment)? (visibility)? attrKind + "def_eval_config_item " ident (bracketedBinder)* " for " ident (configEntries)? : command /-- `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)? - tk:"declare_core_config_elab" elabName:ident type:ident binders:(bracketedBinder)* - 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" +syntax (name := declareCoreConfigElab) (docComment)? (visibility)? + "declare_core_config_elab" ident ident (bracketedBinder)* (configEntries)? : command /-- `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)? - tk:"declare_term_config_elab" elabName:ident type:ident binders:(bracketedBinder)* - 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" +syntax (name := declareTermConfigElab) (docComment)? (visibility)? + "declare_term_config_elab" ident ident (bracketedBinder)* (configEntries)? : command /-- `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)? - tk:"declare_config_elab" elabName:ident type:ident binders:(bracketedBinder)* - 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" +syntax (name := declareTacticConfig) (docComment)? (visibility)? + "declare_config_elab" ident ident (bracketedBinder)* (configEntries)? : command /-- `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)? - tk:"declare_command_config_elab" elabName:ident type:ident binders:(bracketedBinder)* - 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" +syntax (name := declareCommandConfig) (docComment)? (visibility)? + "declare_command_config_elab" ident ident (bracketedBinder)* (configEntries)? : command end Lean.Elab.ConfigEval diff --git a/src/Lean/Elab/ConfigEval/MetaInstances.lean b/src/Lean/Elab/ConfigEval/MetaInstances.lean index 9ab551fbd5..a8f15e3347 100644 --- a/src/Lean/Elab/ConfigEval/MetaInstances.lean +++ b/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)