From 79583d63f3231f0b5c84922292908d7405309486 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 16 Oct 2024 15:12:42 +0200 Subject: [PATCH] fix: don't block on snapshot tree if tracing is not enabled (#5736) While there appears to be an underlying issue of blocking tasks that this specific PR is not resolving, it should alleviate the problems described in https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/reliable.20file.20desync.20on.20Linux.20Mint as it effectively reverts the relevant change introduced in 4.13.0-rc1 when the trace option is not set. --- 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 f26af72750..e73c8c6751 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 }