From d9f007e4ddeff9b194ba799ec6fbf9a87ef8e97e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 17 Apr 2022 15:52:21 -0700
Subject: [PATCH] fix: tactic cache corruption

---
 src/Lean/Elab/Term.lean        | 4 ++--
 src/Lean/Server/Snapshots.lean | 9 +++++++--
 2 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 2a724b677f..b525c0f725 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -125,8 +125,8 @@ structure CacheKey where
   deriving BEq, Hashable, Inhabited
 
 structure Cache where
-   pre  : Std.HashMap CacheKey Snapshot := {}
-   post : Std.HashMap CacheKey Snapshot := {}
+   pre  : Std.PHashMap CacheKey Snapshot := {}
+   post : Std.PHashMap CacheKey Snapshot := {}
    deriving Inhabited
 
 end Tactic
diff --git a/src/Lean/Server/Snapshots.lean b/src/Lean/Server/Snapshots.lean
index b3718ac181..a3d84306b1 100644
--- a/src/Lean/Server/Snapshots.lean
+++ b/src/Lean/Server/Snapshots.lean
@@ -128,17 +128,22 @@ def compileNextCmd (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidget
     return endSnap
   else
     let cmdStateRef ← IO.mkRef { snap.cmdState with messages := msgLog }
+    /- The same snapshot may be executed by different tasks. So, to make sure `elabCommandTopLevel` has exclusive
+       access to the cache, we create a fresh reference here. Before this change, the
+       following `snap.tacticCache.modify` would reset the tactic post cache while another snapshot was still using it. -/
+    let tacticCacheNew ← IO.mkRef (← snap.tacticCache.get)
     let cmdCtx : Elab.Command.Context := {
       cmdPos       := snap.endPos
       fileName     := inputCtx.fileName
       fileMap      := inputCtx.fileMap
-      tacticCache? := some snap.tacticCache
+      tacticCache? := some tacticCacheNew
     }
     let (output, _) ← IO.FS.withIsolatedStreams <| liftM (m := BaseIO) do
       Elab.Command.catchExceptions
         (getResetInfoTrees *> Elab.Command.elabCommandTopLevel cmdStx)
         cmdCtx cmdStateRef
-    snap.tacticCache.modify fun { pre, post } => { pre := post, post := {} }
+    let postNew := (← tacticCacheNew.get).post
+    snap.tacticCache.modify fun { pre, post } => { pre := postNew, post := {} }
     let mut postCmdState ← cmdStateRef.get
     if !output.isEmpty then
       postCmdState := {