hack: disable snapshotting

opencompl · Nov 1, 2024 · 7a8244a · 7a8244a
1 parent 8c7f748
commit 7a8244a
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
@@ -532,12 +532,14 @@ 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 (← 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 }