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)