Commit 2025-11-11 10:35 d6b397a9

fix: panic in tactic analysis framework (#31472) The test added in this PR causes a panic on current mathlib, the panic being this one: https://github.com/leanprover-community/mathlib4/blob/32fb6832e1009174e2787a2cbbc7669399175c61/Mathlib/Lean/ContextInfo.lean#L72 This PR fixes the panic. The issue is in the tactic analysis framework's terminalReplacement linter builder. The idea with terminalReplacement is to try all old_tactic occurrences to see if swapping in new_tactic finishes at that point. If new_tactic works but doesn't finish it is supposed to print the new goal(s) produced by new_tactic; this is the case that was causing the panic. The issue was that the MetaM call(s) to infer the type(s) of the new goal(s) were being routed through the Lean.Elab.ContextInfo.runTactic function, which panics if (as will typically be the case) one of these goals represents nontrivial progress from the previous goal state. I have fixed this by storing the types of the new goals at the time they are generated, so we don't need Lean.Elab.ContextInfo.runTactic to cook up a new MetaM instance.