fix: teach Exception.isRuntime to detect nested errors

[eric-wieser]

This PR prevents try swallowing heartbeat errors from nested simp calls, and more generally ensures the isRuntime flag is propagated by throwNestedTacticEx. This prevents the behavior of proofs (especially those using aesop) being affected by the current recursion depth or heartbeat limit.

This breaks a single caller in Mathlib where simp uses a lemma of the form x = f (g x) and stack overflows, which can be fixed by generalizing over g x.

Closes #7811.

[eric-wieser]

changelog-language

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-12-01 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-12-03 04:06:10)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase bf51e1dcfa3322f639cb17e283a9b8caa1c16209 --onto 62f2f9229356039356c0469a46d8ecd77be88e2a. You can force reference manual CI using the force-manual-ci label. (2025-12-09 11:26:56)

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-11490 build failed against this PR. (2025-12-03 04:59:04) View Log
• ✅ Mathlib branch lean-pr-testing-11490 has successfully built against this PR. (2025-12-04 00:51:47) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase bf51e1dcfa3322f639cb17e283a9b8caa1c16209 --onto 1d0d3915ca79d0875a757fc5061121ae9cd58543. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-09 11:26:54)

[Kha]

!bench

[Kha]

!bench

[leanprover-radar]

Benchmark results for 89cebd1 against bf51e1d are in! @Kha