`try ... catch` is not infotree-safe in `TacticM`

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

Currently, try ... catch blocks in TacticM (and definitions built on them, such as tryTactic) are liable to produce RPC errors in the infoview when a failure is encountered. This is because Tactic.tryCatch rewinds the tactic state on failure, but neither saves the infotree context nor rewinds the infotrees. As such, any new metavariables which are introduced to the infotree during the try block create RPC errors in the infoview.

It would be nice if the default behavior of try ... catch blocks in tactic code was "safe" with respect to infotree contexts, either by rewinding the infotrees or saving the infotree context on error (preferably the latter).

Context

This was the cause of this rw ... at * RPC error reported on zulip. withLocation invokes tryTactic when given a wildcard location, and the rewrite failure caused an RPC error on rewrite rules which involved _'s.

Steps to Reproduce

MWE:

import Lean

open Lean Meta Elab Tactic in
elab "test " stx:term : tactic => withMainContext do
  try
    discard <| elabTerm stx none
    failure
  catch _ =>
    throwError "failed"

example : True := by
  test _ + _ -- Place cursor before last `_`; observe the following error in the infoview:

Error updating: Error fetching goals: Rpc error: InternalError: unknown metavariable '?_uniq.2936'

Expected behavior: No RPC error; preferably, we could view the infotree that was generated during elaboration.

Actual behavior: The RPC error shown above.

Versions

4.3.0-rc2; macOS and Lean web.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start with Tactic.tryCatch and the tryTactic path described in the issue, including withLocation for wildcard locations. Reproduce the minimal example in a Lean file and inspect how failed elaboration affects infotree state. Done means the example no longer produces an infoview RPC error and the generated infotree remains usable after the failure.