diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index 4e1d393c8c4b..2eaa92138232 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -309,7 +309,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} ` to set the limit.\ {useDiagnosticMsg}" @@ -396,8 +396,7 @@ export Core (CoreM mkFreshUserName checkSystem withCurrHeartbeats) 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 + | Exception.error _ (.tagged tag _) => (`runtime.maxHeartbeats).isPrefixOf tag | _ => false /-- Creates the expression `d → b` -/