From 29adf42309c7e11a7de10440c8bcc77c08ef7072 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Tue, 19 May 2026 11:16:21 -0700 Subject: [PATCH] refactor: use builtin command elaborators for configuration evaluation (part 2) (#13780) This PR is part 2 to #13779. It completes the transition of the configuration evaluation metaprograms into being builtin elaborators. After this, building stage1 will not invoke the interpreter when generating configuration evaluators. A tradeoff is that changes to ConfigEval will not affect stage1 builds, but these changes ought to be infrequent. --- src/Lean/Elab/ConfigEval.lean | 3 ++ src/Lean/Elab/ConfigEval/Builtins.lean | 31 --------------------- src/Lean/Elab/ConfigEval/MetaInstances.lean | 4 +-- 3 files changed, 5 insertions(+), 33 deletions(-) diff --git a/src/Lean/Elab/ConfigEval.lean b/src/Lean/Elab/ConfigEval.lean index 2ece69cdec..b192405488 100644 --- a/src/Lean/Elab/ConfigEval.lean +++ b/src/Lean/Elab/ConfigEval.lean @@ -9,6 +9,9 @@ prelude public import Lean.Elab.ConfigEval.Types public import Lean.Elab.ConfigEval.Basic public import Lean.Elab.ConfigEval.Commands +public import Lean.Elab.ConfigEval.DeriveEvalTerm +public import Lean.Elab.ConfigEval.DeriveEvalExpr +public import Lean.Elab.ConfigEval.DeriveEvalConfigItem public import Lean.Elab.ConfigEval.Instances public import Lean.Elab.ConfigEval.MetaInstances public import Lean.Elab.ConfigEval.Extra diff --git a/src/Lean/Elab/ConfigEval/Builtins.lean b/src/Lean/Elab/ConfigEval/Builtins.lean index a9fa3765d6..27fb5dac6b 100644 --- a/src/Lean/Elab/ConfigEval/Builtins.lean +++ b/src/Lean/Elab/ConfigEval/Builtins.lean @@ -185,35 +185,4 @@ 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/MetaInstances.lean b/src/Lean/Elab/ConfigEval/MetaInstances.lean index a8f15e3347..58b93beff9 100644 --- a/src/Lean/Elab/ConfigEval/MetaInstances.lean +++ b/src/Lean/Elab/ConfigEval/MetaInstances.lean @@ -7,9 +7,9 @@ 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) +import Lean.Elab.ConfigEval.DeriveEvalTerm +import Lean.Elab.ConfigEval.DeriveEvalExpr /-! # Derived evaluator instances for built-in Meta types