From cceb88840bf98fc3ed01252ce0349dba7a0ea561 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 15 Oct 2024 18:04:39 +0200 Subject: [PATCH] fix: don't block on snapshot tree if tracing is not enabled --- src/Lean/Elab/Command.lean | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index 47bc7dbdbae4..e3d867a45520 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -532,11 +532,12 @@ def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do pro let mut msgs := (← get).messages for tree in (← getInfoTrees) do trace[Elab.info] (← tree.format) - if let some snap := (← read).snap? then - -- We can assume that the root command snapshot is not involved in parallelism yet, so this - -- should be true iff the command supports incrementality - if (← IO.hasFinished snap.new.result) then - liftCoreM <| Language.ToSnapshotTree.toSnapshotTree snap.new.result.get |>.trace + if (← isTracingEnabledFor `Elab.snapshotTree) then + if let some snap := (← read).snap? then + -- We can assume that the root command snapshot is not involved in parallelism yet, so this + -- should be true iff the command supports incrementality + if (← IO.hasFinished snap.new.result) then + liftCoreM <| Language.ToSnapshotTree.toSnapshotTree snap.new.result.get |>.trace modify fun st => { st with messages := initMsgs ++ msgs infoState := { st.infoState with trees := initInfoTrees ++ st.infoState.trees }