Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Recursion depth errors are silenced inconsistently by tactics, and as a result are sometimes caught by try and sometimes not.

Context

Non-erroring tactic behavior should not depend on resource constraints such as heartbeats or recursion depth limits, as these are implementation details that can change between systems and in tactic refactoring.

As the decision has already been made for try to not to catch such errors, other tactics should certainly not do so when catching and rethrowing errors.

Steps to Reproduce

Run

import Lean

set_option maxRecDepth 200 -- low to make this fast

example : 1 = sorry := by
  -- recursion depth error is silenced (bad)
  try simp [← Nat.add_zero 1]
  -- recursion depth error is not silenced (good)
  try repeat rw [← Nat.add_zero 1]
  sorry

Expected behavior: Both trys should result in non-silenced recursion depth errors

Actual behavior: Only the second one is

Versions

Lean 4.19.0-rc2
Target: x86_64-unknown-linux-gnu

Additional Information

The cause of this is the following lines, which discard the top-level .tagged `runtime.* part of the message

which are read by

See also leanprover-community/aesop#211

Impact

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