max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: use builtin command elaborators for configuration evaluation (part 2) (#13780)

Browse source 
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.
This commit is contained in:
Kyle Miller 2026-05-19 11:16:21 -07:00 • committed by GitHub
parent 731d0c4878
commit 29adf42309
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 5 additions and 33 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/Elab/ConfigEval.lean
View file

@ -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

31
src/Lean/Elab/ConfigEval/Builtins.lean
View file

@ -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

4
src/Lean/Elab/ConfigEval/MetaInstances.lean
View file

@ -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