From 7a8244a251ca2b68384a661d6a922c801848c469 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Thu, 31 Oct 2024 19:25:33 -0500
Subject: [PATCH] hack: disable snapshotting

---
 src/Lean/Elab/Command.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 296a2bede02f..119f8942a317 100644
--- 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 }