Commit 2026-09-04 15:28 95707487

fix(TacticAnalysis): discard messages logged by re-run tactics (#43397) ContextInfo.runTacticCode migrates whatever the tactic under test logs (e.g. "Try this" suggestions) into the command's message log, so it gets reported as if a tactic analysis pass had produced the log message. There are a couple of exceptions: rwMerge and verifyTryThisSuggestions. They worked around the default setup by manually saving and restoring the log (I see comments like "Drop any messages, since they will appear as if they are genuine errors"). This PR restores the log inside runTacticCode itself, so a pass only ever reports what it logs on its own. runTacticCodeCapturingInfoTree is unchanged, for callers that want to inspect the output of re-running a tactic. AFAICS, runTacticCode has no callers outside the tactic analysis framework, and all of them only read the returned goals. Also, drop the hand-rolled save-the-log-and-restore-it-later juggling around runTacticCode in rwMerge and verifyTryThisSuggestions, since it's no longer needed. (verifyTryThisSuggestions keeps its other restore, the one around runTacticCodeCapturingInfoTree, on purpose: that call wants the re-run's info trees.) One existing expectation changes: the tryAtEachStepSimpAllSuggestions test no longer shows the Try this: simp_all only [p] line, which came from the re-run simp_all? rather than from the pass. A new test checks that a re-run tactic's message doesn't get reported.