From 2bbf5db04fc536a192756091ee9f640b6ddf489f Mon Sep 17 00:00:00 2001 From: Anne Baanen Date: Fri, 12 Sep 2025 18:30:44 +0200 Subject: [PATCH] fix: add infotree context to `classical` tactic (#10332) This PR ensures that the infotree recognizes `Classical.propDecidable` as an instance, when below a `classical` tactic. The `classical` tactic modifies the environment that the subsequent sequence of tactics runs in (by making `Classical.propDecidable` an instance). However, it does not add a corresponding `InfoTree.context` node, so its effects are not visible when we want to replay a tactic sequence (for example when running a tactic in the tactic analysis framework). We should add a call to `Lean.Elab.withSafeInfoContext` to remedy this issue. There are two potential places to add this class: in the meta-level `Lean.Elab.Tactic.classical` wrapper, or the tactic-level `evalClassical` tactic elaborator. I chose the latter since meta-level does not have access to info tree operations (unless we add many parameters to `Lean.Elab.Tactic.classical`: `[MonadNameGenerator m] [MonadOptions m] [MonadMCtx m] [MonadResolveName m] [MonadFileMap m]`). A testcase that uses the tactic analysis framework is available here: https://github.com/leanprover-community/mathlib4/pull/29501 --- src/Lean/Elab/Tactic/Classical.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Lean/Elab/Tactic/Classical.lean b/src/Lean/Elab/Tactic/Classical.lean index 2d3e54126f..6abca3eecc 100644 --- a/src/Lean/Elab/Tactic/Classical.lean +++ b/src/Lean/Elab/Tactic/Classical.lean @@ -30,6 +30,7 @@ def classical [Monad m] [MonadEnv m] [MonadFinally m] [MonadLiftT MetaM m] (t : @[builtin_tactic Lean.Parser.Tactic.classical, builtin_incremental] def evalClassical : Tactic := fun stx => - classical <| Term.withNarrowedArgTacticReuse (argIdx := 1) Elab.Tactic.evalTactic stx + classical <| withSaveInfoContext <| + Term.withNarrowedArgTacticReuse (argIdx := 1) Elab.Tactic.evalTactic stx end Lean.Elab.Tactic