feat: push/pop tactic API

[kmill]

Adds pushGoal/pushGoals and popGoal for manipulating the goal state. These are an alternative to replaceMainGoal and getMainGoal, and with them you don't need to worry about making sure nothing clears assigned metavariables from the goal list between assigning the main goal and using replaceMainGoal.

Modifies closeMainGoalUsing, which is like a TacticM version of liftMetaTactic. Now the callback is run in a context where the main goal is removed from the goal list, and the callback is free to modify the goal list. Furthermore, the checkUnassigned argument has been replaced with checkNewUnassigned, which checks whether the value assigned to the goal has any new metavariables, relative to the start of execution of the callback. This API is sufficient for the exact tactic for example.

Modifies withCollectingNewGoalsFrom to take the parentTag argument explicitly rather than indirectly via getMainTag. This is needed when used under closeMainGoalUsing.

Modifies elabTermWithHoles to optionally take parentTag?. It defaults to getMainTag if it is none.

Renames Tactic.tryCatch to Tactic.tryCatchRestore, and adds a Tactic.tryCatch that doesn't do backtracking.

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-5720 has successfully built against this PR. (2024-10-15 08:27:53) View Log
• 💥 Mathlib branch lean-pr-testing-5720 build failed against this PR. (2024-10-15 17:30:25) View Log
• ✅ Mathlib branch lean-pr-testing-5720 has successfully built against this PR. (2024-10-15 18:48:46) View Log
• ✅ Mathlib branch lean-pr-testing-5720 has successfully built against this PR. (2024-10-16 01:38:52) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 831fa0899fd0397e5a8f21abc2c5fcee8883c481 --onto 225e08965d644715e8961cd205ffedf1cf7d24c2. (2024-10-16 03:50:43)