throwNestedTacticEx silences runtime errors

[eric-wieser]

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

lean4/src/Lean/Meta/Tactic/Simp/Main.lean

Lines 807 to 814 in 5f2f010

	tryCatchRuntimeEx
	(simp e)
	fun ex => do
	reportDiag (← get).diag
	if ex.isRuntime then
	throwNestedTacticEx `simp ex
	else
	throw ex

which are read by

lean4/src/Lean/CoreM.lean

Lines 514 to 519 in fafd381

	/--
	Return true if `ex` was generated by `throwMaxHeartbeat`.
	This function is a bit hackish. The heartbeat exception should probably be an internal exception.
	We used a similar hack at `Exception.isMaxRecDepth` -/
	def Exception.isMaxHeartbeat (ex : Exception) : Bool :=
	ex matches Exception.error _ (.tagged `runtime.maxHeartbeats _)

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.

[Kha]

Likely throwNestedTacticEx should move these tags to the outside. @eric-wieser Since you implemented the tags, do you want to take this :) ?

[eric-wieser]

That was the quick hack I had in mind too :)

An alternative would be to change Exception.isMaxHeartbeat to match any nested tags anywhere rather than just top-level tags, which would also cover any user concatenation of errors, but this might be surprising behavior.

[eric-wieser]

#9653 seems related here.

[eric-wieser]

Hopefully fixed in #11490