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

perf: --profile can use tracing fast path

Browse source
This commit is contained in:
Sebastian Ullrich 2023-04-08 15:51:17 +02:00
parent 41a3ebed02
commit a0b960b77b
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -184,7 +184,7 @@ def withTraceNode [MonadExcept ε m] [MonadLiftT BaseIO m] (cls : Name) (msg : E
(collapsed := true) : m α := do
let opts ← getOptions
let clsEnabled ← isTracingEnabledFor cls
unless clsEnabled || profiler.get opts || trace.profiler.get opts do
unless clsEnabled || trace.profiler.get opts do
return (← k)
let oldTraces ← getResetTraces
let (res, secs) ← withSeconds <| observing k
@ -267,7 +267,7 @@ TODO: find better name for this function.
def withTraceNodeBefore [MonadRef m] [AddMessageContext m] [MonadOptions m] [MonadExcept ε m] [MonadLiftT BaseIO m] [ExceptToEmoji ε α] (cls : Name) (msg : m MessageData) (k : m α) (collapsed := true) : m α := do
let opts ← getOptions
let clsEnabled ← isTracingEnabledFor cls
unless clsEnabled || profiler.get opts || trace.profiler.get opts do
unless clsEnabled || trace.profiler.get opts do
return (← k)
let oldTraces ← getResetTraces
let ref ← getRef