From a0b960b77bf48a7a4b604efe7155f0dabe59e7da Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 8 Apr 2023 15:51:17 +0200 Subject: [PATCH] perf: `--profile` can use tracing fast path --- src/Lean/Util/Trace.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean index 75e2d2df38..0e56e8a908 100644 --- a/src/Lean/Util/Trace.lean +++ b/src/Lean/Util/Trace.lean @@ -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