feat: add debug.moduleNameAtTimeout option

closes #3554

src/Lean/CoreM.lean

@@ -244,8 +244,16 @@ protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m
     -- should never be visible to users!
     throw <| Exception.error .missing "elaboration interrupted"
 
+register_builtin_option debug.moduleNameAtTimeout : Bool := {
+  defValue := true
+  group    := "debug"
+  descr    := "include module name in deterministic timeout error messages.\nRemark: we set this option to false to increase the stability of our test suite"
+}
+
 def throwMaxHeartbeat (moduleName : Name) (optionName : Name) (max : Nat) : CoreM Unit := do
-  let msg := s!"(deterministic) timeout at `{moduleName}`, maximum number of heartbeats ({max/1000}) has been reached\nuse `set_option {optionName} <num>` to set the limit\nuse `set_option {diagnostics.name} true` to get diagnostic information"
+  let includeModuleName := debug.moduleNameAtTimeout.get (← getOptions)
+  let atModuleName := if includeModuleName then s!" at `{moduleName}`" else ""
+  let msg := s!"(deterministic) timeout{atModuleName}, maximum number of heartbeats ({max/1000}) has been reached\nuse `set_option {optionName} <num>` to set the limit\nuse `set_option {diagnostics.name} true` to get diagnostic information"
   throw <| Exception.error (← getRef) (MessageData.ofFormat (Std.Format.text msg))
 
 def checkMaxHeartbeatsCore (moduleName : String) (optionName : Name) (max : Nat) : CoreM Unit := do

src/Lean/Elab/SyntheticMVars.lean

@@ -340,26 +340,26 @@ mutual
     Regarding issue #1380, we addressed the issue by avoiding the elaboration postponement step. However, the same issue can happen
     in more complicated scenarios.
     -/
-    try
-      let remainingGoals ← withInfoHole mvarId <| Tactic.run mvarId do
-        withTacticInfoContext tacticCode do
-          -- also put an info node on the `by` keyword specifically -- the token may be `canonical` and thus shown in the info
-          -- view even though it is synthetic while a node like `tacticCode` never is (#1990)
-          withTacticInfoContext tacticCode[0] do
-            evalTactic code
-        synthesizeSyntheticMVars (postpone := .no)
-      unless remainingGoals.isEmpty do
-        if report then
-          reportUnsolvedGoals remainingGoals
+    tryCatchRuntimeEx
+      (do let remainingGoals ← withInfoHole mvarId <| Tactic.run mvarId do
+            withTacticInfoContext tacticCode do
+              -- also put an info node on the `by` keyword specifically -- the token may be `canonical` and thus shown in the info
+              -- view even though it is synthetic while a node like `tacticCode` never is (#1990)
+              withTacticInfoContext tacticCode[0] do
+                evalTactic code
+            synthesizeSyntheticMVars (postpone := .no)
+          unless remainingGoals.isEmpty do
+            if report then
+              reportUnsolvedGoals remainingGoals
+            else
+              throwError "unsolved goals\n{goalsToMessageData remainingGoals}")
+      fun ex => do
+        if report && (← read).errToSorry then
+          for mvarId in (← getMVars (mkMVar mvarId)) do
+            mvarId.admit
+          logException ex
         else
-          throwError "unsolved goals\n{goalsToMessageData remainingGoals}"
-    catch ex =>
-      if report && (← read).errToSorry then
-        for mvarId in (← getMVars (mkMVar mvarId)) do
-          mvarId.admit
-        logException ex
-      else
-        throw ex
+          throw ex
 
   /-- Try to synthesize the given pending synthetic metavariable. -/
   private partial def synthesizeSyntheticMVar (mvarId : MVarId) (postponeOnError : Bool) (runTactics : Bool) : TermElabM Bool := do

src/Lean/Elab/Tactic/Basic.lean

@@ -231,15 +231,15 @@ def closeUsingOrAdmit (tac : TacticM Unit) : TacticM Unit := do
   /- Important: we must define `closeUsingOrAdmit` before we define
      the instance `MonadExcept` for `TacticM` since it backtracks the state including error messages. -/
   let mvarId :: mvarIds ← getUnsolvedGoals | throwNoGoalsToBeSolved
-  try
-    focusAndDone tac
-  catch ex =>
-    if (← read).recover then
-      logException ex
-      admitGoal mvarId
-      setGoals mvarIds
-    else
-      throw ex
+  tryCatchRuntimeEx
+    (focusAndDone tac)
+    fun ex => do
+      if (← read).recover then
+        logException ex
+        admitGoal mvarId
+        setGoals mvarIds
+      else
+        throw ex
 
 instance : MonadBacktrack SavedState TacticM where
   saveState := Tactic.saveState

tests/lean/run/3554.lean

@@ -0,0 +1,37 @@
+def foo : Nat → Nat
+| 0 => 0
+| n+1 => foo n + 1
+
+set_option debug.moduleNameAtTimeout false
+/--
+error: (deterministic) timeout, maximum number of heartbeats (100) has been reached
+use `set_option maxHeartbeats <num>` to set the limit
+use `set_option diagnostics true` to get diagnostic information
+-/
+#guard_msgs in
+set_option maxHeartbeats 100 in
+theorem bar : True := by
+  simp [show foo 1000 = 1000 from rfl]
+
+/--
+info: theorem bar : True :=
+sorryAx True true
+-/
+#guard_msgs in
+#print bar
+
+/--
+error: maximum recursion depth has been reached
+use `set_option maxRecDepth <num>` to increase limit
+use `set_option diagnostics true` to get diagnostic information
+-/
+#guard_msgs in
+theorem bar2 : True := by
+  simp [show foo 1000 = 1000 from rfl]
+
+/--
+info: theorem bar2 : True :=
+sorryAx True true
+-/
+#guard_msgs in
+#print bar2