max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: handle error in withTraceNode message action (#2364)

Browse source 
* 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>
This commit is contained in:
Wojciech Nawrocki 2023-07-28 08:01:13 -07:00 • committed by GitHub
parent aeb60764c1
commit 74e0f09009
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Util/Trace.lean
View file

@ -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