From 74e0f09009377d2e85ee2cc4fa704bad47383dd5 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <t-wnawrocki@microsoft.com>
Date: Fri, 28 Jul 2023 08:01:13 -0700
Subject: [PATCH] fix: handle error in withTraceNode message action (#2364)

* fix: handle error in withTrace message action

* Update src/Lean/Util/Trace.lean

Co-authored-by: Gabriel Ebner <gebner@gebner.org>

* Update Trace.lean

---------

Co-authored-by: Gabriel Ebner <gebner@gebner.org>
---
 src/Lean/Util/Trace.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean
index 0e56e8a908..17530a4d92 100644
--- a/src/Lean/Util/Trace.lean
+++ b/src/Lean/Util/Trace.lean
@@ -193,7 +193,7 @@ def withTraceNode [MonadExcept ε m] [MonadLiftT BaseIO m] (cls : Name) (msg : E
     modifyTraces (oldTraces ++ ·)
     return (← MonadExcept.ofExcept res)
   let ref ← getRef
-  let mut m ← msg res
+  let mut m ← try msg res catch _ => pure m!"<exception thrown while producing trace node message>"
   if profiler.get opts || aboveThresh then
     m := m!"[{secs}s] {m}"
   addTraceNode oldTraces cls ref m collapsed