try marking environment persistent after each command

leanprover · Jun 22, 2024 · a08eebd · a08eebd
1 parent 3345a74
commit a08eebd
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/Lean/Language/Lean.lean b/src/Lean/Language/Lean.lean
@@ -571,6 +571,8 @@ where
       let postNew := (← tacticCacheNew.get).post
       tacticCache.modify fun _ => { pre := postNew, post := {} }
       let cmdState ← cmdStateRef.get
+      -- TODO: should not be done in server mode
+      let cmdState := Runtime.markPersistent cmdState
       let mut messages := cmdState.messages
       if !output.isEmpty then
         messages := messages.add {