fix: use MessageData.tagged to mark maxHeartbeat exceptions (leanpr…

…over#5566)

Fixes leanprover#5565, by using tags instead of trying to string match on a
`MessageData`. This ends up reverting some unwanted test output changes
from leanprover#4781 too.

This changes `isMaxRecDepth` for good measure too.

This was a regression in Lean 4.11.0, so may be worth backporting to
4.12.x, if not also 4.11.x.

src/Lean/CoreM.lean

@@ -302,7 +302,7 @@ register_builtin_option debug.moduleNameAtTimeout : Bool := {
 def throwMaxHeartbeat (moduleName : Name) (optionName : Name) (max : Nat) : CoreM Unit := do
   let includeModuleName := debug.moduleNameAtTimeout.get (← getOptions)
   let atModuleName := if includeModuleName then s!" at `{moduleName}`" else ""
-  throw <| Exception.error (← getRef) m!"\
+  throw <| Exception.error (← getRef) <| .tagged `runtime.maxHeartbeats m!"\
     (deterministic) timeout{atModuleName}, maximum number of heartbeats ({max/1000}) has been reached\n\
     Use `set_option {optionName} <num>` to set the limit.\
     {useDiagnosticMsg}"
@@ -388,10 +388,7 @@ export Core (CoreM mkFreshUserName checkSystem withCurrHeartbeats)
   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 :=
-  match ex with
-  | Exception.error _ (MessageData.ofFormatWithInfos ⟨Std.Format.text msg, _⟩) =>
-    "(deterministic) timeout".isPrefixOf msg
-  | _ => false
+  ex matches Exception.error _ (.tagged `runtime.maxHeartbeats _)
 
 /-- Creates the expression `d → b` -/
 def mkArrow (d b : Expr) : CoreM Expr :=

src/Lean/Exception.lean

@@ -120,7 +120,7 @@ instance [BEq α] [Hashable α] [Monad m] [STWorld ω m] [MonadRecDepth m] : Mon
 Throw a "maximum recursion depth has been reached" exception using the given reference syntax.
 -/
 def throwMaxRecDepthAt [MonadError m] (ref : Syntax) : m α :=
-  throw <| .error ref (MessageData.ofFormat (Std.Format.text maxRecDepthErrorMessage))
+  throw <| .error ref (.tagged `runtime.maxRecDepth <| MessageData.ofFormat (Std.Format.text maxRecDepthErrorMessage))
 
 /--
 Return true if `ex` was generated by `throwMaxRecDepthAt`.
@@ -129,9 +129,7 @@ but it is also produced by `MacroM` which implemented in the prelude, and intern
 been defined yet.
 -/
 def Exception.isMaxRecDepth (ex : Exception) : Bool :=
-  match ex with
-  | error _ (MessageData.ofFormatWithInfos ⟨Std.Format.text msg, _⟩) => msg == maxRecDepthErrorMessage
-  | _ => false
+  ex matches error _ (.tagged `runtime.maxRecDepth _)
 
 /--
 Increment the current recursion depth and then execute `x`.

tests/lean/run/3554.lean

@@ -7,10 +7,6 @@ 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.
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
----
-error: (deterministic) timeout, maximum number of heartbeats (100) has been reached
-Use `set_option maxHeartbeats <num>` to set the limit.
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 set_option maxHeartbeats 100 in

tests/lean/run/5565.lean

@@ -0,0 +1,9 @@
+import Lean.Elab.Command
+
+run_meta do
+  Lean.tryCatchRuntimeEx
+    (do
+      Lean.Core.throwMaxHeartbeat `foo `bar 200)
+    (fun e =>
+      unless e.isMaxHeartbeat do
+        throwError "Not a max heartbeat error:{Lean.indentD e.toMessageData}")

tests/lean/run/isDefEqProjIssue.lean

@@ -54,34 +54,6 @@ where
 error: (deterministic) timeout at `whnf`, maximum number of heartbeats (400) has been reached
 Use `set_option maxHeartbeats <num>` to set the limit.
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
----
-error: (deterministic) timeout at `isDefEq`, maximum number of heartbeats (400) has been reached
-Use `set_option maxHeartbeats <num>` to set the limit.
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
----
-error: (deterministic) timeout at `elaborator`, maximum number of heartbeats (400) has been reached
-Use `set_option maxHeartbeats <num>` to set the limit.
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
----
-error: (deterministic) timeout at `isDefEq`, maximum number of heartbeats (400) has been reached
-Use `set_option maxHeartbeats <num>` to set the limit.
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
----
-error: (deterministic) timeout at `isDefEq`, maximum number of heartbeats (400) has been reached
-Use `set_option maxHeartbeats <num>` to set the limit.
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
----
-error: (deterministic) timeout at `elaborator`, maximum number of heartbeats (400) has been reached
-Use `set_option maxHeartbeats <num>` to set the limit.
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
----
-error: (deterministic) timeout at `isDefEq`, maximum number of heartbeats (400) has been reached
-Use `set_option maxHeartbeats <num>` to set the limit.
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
----
-error: (deterministic) timeout at `whnf`, maximum number of heartbeats (400) has been reached
-Use `set_option maxHeartbeats <num>` to set the limit.
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 set_option backward.isDefEq.lazyWhnfCore false in

tests/lean/tcloop.lean.expected.out

@@ -1,3 +1,6 @@
-tcloop.lean:14:2-14:15: error: (deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached
+tcloop.lean:14:2-14:15: error: failed to synthesize
+  B Nat
+(deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached
 Use `set_option synthInstance.maxHeartbeats <num>` to set the limit.
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Additional diagnostic information may be available using the `set_option diagnostics true` command.