distinguish goalsBefore/goalsAfter

README.md

@@ -115,7 +115,7 @@ results in output
  [{"tactic": "exact rfl",
    "proofState": 0,
    "pos": {"line": 5, "column": 29},
-   "goals": "⊢ f + g = 39",
+   "goalsBefore": "⊢ f + g = 39",
    "endPos": {"line": 5, "column": 38}}],
  "env": 0}
  ```
@@ -143,11 +143,11 @@ Example usage:
 
 {"tactic": "apply Int.natAbs", "proofState": 0}
 
-{"proofState": 1, "goals": ["x : Unit\n⊢ Int"]}
+{"proofState": 1, "goalsBefore": ["x : Unit\n⊢ Int"]}
 
 {"tactic": "exact -37", "proofState": 1}
 
-{"proofState": 2, "goals": []}
+{"proofState": 2, "goalsBefore": []}
 ```
 
 You can use `sorry` in tactic mode.

REPL/JSON/REPL.lean

@@ -8,9 +8,9 @@ variable [Monad m] [MonadLiftT IO m]
 open JSON
 
 def TacticResult.toJson (t : TacticResult) : M m JSON.Tactic := do
-  let goals := "\n".intercalate (← t.proofState.ppGoals)
-  let proofStateId ← recordProofSnapshot t.proofState
-  return Tactic.of goals t.src t.pos t.endPos proofStateId
+  let goals := "\n".intercalate (← t.before.ppGoals)
+  let proofStateId ← recordProofSnapshot t.before
+  return Tactic.of goals none t.src t.pos t.endPos proofStateId
 
 def SorryResult.toJson (s : SorryResult) : M m JSON.Sorry := do
   return { ← TacticResult.toJson s.toTacticResult with }
@@ -62,7 +62,7 @@ def ProofStepResponse.toJson (r : ProofStepResponse) : M m JSON.ProofStepRespons
   let id ← recordProofSnapshot r.proofState
   return {
     proofState := id
-    goals := (← r.proofState.ppGoals)
+    goalsAfter := (← r.proofState.ppGoals)
     messages
     sorries
     traces := r.traces }

REPL/JSON/Types.lean

@@ -87,7 +87,8 @@ def Message.of (m : Lean.Message) : IO Message := do pure <|
 structure Tactic where
   pos : Pos
   endPos : Pos
-  goals : String
+  goalsBefore : String
+  goalsAfter? : Option String
   tactic : String
   /--
   The index of the proof state at the sorry.
@@ -97,10 +98,12 @@ structure Tactic where
 deriving ToJson
 
 /-- Construct the JSON representation of a Lean tactic. -/
-def Tactic.of (goals tactic : String) (pos endPos : Lean.Position) (proofState : Option Nat) : Tactic :=
+def Tactic.of (goalsBefore : String) (goalsAfter? : Option String) (tactic : String)
+    (pos endPos : Lean.Position) (proofState : Option Nat) : Tactic :=
   { pos := ⟨pos.line, pos.column⟩,
     endPos := ⟨endPos.line, endPos.column⟩,
-    goals,
+    goalsBefore,
+    goalsAfter?,
     tactic,
     proofState }
 
@@ -110,15 +113,16 @@ structure Sorry extends Tactic where
 
 instance : ToJson Sorry where
   toJson r := Json.mkObj <| .join [
-    [("goals", r.goals)],
+    [("goalsBefore", r.goalsBefore)],
+    match r.goalsAfter? with | .none => [] | .some a => [("goalsAfter", a)],
     [("proofState", toJson r.proofState)],
     if r.pos.line ≠ 0 then [("pos", toJson r.pos)] else [],
     if r.endPos.line ≠ 0 then [("endPos", toJson r.endPos)] else [],
   ]
 
 /-- Construct the JSON representation of a Lean sorry. -/
 def Sorry.of (goal : String) (pos endPos : Lean.Position) (proofState : Option Nat) : Sorry :=
-  { Tactic.of goal "sorry" pos endPos proofState with }
+  { Tactic.of goal none "sorry" pos endPos proofState with }
 
 structure Proof where
 
@@ -165,7 +169,7 @@ A response to a Lean tactic.
 -/
 structure ProofStepResponse where
   proofState : Nat
-  goals : List String
+  goalsAfter : List String
   messages : List Message := []
   sorries : List Sorry := []
   traces : List String
@@ -174,7 +178,7 @@ deriving ToJson
 instance : ToJson ProofStepResponse where
   toJson r := Json.mkObj <| .join [
     [("proofState", r.proofState)],
-    [("goals", toJson r.goals)],
+    [("goalsAfter", toJson r.goalsAfter)],
     Json.nonemptyList "messages" r.messages,
     Json.nonemptyList "sorries" r.sorries,
     Json.nonemptyList "traces" r.traces

REPL/Main.lean

@@ -235,7 +235,8 @@ def recordProofSnapshot (proofState : ProofSnapshot) : M m Nat := do
   return id
 
 structure TacticResult where
-  proofState : ProofSnapshot
+  before : ProofSnapshot
+  after? : Option ProofSnapshot := none
   src : String
   stx : Syntax
   pos : Position
@@ -249,7 +250,10 @@ def tactics (trees : List InfoTree) : m (List TacticResult) :=
   trees.bind InfoTree.tactics |>.mapM
     fun ⟨ctx, stx, goals, pos, endPos⟩ => do
       let src := Format.pretty (← ppTactic ctx stx)
-      return { proofState := (← ProofSnapshot.create ctx none none goals), pos, endPos, src, stx }
+      return {
+        after? := none,
+        before := (← ProofSnapshot.create ctx none none goals),
+        pos, endPos, src, stx }
 where ppTactic (ctx : ContextInfo) (stx : Syntax) : IO Format :=
   ctx.runMetaM {} try
     Lean.PrettyPrinter.ppTactic ⟨stx⟩
@@ -261,9 +265,9 @@ def sorries (trees : List InfoTree) (env? : Option Environment) : m (List SorryR
     fun ⟨ctx, g, pos, endPos⟩ => do
       match g with
       | .tactic g => do
-        pure <| some { proofState := (← ProofSnapshot.create ctx none env? [g]), pos, endPos }
+        pure <| some { before := (← ProofSnapshot.create ctx none env? [g]), pos, endPos }
       | .term lctx (some t) => do
-        pure <| some { proofState := (← ProofSnapshot.create ctx lctx env? [] [t]), pos, endPos }
+        pure <| some { before := (← ProofSnapshot.create ctx lctx env? [] [t]), pos, endPos }
       | .term _ none =>
         pure none
 

test/Mathlib/test/20240209.expected.out

@@ -16,5 +16,5 @@
    "pos": {"line": 0, "column": 0},
    "endPos": {"line": 0, "column": 0},
    "data": "unsolved goals\n⊢ False"}],
- "goals": []}
+ "goalsBefore": []}
 

test/Mathlib/test/exact.expected.out

@@ -18,7 +18,7 @@
    "pos": {"line": 0, "column": 0},
    "endPos": {"line": 0, "column": 0},
    "data": "Try this: exact Nat.zero_lt_one"}],
- "goals": []}
+ "goalsBefore": []}
 
 {"sorries":
  [{"proofState": 2,

test/Mathlib/test/induction.expected.out

@@ -18,12 +18,12 @@
   "case succ\nn✝ : ℕ\nn_ih✝ : n✝ = n✝\n⊢ Nat.succ n✝ = Nat.succ n✝"]}
 
 {"proofState": 2,
- "goals": ["case succ\nn✝ : ℕ\nn_ih✝ : n✝ = n✝\n⊢ Nat.succ n✝ = Nat.succ n✝"]}
+ "goalsBefore": ["case succ\nn✝ : ℕ\nn_ih✝ : n✝ = n✝\n⊢ Nat.succ n✝ = Nat.succ n✝"]}
 
 {"sorries":
  [{"proofState": 3, "goal": "case zero\n⊢ Nat.zero = Nat.zero"},
   {"proofState": 4,
    "goal": "case succ\nx : ℕ\nn_ih✝ : x = x\n⊢ Nat.succ x = Nat.succ x"}],
  "proofState": 5,
- "goals": []}
+ "goalsBefore": []}
 

test/Mathlib/test/pickle.expected.out

@@ -12,5 +12,5 @@
    "data": "declaration uses 'sorry'"}],
  "env": 1}
 
-{"proofState": 1, "goals": ["x : ℕ\nh : 2 * (2 * (2 * (2 * x))) = 48\n⊢ x = 3"]}
+{"proofState": 1, "goalsBefore": ["x : ℕ\nh : 2 * (2 * (2 * (2 * x))) = 48\n⊢ x = 3"]}
 

test/Mathlib/test/pickle_2.expected.out

@@ -1,4 +1,4 @@
-{"proofState": 0, "goals": ["x : ℕ\nh : 2 * (2 * (2 * (2 * x))) = 48\n⊢ x = 3"]}
+{"proofState": 0, "goalsBefore": ["x : ℕ\nh : 2 * (2 * (2 * (2 * x))) = 48\n⊢ x = 3"]}
 
-{"proofState": 1, "goals": ["x : ℕ\nh : 2 * (2 * (2 * (2 * x))) = 48\n⊢ x = 3"]}
+{"proofState": 1, "goalsBefore": ["x : ℕ\nh : 2 * (2 * (2 * (2 * x))) = 48\n⊢ x = 3"]}
 

test/all_tactics.expected.out

@@ -3,12 +3,12 @@
    [{"tactic": "have t := 37",
      "proofState": 0,
      "pos": {"line": 1, "column": 18},
-     "goals": "⊢ Nat",
+     "goalsBefore": "⊢ Nat",
      "endPos": {"line": 1, "column": 30}},
     {"tactic": "exact t",
      "proofState": 1,
      "pos": {"line": 1, "column": 32},
-     "goals": "t : Nat\n⊢ Nat",
+     "goalsBefore": "t : Nat\n⊢ Nat",
      "endPos": {"line": 1, "column": 39}}],
    "source": "def f : Nat := by have t := 37; exact t",
    "env": 0}]}

test/by_cases.expected.out

@@ -3,7 +3,7 @@
    "sorries":
    [{"proofState": 0,
      "pos": {"line": 1, "column": 36},
-     "goals": "x : Int\n⊢ x = x",
+     "goalsBefore": "x : Int\n⊢ x = x",
      "endPos": {"line": 1, "column": 41}}],
    "messages":
    [{"severity": "warning",
@@ -13,15 +13,15 @@
    "env": 0}]}
 
 {"proofState": 1,
- "goals":
+ "goalsAfter":
  ["case pos\nx : Int\nh : x < 0\n⊢ x = x",
   "case neg\nx : Int\nh : ¬x < 0\n⊢ x = x"]}
 
-{"proofState": 2, "goals": ["case neg\nx : Int\nh : ¬x < 0\n⊢ x = x"]}
+{"proofState": 2, "goalsAfter": ["case neg\nx : Int\nh : ¬x < 0\n⊢ x = x"]}
 
 {"sorries":
- [{"proofState": 3, "goals": "case pos\nx : Int\nh : x < 0\n⊢ x = x"},
-  {"proofState": 4, "goals": "case neg\nx : Int\nh : ¬x < 0\n⊢ x = x"}],
+ [{"proofState": 3, "goalsBefore": "case pos\nx : Int\nh : x < 0\n⊢ x = x"},
+  {"proofState": 4, "goalsBefore": "case neg\nx : Int\nh : ¬x < 0\n⊢ x = x"}],
  "proofState": 5,
- "goals": []}
+ "goalsAfter": []}
 

test/calc.expected.out

@@ -3,28 +3,28 @@
    [{"tactic": "calc\n  3 = 4 := by sorry\n  4 = 5 := by sorry",
      "proofState": 2,
      "pos": {"line": 1, "column": 22},
-     "goals": "⊢ 3 = 5",
+     "goalsBefore": "⊢ 3 = 5",
      "endPos": {"line": 3, "column": 19}},
     {"tactic": "sorry",
      "proofState": 3,
      "pos": {"line": 2, "column": 14},
-     "goals": "⊢ 3 = 4",
+     "goalsBefore": "⊢ 3 = 4",
      "endPos": {"line": 2, "column": 19}},
     {"tactic": "sorry",
      "proofState": 4,
      "pos": {"line": 3, "column": 14},
-     "goals": "⊢ 4 = 5",
+     "goalsBefore": "⊢ 4 = 5",
      "endPos": {"line": 3, "column": 19}}],
    "source":
    "example : 3 = 5 := by\n  calc\n    3 = 4 := by sorry\n    4 = 5 := by sorry",
    "sorries":
    [{"proofState": 0,
      "pos": {"line": 2, "column": 14},
-     "goals": "⊢ 3 = 4",
+     "goalsBefore": "⊢ 3 = 4",
      "endPos": {"line": 2, "column": 19}},
     {"proofState": 1,
      "pos": {"line": 3, "column": 14},
-     "goals": "⊢ 4 = 5",
+     "goalsBefore": "⊢ 4 = 5",
      "endPos": {"line": 3, "column": 19}}],
    "messages":
    [{"severity": "warning",

test/file.expected.out

@@ -5,7 +5,7 @@
    [{"tactic": "exact rfl",
      "proofState": 0,
      "pos": {"line": 5, "column": 29},
-     "goals": "⊢ f + g = 39",
+     "goalsBefore": "⊢ f + g = 39",
      "endPos": {"line": 5, "column": 38}}],
    "source": "theorem h : f + g = 39 := by exact rfl",
    "env": 2}]}

test/have_by_sorry.expected.out

@@ -3,7 +3,7 @@
    "sorries":
    [{"proofState": 0,
      "pos": {"line": 2, "column": 23},
-     "goals": "x : Int\n⊢ x = 1",
+     "goalsBefore": "x : Int\n⊢ x = 1",
      "endPos": {"line": 2, "column": 28}}],
    "messages":
    [{"severity": "error",
@@ -21,7 +21,7 @@
    "sorries":
    [{"proofState": 1,
      "pos": {"line": 1, "column": 36},
-     "goals": "x : Int\n⊢ x = x",
+     "goalsBefore": "x : Int\n⊢ x = x",
      "endPos": {"line": 1, "column": 41}}],
    "messages":
    [{"severity": "warning",
@@ -30,7 +30,7 @@
      "data": "declaration uses 'sorry'"}],
    "env": 1}]}
 
-{"sorries": [{"proofState": 2, "goals": "x : Int\n⊢ x = 1"}],
+{"sorries": [{"proofState": 2, "goalsBefore": "x : Int\n⊢ x = 1"}],
  "proofState": 3,
- "goals": ["x : Int\nh : x = 1\n⊢ x = 1"]}
+ "goalsAfter": ["x : Int\nh : x = 1\n⊢ x = 1"]}
 

test/incrementality.expected.out

@@ -4,7 +4,7 @@
    "sorries":
    [{"proofState": 0,
      "pos": {"line": 3, "column": 2},
-     "goals": "⊢ True",
+     "goalsBefore": "⊢ True",
      "endPos": {"line": 3, "column": 7}}],
    "messages":
    [{"severity": "warning",
@@ -18,7 +18,7 @@
    "sorries":
    [{"proofState": 1,
      "pos": {"line": 3, "column": 2},
-     "goals": "⊢ True",
+     "goalsBefore": "⊢ True",
      "endPos": {"line": 3, "column": 7}}],
    "messages":
    [{"severity": "warning",
@@ -32,7 +32,7 @@
    "sorries":
    [{"proofState": 2,
      "pos": {"line": 3, "column": 2},
-     "goals": "⊢ True",
+     "goalsBefore": "⊢ True",
      "endPos": {"line": 3, "column": 7}}],
    "messages":
    [{"severity": "warning",

test/incrementality_2.expected.out

@@ -18,7 +18,7 @@
    "sorries":
    [{"proofState": 0,
      "pos": {"line": 3, "column": 2},
-     "goals": "⊢ True",
+     "goalsBefore": "⊢ True",
      "endPos": {"line": 3, "column": 7}}],
    "messages":
    [{"severity": "warning",

test/invalid_tactic.expected.out

@@ -3,7 +3,7 @@
    "sorries":
    [{"proofState": 0,
      "pos": {"line": 1, "column": 43},
-     "goals": "x : Nat\n⊢ x = x",
+     "goalsBefore": "x : Nat\n⊢ x = x",
      "endPos": {"line": 1, "column": 48}}],
    "messages":
    [{"severity": "warning",
@@ -18,5 +18,5 @@
    "pos": {"line": 0, "column": 0},
    "endPos": {"line": 0, "column": 0},
    "data": "unknown identifier 'my_fake_premise'"}],
- "goals": []}
+ "goalsAfter": []}