From dfe8ad0ac23ea368fdaecc2fec44c5d5206f57bc Mon Sep 17 00:00:00 2001
From: Auguste Poiroux <augustepoiroux@gmail.com>
Date: Mon, 17 Nov 2025 09:38:41 +0100
Subject: [PATCH 01/13] Improve `LocalContext` and `LocalInstance` extraction
 for sorries

---
 REPL/Main.lean      |  8 ++------
 REPL/Snapshots.lean | 49 +++++++++++++++++++++++++++------------------
 2 files changed, 32 insertions(+), 25 deletions(-)

diff --git a/REPL/Main.lean b/REPL/Main.lean
index 9b36b27d..c1b0c717 100644
--- a/REPL/Main.lean
+++ b/REPL/Main.lean
@@ -102,11 +102,7 @@ def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Op
       fun ⟨ctx, g, pos, endPos⟩ => do
         let (goal, proofState) ← match g with
         | .tactic g => do
-          let lctx ← ctx.runMetaM {} do
-              match ctx.mctx.findDecl? g with
-              | some decl => return decl.lctx
-              | none => throwError "unknown metavariable '{g}'"
-          let s ← ProofSnapshot.create ctx lctx env? [g] rootGoals?
+          let s ← ProofSnapshot.create ctx none env? [g] rootGoals?
           pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s)
         | .term lctx (some t) => do
           let s ← ProofSnapshot.create ctx lctx env? [] rootGoals? [t]
@@ -197,7 +193,7 @@ def getProofStatus (proofState : ProofSnapshot) : M m String := do
             unless (← Meta.isDefEq pft expectedType) do
               return s!"Error: proof has type {pft} but root goal has type {expectedType}"
 
-            let pf ← abstractAllLambdaFVars pf
+            let pf ← abstractAllLambdaFVars pf >>= instantiateMVars
             let pft ← Meta.inferType pf >>= instantiateMVars
 
             if pf.hasExprMVar then
diff --git a/REPL/Snapshots.lean b/REPL/Snapshots.lean
index eaebffc4..7f422dff 100644
--- a/REPL/Snapshots.lean
+++ b/REPL/Snapshots.lean
@@ -185,33 +185,44 @@ def runString (p : ProofSnapshot) (t : String) : IO ProofSnapshot :=
 /-- Pretty print the current goals in the `ProofSnapshot`. -/
 def ppGoals (p : ProofSnapshot) : IO (List Format) :=
   Prod.fst <$> p.runMetaM do p.tacticState.goals.mapM (Meta.ppGoal ·)
+
 /--
 Construct a `ProofSnapshot` from a `ContextInfo` and optional `LocalContext`, and a list of goals.
-
 For convenience, we also allow a list of `Expr`s, and these are appended to the goals
 as fresh metavariables with the given types.
 -/
 def create (ctx : ContextInfo) (lctx? : Option LocalContext) (env? : Option Environment)
     (goals : List MVarId) (rootGoals? : Option (List MVarId)) (types : List Expr := [])
     : IO ProofSnapshot := do
-  ctx.runMetaM (lctx?.getD {}) do
-    let goals := goals ++ (← types.mapM fun t => Expr.mvarId! <$> Meta.mkFreshExprMVar (some t))
-    let s ← getThe Core.State
-    let s := match env? with
-    | none => s
-    | some env => { s with env }
-    pure <|
-    { coreState := s
-      coreContext := ← readThe Core.Context
-      metaState := ← getThe Meta.State
-      metaContext := ← readThe Meta.Context
-      termState := {}
-      termContext := {}
-      tacticState := { goals }
-      tacticContext := { elaborator := .anonymous }
-      rootGoals := match rootGoals? with
-        | none => goals
-        | some gs => gs }
+  -- Get the local context from the goals if not provided.
+  let lctx ← match lctx? with
+  | none => match goals with
+    | g :: _ => ctx.runMetaM {} do pure (← g.getDecl).lctx
+    | [] => match rootGoals? with
+      | some (g :: _) => ctx.runMetaM {} do pure (← g.getDecl).lctx
+      | _ => pure {}
+  | some lctx => pure lctx
+
+  ctx.runMetaM lctx do
+    -- update local instances, which is necessary when `types` is non-empty
+    Meta.withLocalInstances (lctx.decls.toList.filterMap id) do
+      let goals := goals ++ (← types.mapM fun t => Expr.mvarId! <$> Meta.mkFreshExprMVar (some t))
+      let s ← getThe Core.State
+      let s := match env? with
+      | none => s
+      | some env => { s with env }
+      pure <|
+      { coreState := s
+        coreContext := ← readThe Core.Context
+        metaState := ← getThe Meta.State
+        metaContext := ← readThe Meta.Context
+        termState := {}
+        termContext := {}
+        tacticState := { goals }
+        tacticContext := { elaborator := .anonymous }
+        rootGoals := match rootGoals? with
+          | none => goals
+          | some gs => gs }
 
 open Lean.Core in
 /-- A copy of `Core.State` with the `Environment`, caches, and logging omitted. -/

From dc85fc545fc80dccacff254dd0516adfcd212bfc Mon Sep 17 00:00:00 2001
From: Auguste Poiroux <augustepoiroux@gmail.com>
Date: Mon, 17 Nov 2025 09:38:42 +0100
Subject: [PATCH 02/13] Add test

---
 test/local_instance_proof.expected.out | 62 ++++++++++++++++++++++++++
 test/local_instance_proof.in           | 21 +++++++++
 2 files changed, 83 insertions(+)
 create mode 100644 test/local_instance_proof.expected.out
 create mode 100644 test/local_instance_proof.in

diff --git a/test/local_instance_proof.expected.out b/test/local_instance_proof.expected.out
new file mode 100644
index 00000000..5a93d082
--- /dev/null
+++ b/test/local_instance_proof.expected.out
@@ -0,0 +1,62 @@
+{"env": 0}
+
+{"env": 1}
+
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 1, "column": 42},
+   "goal": "α : Type\ninst✝ : Inhabited α\n⊢ α",
+   "endPos": {"line": 1, "column": 47}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 4},
+   "endPos": {"line": 1, "column": 9},
+   "data": "declaration uses 'sorry'"}],
+ "env": 2}
+
+{"proofStatus": "Completed", "proofState": 1, "goals": []}
+
+{"sorries":
+ [{"proofState": 2,
+   "pos": {"line": 1, "column": 45},
+   "goal": "α : Type\ninst✝ : Inhabited α\n⊢ α",
+   "endPos": {"line": 1, "column": 50}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 4},
+   "endPos": {"line": 1, "column": 9},
+   "data": "declaration uses 'sorry'"}],
+ "env": 3}
+
+{"proofStatus": "Completed", "proofState": 3, "goals": []}
+
+{"env": 4}
+
+{"sorries":
+ [{"proofState": 4,
+   "pos": {"line": 1, "column": 17},
+   "goal": "α : Type\ns : Inhabited α\n⊢ α",
+   "endPos": {"line": 1, "column": 22}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 4},
+   "endPos": {"line": 1, "column": 9},
+   "data": "declaration uses 'sorry'"}],
+ "env": 5}
+
+{"proofStatus": "Completed", "proofState": 5, "goals": []}
+
+{"sorries":
+ [{"proofState": 6,
+   "pos": {"line": 1, "column": 20},
+   "goal": "α : Type\ns : Inhabited α\n⊢ α",
+   "endPos": {"line": 1, "column": 25}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 4},
+   "endPos": {"line": 1, "column": 9},
+   "data": "declaration uses 'sorry'"}],
+ "env": 6}
+
+{"proofStatus": "Completed", "proofState": 7, "goals": []}
+
diff --git a/test/local_instance_proof.in b/test/local_instance_proof.in
new file mode 100644
index 00000000..eeefd5ef
--- /dev/null
+++ b/test/local_instance_proof.in
@@ -0,0 +1,21 @@
+{"cmd": "def test (α : Type) [s : Inhabited α] : α := @Inhabited.default α s"}
+
+{"cmd": "def test2 (α : Type) [Inhabited α] : α := test α", "env": 0}
+
+{"cmd": "def test2 (α : Type) [Inhabited α] : α := sorry", "env": 0}
+
+{"tactic": "exact test α", "proofState": 0}
+
+{"cmd": "def test2 (α : Type) [Inhabited α] : α := by sorry", "env": 0}
+
+{"tactic": "exact test α", "proofState": 2}
+
+{"cmd": "variable (α : Type) [s : Inhabited α]", "env": 0}
+
+{"cmd": "def test2 : α := sorry", "env": 4}
+
+{"tactic": "exact test α", "proofState": 4}
+
+{"cmd": "def test2 : α := by sorry", "env": 4}
+
+{"tactic": "exact test α", "proofState": 6}

From 8b709807c902e0ec3fc272abe50f0081e5d40067 Mon Sep 17 00:00:00 2001
From: Auguste Poiroux <augustepoiroux@gmail.com>
Date: Thu, 29 Jan 2026 13:06:27 +0100
Subject: [PATCH 03/13] Fix test v4.28.0-rc1

---
 test/local_instance_proof.expected.out | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/test/local_instance_proof.expected.out b/test/local_instance_proof.expected.out
index 5a93d082..a3c25109 100644
--- a/test/local_instance_proof.expected.out
+++ b/test/local_instance_proof.expected.out
@@ -11,7 +11,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 4},
    "endPos": {"line": 1, "column": 9},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 2}
 
 {"proofStatus": "Completed", "proofState": 1, "goals": []}
@@ -25,7 +25,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 4},
    "endPos": {"line": 1, "column": 9},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 3}
 
 {"proofStatus": "Completed", "proofState": 3, "goals": []}
@@ -41,7 +41,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 4},
    "endPos": {"line": 1, "column": 9},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 5}
 
 {"proofStatus": "Completed", "proofState": 5, "goals": []}
@@ -55,7 +55,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 4},
    "endPos": {"line": 1, "column": 9},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 6}
 
 {"proofStatus": "Completed", "proofState": 7, "goals": []}

From 20e0077a47172fd27fc1475c0645adc7cbfa4cb7 Mon Sep 17 00:00:00 2001
From: Auguste Poiroux <augustepoiroux@gmail.com>
Date: Mon, 15 Sep 2025 18:28:12 +0200
Subject: [PATCH 04/13] First attempt at doing incremental processing of
 commands

---
 REPL/Frontend.lean                  | 60 +++++++++++++++---------
 REPL/JSON.lean                      |  2 +-
 REPL/Main.lean                      | 71 +++++++++++++++++++----------
 test/pattern_match.expected.out     |  6 +++
 test/pattern_match.in               |  6 +++
 test/self_proof_check2.expected.out |  0
 test/self_proof_check2.in           |  6 +++
 7 files changed, 106 insertions(+), 45 deletions(-)
 create mode 100644 test/pattern_match.expected.out
 create mode 100644 test/pattern_match.in
 create mode 100644 test/self_proof_check2.expected.out
 create mode 100644 test/self_proof_check2.in

diff --git a/REPL/Frontend.lean b/REPL/Frontend.lean
index 81575ed3..54ceeb25 100644
--- a/REPL/Frontend.lean
+++ b/REPL/Frontend.lean
@@ -9,6 +9,31 @@ open Lean Elab
 
 namespace Lean.Elab.IO
 
+partial def filterRootTactics (tree : InfoTree) : Bool :=
+  match tree with
+  | InfoTree.hole _     => true
+  | InfoTree.context _ t => filterRootTactics t
+  | InfoTree.node i _   => match i with
+      | .ofTacticInfo _ => false
+      | _ => true
+
+/-- Traverses a command snapshot tree, yielding each intermediate state. -/
+partial def traverseCommandSnapshots (snap : Language.Lean.CommandParsedSnapshot)
+(prevCmdState : Command.State) :
+    IO (List ((List InfoTree) × Command.State)) := do
+  let tree := Language.toSnapshotTree snap
+  let snapshots := tree.getAll
+  let infotrees := snapshots.map (·.infoTree?)
+  let infotrees := (infotrees.filterMap id).toList.filter filterRootTactics
+  let results := [(infotrees, snap.resultSnap.task.get.cmdState)]
+  -- let results := [(infotrees, prevCmdState)]
+  match snap.nextCmdSnap? with
+  | none => return results
+  | some nextSnapTask =>
+      let nextSnap := nextSnapTask.task.get
+      let nextResults ← traverseCommandSnapshots nextSnap snap.resultSnap.task.get.cmdState
+      return results ++ nextResults
+
 /--
 Wrapper for `IO.processCommands` that enables info states, and returns
 * the new command state
@@ -17,41 +42,34 @@ Wrapper for `IO.processCommands` that enables info states, and returns
 -/
 def processCommandsWithInfoTrees
     (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState)
-    (commandState : Command.State) : IO (Command.State × List Message × List InfoTree) := do
+    (commandState : Command.State) : IO (Command.State × List Message × (List ((List InfoTree) × Command.State))) := do
   let commandState := { commandState with infoState.enabled := true }
-  let s ← IO.processCommands inputCtx parserState commandState <&> Frontend.State.commandState
-  pure (s, s.messages.toList, s.infoState.trees.toList)
+  let incs ← IO.processCommandsIncrementally inputCtx parserState commandState none
+  let infoTrees ← traverseCommandSnapshots incs.initialSnap commandState
+  let s := incs.commandState
+  pure (s, s.messages.toList, infoTrees)
 
 /--
 Process some text input, with or without an existing command state.
-If there is no existing environment, we parse the input for headers (e.g. import statements),
-and create a new environment.
-Otherwise, we add to the existing environment.
 
 Returns:
-1. The header-only command state (only useful when cmdState? is none)
-2. The resulting command state after processing the entire input
-3. List of messages
-4. List of info trees
+1. The resulting command state after processing the entire input
+2. List of messages
+3. List of info trees along with Command.State from the incremental processing
 -/
 def processInput (input : String) (cmdState? : Option Command.State)
     (opts : Options := {}) (fileName : Option String := none) :
-    IO (Command.State × Command.State × List Message × List InfoTree) := unsafe do
+    IO (Command.State × List Message × (List ((List InfoTree) × Command.State))) := unsafe do
   Lean.initSearchPath (← Lean.findSysroot)
   enableInitializersExecution
   let fileName   := fileName.getD "<input>"
   let inputCtx   := Parser.mkInputContext input fileName
 
-  match cmdState? with
+  let (parserState, commandState) ← match cmdState? with
   | none => do
-    -- Split the processing into two phases to prevent self-reference in proofs in tactic mode
     let (header, parserState, messages) ← Parser.parseHeader inputCtx
     let (env, messages) ← processHeader header opts messages inputCtx
-    let headerOnlyState := Command.mkState env messages opts
-    let (cmdState, messages, trees) ← processCommandsWithInfoTrees inputCtx parserState headerOnlyState
-    return (headerOnlyState, cmdState, messages, trees)
-
-  | some cmdStateBefore => do
-    let parserState : Parser.ModuleParserState := {}
-    let (cmdStateAfter, messages, trees) ← processCommandsWithInfoTrees inputCtx parserState cmdStateBefore
-    return (cmdStateBefore, cmdStateAfter, messages, trees)
+    pure (parserState, (Command.mkState env messages opts))
+  | some cmdState => do
+    pure ({ : Parser.ModuleParserState }, cmdState)
+  processCommandsWithInfoTrees inputCtx parserState commandState
diff --git a/REPL/JSON.lean b/REPL/JSON.lean
index aaeec551..ad387746 100644
--- a/REPL/JSON.lean
+++ b/REPL/JSON.lean
@@ -47,7 +47,7 @@ deriving ToJson, FromJson
 structure Pos where
   line : Nat
   column : Nat
-deriving ToJson, FromJson
+deriving ToJson, FromJson, BEq, Hashable
 
 /-- Severity of a message. -/
 inductive Severity
diff --git a/REPL/Main.lean b/REPL/Main.lean
index c1b0c717..a4699965 100644
--- a/REPL/Main.lean
+++ b/REPL/Main.lean
@@ -111,29 +111,53 @@ def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Op
         let proofStateId ← proofState.mapM recordProofSnapshot
         return Sorry.of goal pos endPos proofStateId
 
+-- def sorries2 (treeList : List ((List InfoTree) × Command.State)) (rootGoals? : Option (List MVarId))
+-- : M m (List Sorry) := do
+--   -- Create a hash set to track positions we've already seen
+--   let mut seenPositions : Std.HashSet (REPL.Pos × REPL.Pos) := {}
+--   let mut result : List Sorry := []
+
+--   for (trees, cmdState) in treeList do
+--     let newSorries ← sorries trees cmdState.env rootGoals?
+
+--     -- Add only sorries at positions we haven't seen yet
+--     for sorr in newSorries do
+--       let pos := (sorr.pos, sorr.endPos)
+--       unless seenPositions.contains pos do
+--         seenPositions := seenPositions.insert pos
+--         result := sorr :: result
+
+--   return result
+
+def sorries2 (treeList : List ((List InfoTree) × Command.State)) (rootGoals? : Option (List MVarId))
+: M m (List Sorry) :=
+  treeList.flatMapM fun (trees, cmdState) => do sorries trees cmdState.env rootGoals?
+
 def ppTactic (ctx : ContextInfo) (stx : Syntax) : IO Format :=
   ctx.runMetaM {} try
     Lean.PrettyPrinter.ppTactic ⟨stx⟩
   catch _ =>
     pure "<failed to pretty print>"
 
-def tactics (trees : List InfoTree) (env? : Option Environment) : M m (List Tactic) :=
-  trees.flatMap InfoTree.tactics |>.mapM
-    fun ⟨ctx, stx, rootGoals, goals, pos, endPos, ns⟩ => do
-      let proofState := some (← ProofSnapshot.create ctx none env? goals rootGoals)
-      let goals := s!"{(← ctx.ppGoals goals)}".trimAscii.toString
-      let tactic := Format.pretty (← ppTactic ctx stx)
-      let proofStateId ← proofState.mapM recordProofSnapshot
-      return Tactic.of goals tactic pos endPos proofStateId ns
-
-def collectRootGoalsAsSorries (trees : List InfoTree) (env? : Option Environment) : M m (List Sorry) := do
-  trees.flatMap InfoTree.rootGoals |>.mapM
-    fun ⟨ctx, goals, pos⟩ => do
-      let proofState := some (← ProofSnapshot.create ctx none env? goals goals)
-      let goals := s!"{(← ctx.ppGoals goals)}".trimAscii.toString
-      let proofStateId ← proofState.mapM recordProofSnapshot
-      return Sorry.of goals pos pos proofStateId
-
+def tactics (treeList : List ((List InfoTree) × Command.State)) : M m (List Tactic) :=
+  treeList.flatMapM fun (trees, cmdState) => do
+    trees.flatMap InfoTree.tactics |>.mapM
+      fun ⟨ctx, stx, rootGoals, goals, pos, endPos, ns⟩ => do
+        let proofState := some (← ProofSnapshot.create ctx none cmdState.env goals rootGoals)
+        let goals := s!"{(← ctx.ppGoals goals)}".trimAscii.toString
+        let tactic := Format.pretty (← ppTactic ctx stx)
+        let proofStateId ← proofState.mapM recordProofSnapshot
+        return Tactic.of goals tactic pos endPos proofStateId ns
+
+def collectRootGoalsAsSorries (treeList : List ((List InfoTree) × Command.State))
+: M m (List Sorry) := do
+  treeList.flatMapM fun (trees, cmdState) => do
+    trees.flatMap InfoTree.rootGoals |>.mapM
+      fun ⟨ctx, goals, pos⟩ => do
+        let proofState := some (← ProofSnapshot.create ctx none cmdState.env goals goals)
+        let goals := s!"{(← ctx.ppGoals goals)}".trimAscii.toString
+        let proofStateId ← proofState.mapM recordProofSnapshot
+        return Sorry.of goals pos pos proofStateId
 
 private def collectFVarsAux : Expr → NameSet
   | .fvar fvarId => NameSet.empty.insert fvarId.name
@@ -298,19 +322,17 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
   if notFound then
     return .inr ⟨"Unknown environment."⟩
   let initialCmdState? := cmdSnapshot?.map fun c => c.cmdState
-  let (initialCmdState, cmdState, messages, trees) ← try
+  let (cmdState, messages, trees) ← try
     IO.processInput s.cmd initialCmdState?
   catch ex =>
     return .inr ⟨ex.toString⟩
   let messages ← messages.mapM fun m => Message.of m
-  -- For debugging purposes, sometimes we print out the trees here:
-  -- trees.forM fun t => do IO.println (← t.format)
-  let sorries ← sorries trees initialCmdState.env none
+  let sorries ← sorries2 trees none
   let sorries ← match s.rootGoals with
-  | some true => pure (sorries ++ (← collectRootGoalsAsSorries trees initialCmdState.env))
+  | some true => pure (sorries ++ (← collectRootGoalsAsSorries trees))
   | _ => pure sorries
   let tactics ← match s.allTactics with
-  | some true => tactics trees initialCmdState.env
+  | some true => tactics trees
   | _ => pure []
   let cmdSnapshot :=
   { cmdState
@@ -320,6 +342,9 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
         snap? := none,
         cancelTk? := none } }
   let env ← recordCommandSnapshot cmdSnapshot
+  let trees := (trees.map (·.1)).flatten
+  -- For debugging purposes, sometimes we print out the trees here:
+  -- trees.forM fun t => do IO.println (← t.format)
   let jsonTrees := match s.infotree with
   | some "full" => trees
   | some "tactics" => trees.flatMap InfoTree.retainTacticInfo
diff --git a/test/pattern_match.expected.out b/test/pattern_match.expected.out
new file mode 100644
index 00000000..2c1d028e
--- /dev/null
+++ b/test/pattern_match.expected.out
@@ -0,0 +1,6 @@
+{"cmd": "#eval 1 + 1"}
+
+{"cmd": "def foo : (fun ((x, y, z) : Nat × Nat × Nat) => x = x) = fun x => True := by sorry", "env": 0}
+
+{"tactic": "simp", "proofState": 0}
+
diff --git a/test/pattern_match.in b/test/pattern_match.in
new file mode 100644
index 00000000..2c1d028e
--- /dev/null
+++ b/test/pattern_match.in
@@ -0,0 +1,6 @@
+{"cmd": "#eval 1 + 1"}
+
+{"cmd": "def foo : (fun ((x, y, z) : Nat × Nat × Nat) => x = x) = fun x => True := by sorry", "env": 0}
+
+{"tactic": "simp", "proofState": 0}
+
diff --git a/test/self_proof_check2.expected.out b/test/self_proof_check2.expected.out
new file mode 100644
index 00000000..e69de29b
diff --git a/test/self_proof_check2.in b/test/self_proof_check2.in
new file mode 100644
index 00000000..78c0b6a9
--- /dev/null
+++ b/test/self_proof_check2.in
@@ -0,0 +1,6 @@
+{"cmd": "theorem x : False := sorry\nexample : False := by exact?"}
+
+{"cmd": "theorem x : False := sorry\nexample : False := sorry"}
+
+{"proofState": 2, "tactic": "exact?"}
+

From 941656d98c5ae2c5df0eea497ac337aea91fb52c Mon Sep 17 00:00:00 2001
From: Auguste Poiroux <augustepoiroux@gmail.com>
Date: Mon, 15 Sep 2025 18:28:13 +0200
Subject: [PATCH 05/13] Implement incrmental collection of sorries

---
 REPL/Frontend.lean | 83 +++++++++++++++++++++++++---------------------
 REPL/Main.lean     | 63 +++++++++++++++++------------------
 2 files changed, 76 insertions(+), 70 deletions(-)

diff --git a/REPL/Frontend.lean b/REPL/Frontend.lean
index 54ceeb25..8a7e809c 100644
--- a/REPL/Frontend.lean
+++ b/REPL/Frontend.lean
@@ -5,34 +5,41 @@ Authors: Scott Morrison
 -/
 import Lean.Elab.Frontend
 
-open Lean Elab
+open Lean Elab Language
 
 namespace Lean.Elab.IO
 
-partial def filterRootTactics (tree : InfoTree) : Bool :=
-  match tree with
-  | InfoTree.hole _     => true
-  | InfoTree.context _ t => filterRootTactics t
-  | InfoTree.node i _   => match i with
-      | .ofTacticInfo _ => false
-      | _ => true
-
-/-- Traverses a command snapshot tree, yielding each intermediate state. -/
-partial def traverseCommandSnapshots (snap : Language.Lean.CommandParsedSnapshot)
-(prevCmdState : Command.State) :
-    IO (List ((List InfoTree) × Command.State)) := do
-  let tree := Language.toSnapshotTree snap
-  let snapshots := tree.getAll
-  let infotrees := snapshots.map (·.infoTree?)
-  let infotrees := (infotrees.filterMap id).toList.filter filterRootTactics
-  let results := [(infotrees, snap.resultSnap.task.get.cmdState)]
-  -- let results := [(infotrees, prevCmdState)]
-  match snap.nextCmdSnap? with
-  | none => return results
-  | some nextSnapTask =>
-      let nextSnap := nextSnapTask.task.get
-      let nextResults ← traverseCommandSnapshots nextSnap snap.resultSnap.task.get.cmdState
-      return results ++ nextResults
+partial def IO.processCommandsIncrementally' (inputCtx : Parser.InputContext)
+    (parserState : Parser.ModuleParserState) (commandState : Command.State)
+    (old? : Option IncrementalState) :
+    BaseIO (List (IncrementalState × Option InfoTree)) := do
+  let task ← Language.Lean.processCommands inputCtx parserState commandState
+    (old?.map fun old => (old.inputCtx, old.initialSnap))
+  return go task.get task #[]
+where
+  go initialSnap t commands :=
+    let snap := t.get
+    let commands := commands.push snap
+    -- Opting into reuse also enables incremental reporting, so make sure to collect messages from
+    -- all snapshots
+    let messages := toSnapshotTree initialSnap
+      |>.getAll.map (·.diagnostics.msgLog)
+      |>.foldl (· ++ ·) {}
+    -- In contrast to messages, we should collect info trees only from the top-level command
+    -- snapshots as they subsume any info trees reported incrementally by their children.
+    let trees := commands.map (·.infoTreeSnap.get.infoTree?) |>.filterMap id |>.toPArray'
+    let result : (IncrementalState × Option InfoTree) :=
+      ({ commandState := { snap.resultSnap.get.cmdState with messages, infoState.trees := trees }
+         , parserState := snap.parserState
+         , cmdPos := snap.parserState.pos
+         , commands := commands.map (·.stx)
+         , inputCtx := inputCtx
+         , initialSnap := initialSnap
+       }, snap.infoTreeSnap.get.infoTree?)
+    if let some next := snap.nextCmdSnap? then
+      result :: go initialSnap next.task commands
+    else
+      [result]
 
 /--
 Wrapper for `IO.processCommands` that enables info states, and returns
@@ -42,12 +49,11 @@ Wrapper for `IO.processCommands` that enables info states, and returns
 -/
 def processCommandsWithInfoTrees
     (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState)
-    (commandState : Command.State) : IO (Command.State × List Message × (List ((List InfoTree) × Command.State))) := do
+    (commandState : Command.State) (incrementalState? : Option IncrementalState := none)
+    : IO (List (IncrementalState × Option InfoTree) × List Message) := do
   let commandState := { commandState with infoState.enabled := true }
-  let incs ← IO.processCommandsIncrementally inputCtx parserState commandState none
-  let infoTrees ← traverseCommandSnapshots incs.initialSnap commandState
-  let s := incs.commandState
-  pure (s, s.messages.toList, infoTrees)
+  let incStates ← IO.processCommandsIncrementally' inputCtx parserState commandState incrementalState?
+  pure (incStates, (incStates.getLast?.map (·.1.commandState.messages.toList)).getD {})
 
 /--
 Process some text input, with or without an existing command state.
@@ -59,17 +65,20 @@ Returns:
 -/
 def processInput (input : String) (cmdState? : Option Command.State)
     (opts : Options := {}) (fileName : Option String := none) :
-    IO (Command.State × List Message × (List ((List InfoTree) × Command.State))) := unsafe do
+    IO (Command.State × List (IncrementalState × Option InfoTree) × List Message) := unsafe do
   Lean.initSearchPath (← Lean.findSysroot)
   enableInitializersExecution
   let fileName   := fileName.getD "<input>"
   let inputCtx   := Parser.mkInputContext input fileName
-
-  let (parserState, commandState) ← match cmdState? with
+  match cmdState? with
   | none => do
+    -- Split the processing into two phases to prevent self-reference in proofs in tactic mode
     let (header, parserState, messages) ← Parser.parseHeader inputCtx
     let (env, messages) ← processHeader header opts messages inputCtx
-    pure (parserState, (Command.mkState env messages opts))
-  | some cmdState => do
-    pure ({ : Parser.ModuleParserState }, cmdState)
-  processCommandsWithInfoTrees inputCtx parserState commandState
+    let headerOnlyState := Command.mkState env messages opts
+    let incStates ← processCommandsWithInfoTrees inputCtx parserState headerOnlyState
+    return (headerOnlyState, incStates)
+  | some cmdStateBefore => do
+    let parserState : Parser.ModuleParserState := {}
+    let incStates ← processCommandsWithInfoTrees inputCtx parserState cmdStateBefore
+    return (cmdStateBefore, incStates)
diff --git a/REPL/Main.lean b/REPL/Main.lean
index a4699965..dce4b724 100644
--- a/REPL/Main.lean
+++ b/REPL/Main.lean
@@ -111,27 +111,15 @@ def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Op
         let proofStateId ← proofState.mapM recordProofSnapshot
         return Sorry.of goal pos endPos proofStateId
 
--- def sorries2 (treeList : List ((List InfoTree) × Command.State)) (rootGoals? : Option (List MVarId))
--- : M m (List Sorry) := do
---   -- Create a hash set to track positions we've already seen
---   let mut seenPositions : Std.HashSet (REPL.Pos × REPL.Pos) := {}
---   let mut result : List Sorry := []
-
---   for (trees, cmdState) in treeList do
---     let newSorries ← sorries trees cmdState.env rootGoals?
-
---     -- Add only sorries at positions we haven't seen yet
---     for sorr in newSorries do
---       let pos := (sorr.pos, sorr.endPos)
---       unless seenPositions.contains pos do
---         seenPositions := seenPositions.insert pos
---         result := sorr :: result
-
---   return result
-
-def sorries2 (treeList : List ((List InfoTree) × Command.State)) (rootGoals? : Option (List MVarId))
+def sorriesCmd (treeList : List (IncrementalState × Option InfoTree)) (prevEnv : Environment)
+(rootGoals? : Option (List MVarId))
 : M m (List Sorry) :=
-  treeList.flatMapM fun (trees, cmdState) => do sorries trees cmdState.env rootGoals?
+  match treeList with
+  | [] => pure []
+  | (state, infoTree?) :: rest => do
+    let s ← sorries infoTree?.toList prevEnv rootGoals?
+    let restSorries ← sorriesCmd rest state.commandState.env rootGoals?
+    return s ++ restSorries
 
 def ppTactic (ctx : ContextInfo) (stx : Syntax) : IO Format :=
   ctx.runMetaM {} try
@@ -139,22 +127,22 @@ def ppTactic (ctx : ContextInfo) (stx : Syntax) : IO Format :=
   catch _ =>
     pure "<failed to pretty print>"
 
-def tactics (treeList : List ((List InfoTree) × Command.State)) : M m (List Tactic) :=
-  treeList.flatMapM fun (trees, cmdState) => do
-    trees.flatMap InfoTree.tactics |>.mapM
+def tactics (treeList : List (IncrementalState × Option InfoTree)) : M m (List Tactic) :=
+  treeList.flatMapM fun (state, infoTree?) => do
+    infoTree?.toList.flatMap InfoTree.tactics |>.mapM
       fun ⟨ctx, stx, rootGoals, goals, pos, endPos, ns⟩ => do
-        let proofState := some (← ProofSnapshot.create ctx none cmdState.env goals rootGoals)
+        let proofState := some (← ProofSnapshot.create ctx none state.commandState.env goals rootGoals)
         let goals := s!"{(← ctx.ppGoals goals)}".trimAscii.toString
         let tactic := Format.pretty (← ppTactic ctx stx)
         let proofStateId ← proofState.mapM recordProofSnapshot
         return Tactic.of goals tactic pos endPos proofStateId ns
 
-def collectRootGoalsAsSorries (treeList : List ((List InfoTree) × Command.State))
+def collectRootGoalsAsSorries (treeList : List (IncrementalState × Option InfoTree))
 : M m (List Sorry) := do
-  treeList.flatMapM fun (trees, cmdState) => do
-    trees.flatMap InfoTree.rootGoals |>.mapM
+  treeList.flatMapM fun (state, infoTree?) => do
+    infoTree?.toList.flatMap InfoTree.rootGoals |>.mapM
       fun ⟨ctx, goals, pos⟩ => do
-        let proofState := some (← ProofSnapshot.create ctx none cmdState.env goals goals)
+        let proofState := some (← ProofSnapshot.create ctx none state.commandState.env goals goals)
         let goals := s!"{(← ctx.ppGoals goals)}".trimAscii.toString
         let proofStateId ← proofState.mapM recordProofSnapshot
         return Sorry.of goals pos pos proofStateId
@@ -322,17 +310,26 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
   if notFound then
     return .inr ⟨"Unknown environment."⟩
   let initialCmdState? := cmdSnapshot?.map fun c => c.cmdState
-  let (cmdState, messages, trees) ← try
+  let (initialCmdState, incStates, messages) ← try
     IO.processInput s.cmd initialCmdState?
   catch ex =>
     return .inr ⟨ex.toString⟩
+
+  let mut prevPos := 0
+  for (incState, _) in incStates do
+    let endPos := incState.cmdPos
+    let processedText := incState.inputCtx.input.extract prevPos endPos
+    IO.println s!"Processing incremental state [pos: {prevPos}..{endPos}]:\n{processedText}"
+    prevPos := endPos
+
+  let cmdState := (incStates.getLast?.map (fun c => c.1.commandState)).getD initialCmdState
   let messages ← messages.mapM fun m => Message.of m
-  let sorries ← sorries2 trees none
+  let sorries ← sorriesCmd incStates initialCmdState.env none
   let sorries ← match s.rootGoals with
-  | some true => pure (sorries ++ (← collectRootGoalsAsSorries trees))
+  | some true => pure (sorries ++ (← collectRootGoalsAsSorries incStates))
   | _ => pure sorries
   let tactics ← match s.allTactics with
-  | some true => tactics trees
+  | some true => tactics incStates
   | _ => pure []
   let cmdSnapshot :=
   { cmdState
@@ -342,7 +339,7 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
         snap? := none,
         cancelTk? := none } }
   let env ← recordCommandSnapshot cmdSnapshot
-  let trees := (trees.map (·.1)).flatten
+  let trees := cmdState.infoState.trees.toList
   -- For debugging purposes, sometimes we print out the trees here:
   -- trees.forM fun t => do IO.println (← t.format)
   let jsonTrees := match s.infotree with

From 7e5b01330e24ebc388e3269a02a2f001d709a23d Mon Sep 17 00:00:00 2001
From: Auguste Poiroux <augustepoiroux@gmail.com>
Date: Mon, 15 Sep 2025 18:28:13 +0200
Subject: [PATCH 06/13] Fix test output

---
 test/self_proof_check2.expected.out | 49 +++++++++++++++++++++++++++++
 1 file changed, 49 insertions(+)

diff --git a/test/self_proof_check2.expected.out b/test/self_proof_check2.expected.out
index e69de29b..99d5339f 100644
--- a/test/self_proof_check2.expected.out
+++ b/test/self_proof_check2.expected.out
@@ -0,0 +1,49 @@
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 1, "column": 21},
+   "goal": "⊢ False",
+   "endPos": {"line": 1, "column": 26}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 8},
+   "endPos": {"line": 1, "column": 9},
+   "data": "declaration uses 'sorry'"},
+  {"severity": "info",
+   "pos": {"line": 2, "column": 22},
+   "endPos": {"line": 2, "column": 28},
+   "data": "Try this: exact x"},
+  {"severity": "info",
+   "pos": {"line": 2, "column": 0},
+   "endPos": {"line": 2, "column": 28},
+   "data": "Goals accomplished!"}],
+ "env": 0}
+
+{"sorries":
+ [{"proofState": 1,
+   "pos": {"line": 1, "column": 21},
+   "goal": "⊢ False",
+   "endPos": {"line": 1, "column": 26}},
+  {"proofState": 2,
+   "pos": {"line": 2, "column": 19},
+   "goal": "⊢ False",
+   "endPos": {"line": 2, "column": 24}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 8},
+   "endPos": {"line": 1, "column": 9},
+   "data": "declaration uses 'sorry'"},
+  {"severity": "warning",
+   "pos": {"line": 2, "column": 0},
+   "endPos": {"line": 2, "column": 7},
+   "data": "declaration uses 'sorry'"}],
+ "env": 1}
+
+{"proofStatus": "Completed",
+ "proofState": 3,
+ "messages":
+ [{"severity": "info",
+   "pos": {"line": 0, "column": 0},
+   "endPos": {"line": 0, "column": 0},
+   "data": "Try this: exact x"}],
+ "goals": []}
+

From d2eca61ea8f26a78e9b664567d4bc55326a1af9c Mon Sep 17 00:00:00 2001
From: Auguste Poiroux <augustepoiroux@gmail.com>
Date: Mon, 15 Sep 2025 18:28:13 +0200
Subject: [PATCH 07/13] Update tests

---
 ...out => in_command_dependency.expected.out} |  6 +---
 ...oof_check2.in => in_command_dependency.in} |  0
 test/pattern_match.expected.out               | 28 +++++++++++++++++--
 test/pattern_match.in                         |  9 ++++--
 4 files changed, 33 insertions(+), 10 deletions(-)
 rename test/{self_proof_check2.expected.out => in_command_dependency.expected.out} (87%)
 rename test/{self_proof_check2.in => in_command_dependency.in} (100%)

diff --git a/test/self_proof_check2.expected.out b/test/in_command_dependency.expected.out
similarity index 87%
rename from test/self_proof_check2.expected.out
rename to test/in_command_dependency.expected.out
index 99d5339f..e3ba5583 100644
--- a/test/self_proof_check2.expected.out
+++ b/test/in_command_dependency.expected.out
@@ -11,11 +11,7 @@
   {"severity": "info",
    "pos": {"line": 2, "column": 22},
    "endPos": {"line": 2, "column": 28},
-   "data": "Try this: exact x"},
-  {"severity": "info",
-   "pos": {"line": 2, "column": 0},
-   "endPos": {"line": 2, "column": 28},
-   "data": "Goals accomplished!"}],
+   "data": "Try this: exact x"}],
  "env": 0}
 
 {"sorries":
diff --git a/test/self_proof_check2.in b/test/in_command_dependency.in
similarity index 100%
rename from test/self_proof_check2.in
rename to test/in_command_dependency.in
diff --git a/test/pattern_match.expected.out b/test/pattern_match.expected.out
index 2c1d028e..2e16d41f 100644
--- a/test/pattern_match.expected.out
+++ b/test/pattern_match.expected.out
@@ -1,6 +1,28 @@
-{"cmd": "#eval 1 + 1"}
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 1, "column": 77},
+   "goal":
+   "⊢ (fun x =>\n      match x with\n      | (x, fst, snd) => x = x) =\n    fun x => True",
+   "endPos": {"line": 1, "column": 82}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 4},
+   "endPos": {"line": 1, "column": 7},
+   "data": "declaration uses 'sorry'"}],
+ "env": 0}
 
-{"cmd": "def foo : (fun ((x, y, z) : Nat × Nat × Nat) => x = x) = fun x => True := by sorry", "env": 0}
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 1,
+ "goals":
+ ["case h\nx y z : Nat\n⊢ (foo.match_1 (fun x => Prop) (x, y, z) fun x fst snd => x = x) = True"]}
 
-{"tactic": "simp", "proofState": 0}
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 2,
+ "goals": ["case h\nx y z : Nat\n⊢ (x = x) = True"]}
+
+{"proofStatus": "Completed", "proofState": 3, "goals": []}
+
+{"proofStatus": "Completed", "proofState": 4, "goals": []}
+
+{"env": 1}
 
diff --git a/test/pattern_match.in b/test/pattern_match.in
index 2c1d028e..a863f0b9 100644
--- a/test/pattern_match.in
+++ b/test/pattern_match.in
@@ -1,6 +1,11 @@
-{"cmd": "#eval 1 + 1"}
+{"cmd": "def foo : (fun ((x, _, _) : Nat × Nat × Nat) => x = x) = fun _ => True := by sorry"}
 
-{"cmd": "def foo : (fun ((x, y, z) : Nat × Nat × Nat) => x = x) = fun x => True := by sorry", "env": 0}
+{"tactic": "funext ⟨x, y, z⟩", "proofState": 0}
+
+{"tactic": "show (x = x) = True", "proofState": 1}
+
+{"tactic": "rw [eq_self_iff_true]", "proofState": 2}
 
 {"tactic": "simp", "proofState": 0}
 
+{"cmd": "def foo : (fun ((x, _, _) : Nat × Nat × Nat) => x = x) = fun _ => True := by simp"}

From 09c46896ae1ef008011420573cef9e0852e18fbf Mon Sep 17 00:00:00 2001
From: Auguste Poiroux <augustepoiroux@gmail.com>
Date: Mon, 15 Sep 2025 18:28:14 +0200
Subject: [PATCH 08/13] Improving fine-grained environment

---
 REPL/Main.lean      | 63 +++++++++++++++++++++++++--------------------
 REPL/Snapshots.lean | 33 +++++++++++++++++++-----
 2 files changed, 62 insertions(+), 34 deletions(-)

diff --git a/REPL/Main.lean b/REPL/Main.lean
index dce4b724..cedc71ed 100644
--- a/REPL/Main.lean
+++ b/REPL/Main.lean
@@ -127,25 +127,39 @@ def ppTactic (ctx : ContextInfo) (stx : Syntax) : IO Format :=
   catch _ =>
     pure "<failed to pretty print>"
 
-def tactics (treeList : List (IncrementalState × Option InfoTree)) : M m (List Tactic) :=
-  treeList.flatMapM fun (state, infoTree?) => do
-    infoTree?.toList.flatMap InfoTree.tactics |>.mapM
-      fun ⟨ctx, stx, rootGoals, goals, pos, endPos, ns⟩ => do
-        let proofState := some (← ProofSnapshot.create ctx none state.commandState.env goals rootGoals)
-        let goals := s!"{(← ctx.ppGoals goals)}".trimAscii.toString
-        let tactic := Format.pretty (← ppTactic ctx stx)
-        let proofStateId ← proofState.mapM recordProofSnapshot
-        return Tactic.of goals tactic pos endPos proofStateId ns
-
-def collectRootGoalsAsSorries (treeList : List (IncrementalState × Option InfoTree))
-: M m (List Sorry) := do
-  treeList.flatMapM fun (state, infoTree?) => do
-    infoTree?.toList.flatMap InfoTree.rootGoals |>.mapM
-      fun ⟨ctx, goals, pos⟩ => do
-        let proofState := some (← ProofSnapshot.create ctx none state.commandState.env goals goals)
-        let goals := s!"{(← ctx.ppGoals goals)}".trimAscii.toString
-        let proofStateId ← proofState.mapM recordProofSnapshot
-        return Sorry.of goals pos pos proofStateId
+def tactics (trees : List InfoTree) (env? : Option Environment) : M m (List Tactic) :=
+  trees.flatMap InfoTree.tactics |>.mapM
+    fun ⟨ctx, stx, rootGoals, goals, pos, endPos, ns⟩ => do
+      let proofState := some (← ProofSnapshot.create ctx none env? goals rootGoals)
+      let goals := s!"{(← ctx.ppGoals goals)}".trimAscii.toString
+      let tactic := Format.pretty (← ppTactic ctx stx)
+      let proofStateId ← proofState.mapM recordProofSnapshot
+      return Tactic.of goals tactic pos endPos proofStateId ns
+
+def tacticsCmd (treeList : List (IncrementalState × Option InfoTree)) (prevEnv : Environment) : M m (List Tactic) := do
+  match treeList with
+  | [] => pure []
+  | (state, infoTree?) :: rest => do
+    let ts ← tactics infoTree?.toList prevEnv
+    let restTactics ← tacticsCmd rest state.commandState.env
+    return ts ++ restTactics
+
+def collectRootGoalsAsSorries (trees : List InfoTree) (env? : Option Environment) : M m (List Sorry) := do
+  trees.flatMap InfoTree.rootGoals |>.mapM
+    fun ⟨ctx, goals, pos⟩ => do
+      let proofState := some (← ProofSnapshot.create ctx none env? goals goals)
+      let goals := s!"{(← ctx.ppGoals goals)}".trimAscii.toString
+      let proofStateId ← proofState.mapM recordProofSnapshot
+      return Sorry.of goals pos pos proofStateId
+
+def collectRootGoalsAsSorriesCmd (treeList : List (IncrementalState × Option InfoTree)) (prevEnv : Environment) :
+    M m (List Sorry) := do
+  match treeList with
+  | [] => pure []
+  | (state, infoTree?) :: rest => do
+    let sorries ← collectRootGoalsAsSorries infoTree?.toList prevEnv
+    let restSorries ← collectRootGoalsAsSorriesCmd rest state.commandState.env
+    return sorries ++ restSorries
 
 private def collectFVarsAux : Expr → NameSet
   | .fvar fvarId => NameSet.empty.insert fvarId.name
@@ -315,21 +329,14 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
   catch ex =>
     return .inr ⟨ex.toString⟩
 
-  let mut prevPos := 0
-  for (incState, _) in incStates do
-    let endPos := incState.cmdPos
-    let processedText := incState.inputCtx.input.extract prevPos endPos
-    IO.println s!"Processing incremental state [pos: {prevPos}..{endPos}]:\n{processedText}"
-    prevPos := endPos
-
   let cmdState := (incStates.getLast?.map (fun c => c.1.commandState)).getD initialCmdState
   let messages ← messages.mapM fun m => Message.of m
   let sorries ← sorriesCmd incStates initialCmdState.env none
   let sorries ← match s.rootGoals with
-  | some true => pure (sorries ++ (← collectRootGoalsAsSorries incStates))
+  | some true => pure (sorries ++ (← collectRootGoalsAsSorriesCmd incStates initialCmdState.env))
   | _ => pure sorries
   let tactics ← match s.allTactics with
-  | some true => tactics incStates
+  | some true => tacticsCmd incStates initialCmdState.env
   | _ => pure []
   let cmdSnapshot :=
   { cmdState
diff --git a/REPL/Snapshots.lean b/REPL/Snapshots.lean
index 7f422dff..ca6814c3 100644
--- a/REPL/Snapshots.lean
+++ b/REPL/Snapshots.lean
@@ -191,7 +191,7 @@ Construct a `ProofSnapshot` from a `ContextInfo` and optional `LocalContext`, an
 For convenience, we also allow a list of `Expr`s, and these are appended to the goals
 as fresh metavariables with the given types.
 -/
-def create (ctx : ContextInfo) (lctx? : Option LocalContext) (env? : Option Environment)
+def create (ctx : ContextInfo) (lctx? : Option LocalContext) (prevEnv? : Option Environment)
     (goals : List MVarId) (rootGoals? : Option (List MVarId)) (types : List Expr := [])
     : IO ProofSnapshot := do
   -- Get the local context from the goals if not provided.
@@ -207,12 +207,33 @@ def create (ctx : ContextInfo) (lctx? : Option LocalContext) (env? : Option Envi
     -- update local instances, which is necessary when `types` is non-empty
     Meta.withLocalInstances (lctx.decls.toList.filterMap id) do
       let goals := goals ++ (← types.mapM fun t => Expr.mvarId! <$> Meta.mkFreshExprMVar (some t))
-      let s ← getThe Core.State
-      let s := match env? with
-      | none => s
-      | some env => { s with env }
+
+      -- Create a filtered environment that excludes the new (non-auxiliary) declarations
+      -- Necessary to avoid self-references in proofs in tactic mode, while still allowing
+      -- auxiliary declarations to be used in the proof.
+      let coreState ← match prevEnv? with
+      | none => getThe Core.State
+      | some prevEnv => do
+        let declsToFilter := ((← getLCtx).decls.toList.filterMap id).map (·.userName)
+        let declsToFilterSet : Std.HashSet Name := declsToFilter.foldl (init := {}) fun s n => s.insert n
+
+        let currentConsts := ctx.env.constants.map₂.toList
+        let prevConsts := prevEnv.constants.map₂.toList
+        let diff := currentConsts.filter (fun (name, _) =>
+          !prevConsts.any (fun (name', _) => name == name'))
+        let filteredConstants := diff.filter fun (name, _) => !declsToFilterSet.contains name
+
+        -- Print for debugging purposes
+        IO.println s!"Constants to filter: {declsToFilter}"
+        IO.println s!"Replayed constants: {filteredConstants.map (·.1)}"
+
+        let filteredEnv ← prevEnv.replay (Std.HashMap.ofList filteredConstants)
+        -- let filteredEnv := prevEnv
+        let s ← getThe Core.State
+        pure { s with env := filteredEnv }
+
       pure <|
-      { coreState := s
+      { coreState := coreState
         coreContext := ← readThe Core.Context
         metaState := ← getThe Meta.State
         metaContext := ← readThe Meta.Context

From 83cedb431ff6c71c2c940c4aa5269a74b0ac1994 Mon Sep 17 00:00:00 2001
From: Auguste Poiroux <augustepoiroux@gmail.com>
Date: Mon, 15 Sep 2025 18:28:14 +0200
Subject: [PATCH 09/13] Revert constant replay

---
 REPL/Snapshots.lean             | 31 +++++--------------------------
 test/pattern_match.expected.out | 28 ----------------------------
 test/pattern_match.in           | 11 -----------
 3 files changed, 5 insertions(+), 65 deletions(-)
 delete mode 100644 test/pattern_match.expected.out
 delete mode 100644 test/pattern_match.in

diff --git a/REPL/Snapshots.lean b/REPL/Snapshots.lean
index ca6814c3..b5597a40 100644
--- a/REPL/Snapshots.lean
+++ b/REPL/Snapshots.lean
@@ -207,33 +207,12 @@ def create (ctx : ContextInfo) (lctx? : Option LocalContext) (prevEnv? : Option
     -- update local instances, which is necessary when `types` is non-empty
     Meta.withLocalInstances (lctx.decls.toList.filterMap id) do
       let goals := goals ++ (← types.mapM fun t => Expr.mvarId! <$> Meta.mkFreshExprMVar (some t))
-
-      -- Create a filtered environment that excludes the new (non-auxiliary) declarations
-      -- Necessary to avoid self-references in proofs in tactic mode, while still allowing
-      -- auxiliary declarations to be used in the proof.
-      let coreState ← match prevEnv? with
-      | none => getThe Core.State
-      | some prevEnv => do
-        let declsToFilter := ((← getLCtx).decls.toList.filterMap id).map (·.userName)
-        let declsToFilterSet : Std.HashSet Name := declsToFilter.foldl (init := {}) fun s n => s.insert n
-
-        let currentConsts := ctx.env.constants.map₂.toList
-        let prevConsts := prevEnv.constants.map₂.toList
-        let diff := currentConsts.filter (fun (name, _) =>
-          !prevConsts.any (fun (name', _) => name == name'))
-        let filteredConstants := diff.filter fun (name, _) => !declsToFilterSet.contains name
-
-        -- Print for debugging purposes
-        IO.println s!"Constants to filter: {declsToFilter}"
-        IO.println s!"Replayed constants: {filteredConstants.map (·.1)}"
-
-        let filteredEnv ← prevEnv.replay (Std.HashMap.ofList filteredConstants)
-        -- let filteredEnv := prevEnv
-        let s ← getThe Core.State
-        pure { s with env := filteredEnv }
-
+      let s ← getThe Core.State
+      let s := match prevEnv? with
+      | none => s
+      | some env => { s with env }
       pure <|
-      { coreState := coreState
+      { coreState := s
         coreContext := ← readThe Core.Context
         metaState := ← getThe Meta.State
         metaContext := ← readThe Meta.Context
diff --git a/test/pattern_match.expected.out b/test/pattern_match.expected.out
deleted file mode 100644
index 2e16d41f..00000000
--- a/test/pattern_match.expected.out
+++ /dev/null
@@ -1,28 +0,0 @@
-{"sorries":
- [{"proofState": 0,
-   "pos": {"line": 1, "column": 77},
-   "goal":
-   "⊢ (fun x =>\n      match x with\n      | (x, fst, snd) => x = x) =\n    fun x => True",
-   "endPos": {"line": 1, "column": 82}}],
- "messages":
- [{"severity": "warning",
-   "pos": {"line": 1, "column": 4},
-   "endPos": {"line": 1, "column": 7},
-   "data": "declaration uses 'sorry'"}],
- "env": 0}
-
-{"proofStatus": "Incomplete: open goals remain",
- "proofState": 1,
- "goals":
- ["case h\nx y z : Nat\n⊢ (foo.match_1 (fun x => Prop) (x, y, z) fun x fst snd => x = x) = True"]}
-
-{"proofStatus": "Incomplete: open goals remain",
- "proofState": 2,
- "goals": ["case h\nx y z : Nat\n⊢ (x = x) = True"]}
-
-{"proofStatus": "Completed", "proofState": 3, "goals": []}
-
-{"proofStatus": "Completed", "proofState": 4, "goals": []}
-
-{"env": 1}
-
diff --git a/test/pattern_match.in b/test/pattern_match.in
deleted file mode 100644
index a863f0b9..00000000
--- a/test/pattern_match.in
+++ /dev/null
@@ -1,11 +0,0 @@
-{"cmd": "def foo : (fun ((x, _, _) : Nat × Nat × Nat) => x = x) = fun _ => True := by sorry"}
-
-{"tactic": "funext ⟨x, y, z⟩", "proofState": 0}
-
-{"tactic": "show (x = x) = True", "proofState": 1}
-
-{"tactic": "rw [eq_self_iff_true]", "proofState": 2}
-
-{"tactic": "simp", "proofState": 0}
-
-{"cmd": "def foo : (fun ((x, _, _) : Nat × Nat × Nat) => x = x) = fun _ => True := by simp"}

From 12804ad5589689008bd904bedbba8f6cd709e304 Mon Sep 17 00:00:00 2001
From: Auguste Poiroux <augustepoiroux@gmail.com>
Date: Mon, 15 Sep 2025 18:28:15 +0200
Subject: [PATCH 10/13] Fix v4.22.0-rc2

---
 REPL/Frontend.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/REPL/Frontend.lean b/REPL/Frontend.lean
index 8a7e809c..bc2dff1e 100644
--- a/REPL/Frontend.lean
+++ b/REPL/Frontend.lean
@@ -27,15 +27,15 @@ where
       |>.foldl (· ++ ·) {}
     -- In contrast to messages, we should collect info trees only from the top-level command
     -- snapshots as they subsume any info trees reported incrementally by their children.
-    let trees := commands.map (·.infoTreeSnap.get.infoTree?) |>.filterMap id |>.toPArray'
+    let trees := commands.map (·.elabSnap.infoTreeSnap.get.infoTree?) |>.filterMap id |>.toPArray'
     let result : (IncrementalState × Option InfoTree) :=
-      ({ commandState := { snap.resultSnap.get.cmdState with messages, infoState.trees := trees }
+      ({ commandState := { snap.elabSnap.resultSnap.get.cmdState with messages, infoState.trees := trees }
          , parserState := snap.parserState
          , cmdPos := snap.parserState.pos
          , commands := commands.map (·.stx)
          , inputCtx := inputCtx
          , initialSnap := initialSnap
-       }, snap.infoTreeSnap.get.infoTree?)
+       }, snap.elabSnap.infoTreeSnap.get.infoTree?)
     if let some next := snap.nextCmdSnap? then
       result :: go initialSnap next.task commands
     else

From b7b50cffd5697a41e1d59c6073e2a4bc3ed7fe01 Mon Sep 17 00:00:00 2001
From: Auguste Poiroux <augustepoiroux@gmail.com>
Date: Mon, 15 Sep 2025 18:30:24 +0200
Subject: [PATCH 11/13] Fix test v4.24.0-rc1

---
 test/in_command_dependency.expected.out | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/test/in_command_dependency.expected.out b/test/in_command_dependency.expected.out
index e3ba5583..66371d34 100644
--- a/test/in_command_dependency.expected.out
+++ b/test/in_command_dependency.expected.out
@@ -11,7 +11,7 @@
   {"severity": "info",
    "pos": {"line": 2, "column": 22},
    "endPos": {"line": 2, "column": 28},
-   "data": "Try this: exact x"}],
+   "data": "Try this:\n  exact x"}],
  "env": 0}
 
 {"sorries":
@@ -40,6 +40,6 @@
  [{"severity": "info",
    "pos": {"line": 0, "column": 0},
    "endPos": {"line": 0, "column": 0},
-   "data": "Try this: exact x"}],
+   "data": "Try this:\n  exact x"}],
  "goals": []}
 

From d3439426051484e1dd4c552b28d353c183206581 Mon Sep 17 00:00:00 2001
From: Auguste Poiroux <augustepoiroux@gmail.com>
Date: Wed, 22 Oct 2025 11:48:02 +0200
Subject: [PATCH 12/13] Fix test v4.25.0-rc1

---
 test/in_command_dependency.expected.out | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/test/in_command_dependency.expected.out b/test/in_command_dependency.expected.out
index 66371d34..e22d70ba 100644
--- a/test/in_command_dependency.expected.out
+++ b/test/in_command_dependency.expected.out
@@ -11,7 +11,7 @@
   {"severity": "info",
    "pos": {"line": 2, "column": 22},
    "endPos": {"line": 2, "column": 28},
-   "data": "Try this:\n  exact x"}],
+   "data": "Try this:\n  [apply] exact x"}],
  "env": 0}
 
 {"sorries":
@@ -40,6 +40,6 @@
  [{"severity": "info",
    "pos": {"line": 0, "column": 0},
    "endPos": {"line": 0, "column": 0},
-   "data": "Try this:\n  exact x"}],
+   "data": "Try this:\n  [apply] exact x"}],
  "goals": []}
 

From 5cf9d51b3fcfc95c22989d99ea5c78c4f4b031d0 Mon Sep 17 00:00:00 2001
From: Auguste Poiroux <augustepoiroux@gmail.com>
Date: Thu, 29 Jan 2026 13:10:20 +0100
Subject: [PATCH 13/13] Fix test v4.28.0-rc1

---
 test/in_command_dependency.expected.out | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/test/in_command_dependency.expected.out b/test/in_command_dependency.expected.out
index e22d70ba..faea5f3b 100644
--- a/test/in_command_dependency.expected.out
+++ b/test/in_command_dependency.expected.out
@@ -7,7 +7,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 8},
    "endPos": {"line": 1, "column": 9},
-   "data": "declaration uses 'sorry'"},
+   "data": "declaration uses `sorry`"},
   {"severity": "info",
    "pos": {"line": 2, "column": 22},
    "endPos": {"line": 2, "column": 28},
@@ -27,11 +27,11 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 8},
    "endPos": {"line": 1, "column": 9},
-   "data": "declaration uses 'sorry'"},
+   "data": "declaration uses `sorry`"},
   {"severity": "warning",
    "pos": {"line": 2, "column": 0},
    "endPos": {"line": 2, "column": 7},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 1}
 
 {"proofStatus": "Completed",