From 8562cf0dc1db9fd2fd69517ba581ba773614b1c9 Mon Sep 17 00:00:00 2001
From: Auguste Poiroux <augustepoiroux@gmail.com>
Date: Thu, 2 Jan 2025 12:52:13 +0100
Subject: [PATCH] Add proofStatus field in ProofStepResponse + update tests

---
 REPL/JSON.lean                             |  4 +-
 REPL/Main.lean                             | 97 ++++++++++------------
 REPL/Snapshots.lean                        |  7 +-
 test/Mathlib/test/20240209.expected.out    |  3 +-
 test/Mathlib/test/H20231115.expected.out   |  3 +-
 test/Mathlib/test/exact.expected.out       |  3 +-
 test/Mathlib/test/induction.expected.out   |  7 +-
 test/Mathlib/test/on_goal.expected.out     |  1 +
 test/Mathlib/test/pickle.expected.out      |  4 +-
 test/Mathlib/test/pickle_2.expected.out    |  8 +-
 test/by_cases.expected.out                 | 13 ++-
 test/have_by_sorry.expected.out            |  1 +
 test/import_lean.expected.out              |  2 +
 test/invalid_tactic.expected.out           |  9 +-
 test/name_generator.expected.out           | 18 +++-
 test/pickle_proof_state_1.expected.out     | 22 +++--
 test/pickle_proof_state_2.expected.out     |  6 +-
 test/pickle_proof_state_env.expected.out   | 22 +++--
 test/pickle_scoped_notation.expected.out   | 16 ++++
 test/pickle_scoped_notation_2.expected.out |  9 ++
 test/proof_step.expected.out               | 10 ++-
 test/readme.expected.out                   |  6 +-
 test/self_proof_check.expected.out         | 25 ++++++
 test/self_proof_check.in                   |  5 ++
 test/self_proof_exact_check.expected.out   | 29 +++++++
 test/self_proof_exact_check.in             |  6 ++
 test/sorry_hypotheses.expected.out         |  1 +
 test/tactic_mode_sorry.expected.out        |  5 +-
 test/trace_simp.expected.out               |  6 +-
 29 files changed, 246 insertions(+), 102 deletions(-)
 create mode 100644 test/import_lean.expected.out
 create mode 100644 test/pickle_scoped_notation.expected.out
 create mode 100644 test/pickle_scoped_notation_2.expected.out
 create mode 100644 test/self_proof_check.expected.out
 create mode 100644 test/self_proof_check.in
 create mode 100644 test/self_proof_exact_check.expected.out
 create mode 100644 test/self_proof_exact_check.in

diff --git a/REPL/JSON.lean b/REPL/JSON.lean
index d5c5ba2..5398c4e 100644
--- a/REPL/JSON.lean
+++ b/REPL/JSON.lean
@@ -150,6 +150,7 @@ structure ProofStepResponse where
   messages : List Message := []
   sorries : List Sorry := []
   traces : List String
+  proofStatus : String
 deriving ToJson, FromJson
 
 instance : ToJson ProofStepResponse where
@@ -158,7 +159,8 @@ instance : ToJson ProofStepResponse where
     [("goals", toJson r.goals)],
     Json.nonemptyList "messages" r.messages,
     Json.nonemptyList "sorries" r.sorries,
-    Json.nonemptyList "traces" r.traces
+    Json.nonemptyList "traces" r.traces,
+    [("proofStatus", r.proofStatus)]
   ]
 
 /-- Json wrapper for an error. -/
diff --git a/REPL/Main.lean b/REPL/Main.lean
index ff471a9..ca05d94 100644
--- a/REPL/Main.lean
+++ b/REPL/Main.lean
@@ -94,17 +94,18 @@ def recordProofSnapshot (proofState : ProofSnapshot) : M m Nat := do
   modify fun s => { s with proofStates := s.proofStates.push proofState }
   return id
 
-def sorries (trees : List InfoTree) (env? : Option Environment) : M m (List Sorry) :=
+def sorries (trees : List InfoTree) (env? : Option Environment) (initGoals? : Option (List MVarId))
+: M m (List Sorry) :=
   trees.flatMap InfoTree.sorries |>.filter (fun t => match t.2.1 with
     | .term _ none => false
     | _ => true ) |>.mapM
       fun ⟨ctx, g, pos, endPos⟩ => do
         let (goal, proofState) ← match g with
         | .tactic g => do
-           let s ← ProofSnapshot.create ctx none env? [g]
+           let s ← ProofSnapshot.create ctx none env? [g] initGoals?
            pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s)
         | .term lctx (some t) => do
-           let s ← ProofSnapshot.create ctx lctx env? [] [t]
+           let s ← ProofSnapshot.create ctx lctx env? [] initGoals? [t]
            pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s)
         | .term _ none => unreachable!
         let proofStateId ← proofState.mapM recordProofSnapshot
@@ -126,55 +127,47 @@ def tactics (trees : List InfoTree) : M m (List Tactic) :=
       return Tactic.of goals tactic pos endPos proofStateId ns
 
 /-- Inspired from LeanDojo REPL. -/
-def validateProof (proofState : ProofSnapshot) : M m Message := do
-  let res := proofState.runMetaM do
-    match proofState.initialGoals with
-    | [goalId] =>
-      match proofState.metaState.mctx.getExprAssignmentCore? goalId with
-      | none => return ("Goal not assigned", Severity.error)
-      | some pf => do
-        let pf ← instantiateMVars pf
-        let pft ← Meta.inferType pf >>= instantiateMVars
-        if pf.hasSorry then
-          return ("Proof contains sorry", Severity.warning)
-        if pf.hasExprMVar then
-          return ("Proof contains metavariable", Severity.error)
-
-        -- temporary: check only for one declaration
-        let declCI := proofState.coreState.env.constants.map₂.toList.head!.snd
-
-        let decl := match declCI with
-        | .defnInfo info => some (Declaration.defnDecl ({
-              info with name := Name.anonymous, type := pft, value := pf
-            }))
-        | .thmInfo info => some (Declaration.thmDecl ({
-              info with name := Name.anonymous, type := pft, value := pf
-            }))
-        | _ => none
-
-        match decl with
-        | none => return ("Proof not verified", Severity.warning)
-        | some decl => do
-          try
-            let _ ← addDecl decl
-          catch ex =>
-            return (s!"Kernel type check failed: {← ex.toMessageData.toString}", Severity.error)
-          return ("Proof finished", Severity.info)
-
-    | _ => return ("More than one initial goal", Severity.error)
-
-  return {
-      pos := {line := 0, column := 0},
-      endPos := none,
-      severity := (← res).fst.snd,
-      data := (← res).fst.fst
-    }
+def getProofStatus (proofState : ProofSnapshot) : M m String := do
+  match proofState.tacticState.goals with
+    | [] =>
+      let res := proofState.runMetaM do
+        match proofState.initialGoals with
+        | [goalId] =>
+          match proofState.metaState.mctx.getExprAssignmentCore? goalId with
+          | none => return "Error: Goal not assigned"
+          | some pf => do
+            let pf ← instantiateMVars pf
+            let pft ← Meta.inferType pf >>= instantiateMVars
+            if pf.hasSorry then
+              return "Incomplete: contains sorry"
+            if pf.hasExprMVar then
+              return "Incomplete: contains metavariable(s)"
+
+            let decl := Declaration.defnDecl ({
+              name := Name.anonymous,
+              type := pft,
+              value := pf,
+              levelParams := [],
+              hints := ReducibilityHints.opaque,
+              safety := DefinitionSafety.safe
+            })
+
+            try
+              let _ ← addDecl decl
+            catch ex =>
+              return s!"Error: kernel type check failed: {← ex.toMessageData.toString}"
+            return "Completed"
+
+        | _ => return "Not verified: more than one initial goal"
+      return (← res).fst
+
+    | _ => return "Incomplete: open goals remain"
 
 /-- Record a `ProofSnapshot` and generate a JSON response for it. -/
 def createProofStepReponse (proofState : ProofSnapshot) (old? : Option ProofSnapshot := none) :
     M m ProofStepResponse := do
   let messages := proofState.newMessages old?
-  let mut messages ← messages.mapM fun m => Message.of m
+  let messages ← messages.mapM fun m => Message.of m
   let traces ← proofState.newTraces old?
   let trees := proofState.newInfoTrees old?
   let trees ← match old? with
@@ -185,17 +178,15 @@ def createProofStepReponse (proofState : ProofSnapshot) (old? : Option ProofSnap
   | none => pure trees
   -- For debugging purposes, sometimes we print out the trees here:
   -- trees.forM fun t => do IO.println (← t.format)
-  let sorries ← sorries trees none
+  let sorries ← sorries trees none (some proofState.initialGoals)
   let id ← recordProofSnapshot proofState
-  if proofState.tacticState.goals.isEmpty then
-    messages := messages ++ [← validateProof proofState]
-
   return {
     proofState := id
     goals := (← proofState.ppGoals).map fun s => s!"{s}"
     messages
     sorries
-    traces }
+    traces
+    proofStatus := (← getProofStatus proofState) }
 
 /-- Pickle a `CommandSnapshot`, generating a JSON response. -/
 def pickleCommandSnapshot (n : PickleEnvironment) : M m (CommandResponse ⊕ Error) := do
@@ -251,7 +242,7 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
   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?.map (·.env))
+  let sorries ← sorries trees (initialCmdState?.map (·.env)) none
   let tactics ← match s.allTactics with
   | some true => tactics trees
   | _ => pure []
diff --git a/REPL/Snapshots.lean b/REPL/Snapshots.lean
index 6b8f192..bed5521 100644
--- a/REPL/Snapshots.lean
+++ b/REPL/Snapshots.lean
@@ -192,7 +192,8 @@ For convenience, we also allow a list of `Expr`s, and these are appended to the
 as fresh metavariables with the given types.
 -/
 def create (ctx : ContextInfo) (lctx? : Option LocalContext) (env? : Option Environment)
-    (goals : List MVarId) (types : List Expr := []) : IO ProofSnapshot := do
+    (goals : List MVarId) (initGoals? : 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
@@ -208,7 +209,9 @@ def create (ctx : ContextInfo) (lctx? : Option LocalContext) (env? : Option Envi
       termContext := {}
       tacticState := { goals }
       tacticContext := { elaborator := .anonymous }
-      initialGoals := goals }
+      initialGoals := match initGoals? with
+        | none => goals
+        | some gs => gs }
 
 open Lean.Core in
 /-- A copy of `Core.State` with the `Environment`, caches, and logging omitted. -/
diff --git a/test/Mathlib/test/20240209.expected.out b/test/Mathlib/test/20240209.expected.out
index b83ff66..b7cfc2d 100644
--- a/test/Mathlib/test/20240209.expected.out
+++ b/test/Mathlib/test/20240209.expected.out
@@ -10,7 +10,8 @@
    "data": "declaration uses 'sorry'"}],
  "env": 0}
 
-{"proofState": 1,
+{"proofStatus": "Incomplete: contains sorry",
+ "proofState": 1,
  "messages":
  [{"severity": "error",
    "pos": {"line": 0, "column": 0},
diff --git a/test/Mathlib/test/H20231115.expected.out b/test/Mathlib/test/H20231115.expected.out
index 2efb1d8..e283b37 100644
--- a/test/Mathlib/test/H20231115.expected.out
+++ b/test/Mathlib/test/H20231115.expected.out
@@ -12,7 +12,8 @@
    "data": "declaration uses 'sorry'"}],
  "env": 1}
 
-{"proofState": 1,
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 1,
  "goals":
  ["case zero\n⊢ 0 + 1 > 0",
   "case succ\nx : Nat\nhx : x + 1 > x\n⊢ x + 1 + 1 > x + 1"]}
diff --git a/test/Mathlib/test/exact.expected.out b/test/Mathlib/test/exact.expected.out
index 86cd1c6..39e7796 100644
--- a/test/Mathlib/test/exact.expected.out
+++ b/test/Mathlib/test/exact.expected.out
@@ -12,7 +12,8 @@
    "data": "declaration uses 'sorry'"}],
  "env": 1}
 
-{"proofState": 1,
+{"proofStatus": "Completed",
+ "proofState": 1,
  "messages":
  [{"severity": "info",
    "pos": {"line": 0, "column": 0},
diff --git a/test/Mathlib/test/induction.expected.out b/test/Mathlib/test/induction.expected.out
index 7ef34d3..7f80087 100644
--- a/test/Mathlib/test/induction.expected.out
+++ b/test/Mathlib/test/induction.expected.out
@@ -12,16 +12,19 @@
    "data": "declaration uses 'sorry'"}],
  "env": 1}
 
-{"proofState": 1,
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 1,
  "goals":
  ["case zero\n⊢ 0 = 0", "case succ\nn✝ : ℕ\na✝ : n✝ = n✝\n⊢ n✝ + 1 = n✝ + 1"]}
 
-{"proofState": 2,
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 2,
  "goals": ["case succ\nn✝ : ℕ\na✝ : n✝ = n✝\n⊢ n✝ + 1 = n✝ + 1"]}
 
 {"sorries":
  [{"proofState": 3, "goal": "case zero\n⊢ 0 = 0"},
   {"proofState": 4, "goal": "case succ\nx : ℕ\na✝ : x = x\n⊢ x + 1 = x + 1"}],
+ "proofStatus": "Incomplete: contains sorry",
  "proofState": 5,
  "goals": []}
 
diff --git a/test/Mathlib/test/on_goal.expected.out b/test/Mathlib/test/on_goal.expected.out
index e332586..510cfe1 100644
--- a/test/Mathlib/test/on_goal.expected.out
+++ b/test/Mathlib/test/on_goal.expected.out
@@ -15,6 +15,7 @@
 {"sorries":
  [{"proofState": 1, "goal": "x : ℝ\nh0 : |x| > 1\n⊢ x = x"},
   {"proofState": 2, "goal": "x : ℝ\nh0 : |x| > 1\nh1 : x = x\n⊢ x = x"}],
+ "proofStatus": "Incomplete: open goals remain",
  "proofState": 3,
  "goals":
  ["case pos\nx : ℝ\nh0 : |x| > 1\nh1 h2 : x = x\nh3 : x < 0\n⊢ x < 0 ∨ 2 * x > 2",
diff --git a/test/Mathlib/test/pickle.expected.out b/test/Mathlib/test/pickle.expected.out
index 598ba42..e3d1c16 100644
--- a/test/Mathlib/test/pickle.expected.out
+++ b/test/Mathlib/test/pickle.expected.out
@@ -12,5 +12,7 @@
    "data": "declaration uses 'sorry'"}],
  "env": 1}
 
-{"proofState": 1, "goals": ["x : ℕ\nh : 2 * (2 * (2 * (2 * x))) = 48\n⊢ x = 3"]}
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 1,
+ "goals": ["x : ℕ\nh : 2 * (2 * (2 * (2 * x))) = 48\n⊢ x = 3"]}
 
diff --git a/test/Mathlib/test/pickle_2.expected.out b/test/Mathlib/test/pickle_2.expected.out
index d484cb9..f614f97 100644
--- a/test/Mathlib/test/pickle_2.expected.out
+++ b/test/Mathlib/test/pickle_2.expected.out
@@ -1,4 +1,8 @@
-{"proofState": 0, "goals": ["x : ℕ\nh : 2 * (2 * (2 * (2 * x))) = 48\n⊢ x = 3"]}
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 0,
+ "goals": ["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"]}
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 1,
+ "goals": ["x : ℕ\nh : 2 * (2 * (2 * (2 * x))) = 48\n⊢ x = 3"]}
 
diff --git a/test/by_cases.expected.out b/test/by_cases.expected.out
index b1ccbd3..978df50 100644
--- a/test/by_cases.expected.out
+++ b/test/by_cases.expected.out
@@ -10,21 +10,20 @@
    "data": "declaration uses 'sorry'"}],
  "env": 0}
 
-{"proofState": 1,
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 1,
  "goals":
  ["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"]}
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 2,
+ "goals": ["case neg\nx : Int\nh : ¬x < 0\n⊢ x = x"]}
 
 {"sorries":
  [{"proofState": 3, "goal": "case pos\nx : Int\nh : x < 0\n⊢ x = x"},
   {"proofState": 4, "goal": "case neg\nx : Int\nh : ¬x < 0\n⊢ x = x"}],
+ "proofStatus": "Incomplete: contains sorry",
  "proofState": 5,
- "messages":
- [{"severity": "warning",
-   "pos": {"line": 0, "column": 0},
-   "endPos": null,
-   "data": "Proof contains sorry"}],
  "goals": []}
 
diff --git a/test/have_by_sorry.expected.out b/test/have_by_sorry.expected.out
index 1f792a7..03c7901 100644
--- a/test/have_by_sorry.expected.out
+++ b/test/have_by_sorry.expected.out
@@ -23,6 +23,7 @@
  "env": 1}
 
 {"sorries": [{"proofState": 2, "goal": "x : Int\n⊢ x = 1"}],
+ "proofStatus": "Incomplete: open goals remain",
  "proofState": 3,
  "goals": ["x : Int\nh : x = 1\n⊢ x = 1"]}
 
diff --git a/test/import_lean.expected.out b/test/import_lean.expected.out
new file mode 100644
index 0000000..4855ce4
--- /dev/null
+++ b/test/import_lean.expected.out
@@ -0,0 +1,2 @@
+{"env": 0}
+
diff --git a/test/invalid_tactic.expected.out b/test/invalid_tactic.expected.out
index 10fbab9..3ba2c50 100644
--- a/test/invalid_tactic.expected.out
+++ b/test/invalid_tactic.expected.out
@@ -10,15 +10,12 @@
    "data": "declaration uses 'sorry'"}],
  "env": 0}
 
-{"proofState": 1,
+{"proofStatus": "Incomplete: contains sorry",
+ "proofState": 1,
  "messages":
  [{"severity": "error",
    "pos": {"line": 0, "column": 0},
    "endPos": {"line": 0, "column": 0},
-   "data": "unknown identifier 'my_fake_premise'"},
-  {"severity": "warning",
-   "pos": {"line": 0, "column": 0},
-   "endPos": null,
-   "data": "Proof contains sorry"}],
+   "data": "unknown identifier 'my_fake_premise'"}],
  "goals": []}
 
diff --git a/test/name_generator.expected.out b/test/name_generator.expected.out
index b4d885b..01213b5 100644
--- a/test/name_generator.expected.out
+++ b/test/name_generator.expected.out
@@ -11,31 +11,40 @@
  "env": 0}
 
 {"sorries": [{"proofState": 1, "goal": "x : Int\nh0 : x > 0\n⊢ x > 0"}],
+ "proofStatus": "Incomplete: open goals remain",
  "proofState": 2,
  "goals": ["x : Int\nh0 h : x > 0\n⊢ False"]}
 
-{"proofState": 3, "goals": []}
+{"proofStatus": "Incomplete: contains metavariable(s)",
+ "proofState": 3,
+ "goals": []}
 
-{"proofState": 4, "goals": []}
+{"proofStatus": "Incomplete: contains metavariable(s)",
+ "proofState": 4,
+ "goals": []}
 
 {"traces":
  ["[Meta.Tactic.simp.rewrite] of_eq_true (eq_true h0):1000, x > 0 ==> True"],
+ "proofStatus": "Incomplete: contains metavariable(s)",
  "proofState": 5,
  "goals": []}
 
 {"traces":
  ["[Meta.Tactic.simp.rewrite] gt_iff_lt:1000, x > 0 ==> 0 < x",
   "[Meta.Tactic.simp.rewrite] h0:1000, 0 < x ==> True"],
+ "proofStatus": "Incomplete: contains metavariable(s)",
  "proofState": 6,
  "goals": []}
 
 {"traces":
  ["[Meta.Tactic.simp.rewrite] gt_iff_lt:1000, x > 0 ==> 0 < x",
   "[Meta.Tactic.simp.rewrite] h0:1000, 0 < x ==> True"],
+ "proofStatus": "Incomplete: contains metavariable(s)",
  "proofState": 7,
  "goals": []}
 
-{"proofState": 8,
+{"proofStatus": "Incomplete: contains sorry",
+ "proofState": 8,
  "messages":
  [{"severity": "error",
    "pos": {"line": 0, "column": 0},
@@ -43,7 +52,8 @@
    "data": "unsolved goals\nx : Int\nh0 : x > 0\n⊢ x > 0"}],
  "goals": []}
 
-{"proofState": 9,
+{"proofStatus": "Incomplete: contains sorry",
+ "proofState": 9,
  "messages":
  [{"severity": "error",
    "pos": {"line": 0, "column": 0},
diff --git a/test/pickle_proof_state_1.expected.out b/test/pickle_proof_state_1.expected.out
index 86668df..238b74c 100644
--- a/test/pickle_proof_state_1.expected.out
+++ b/test/pickle_proof_state_1.expected.out
@@ -12,15 +12,25 @@
    "data": "declaration uses 'sorry'"}],
  "env": 1}
 
-{"proofState": 1, "goals": ["⊢ Nat"]}
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 1,
+ "goals": ["⊢ Nat"]}
 
-{"proofState": 2, "goals": ["⊢ Nat"]}
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 2,
+ "goals": ["⊢ Nat"]}
 
-{"proofState": 3, "goals": ["t : Nat\n⊢ Nat"]}
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 3,
+ "goals": ["t : Nat\n⊢ Nat"]}
 
-{"proofState": 4, "goals": ["t : Nat\n⊢ Nat"]}
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 4,
+ "goals": ["t : Nat\n⊢ Nat"]}
 
-{"proofState": 5, "goals": ["t : Nat\n⊢ Nat"]}
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 5,
+ "goals": ["t : Nat\n⊢ Nat"]}
 
-{"proofState": 6, "goals": []}
+{"proofStatus": "Completed", "proofState": 6, "goals": []}
 
diff --git a/test/pickle_proof_state_2.expected.out b/test/pickle_proof_state_2.expected.out
index 09a6bdf..8a6bb9d 100644
--- a/test/pickle_proof_state_2.expected.out
+++ b/test/pickle_proof_state_2.expected.out
@@ -1,4 +1,6 @@
-{"proofState": 0, "goals": ["t : Nat\n⊢ Nat"]}
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 0,
+ "goals": ["t : Nat\n⊢ Nat"]}
 
-{"proofState": 1, "goals": []}
+{"proofStatus": "Completed", "proofState": 1, "goals": []}
 
diff --git a/test/pickle_proof_state_env.expected.out b/test/pickle_proof_state_env.expected.out
index 86668df..238b74c 100644
--- a/test/pickle_proof_state_env.expected.out
+++ b/test/pickle_proof_state_env.expected.out
@@ -12,15 +12,25 @@
    "data": "declaration uses 'sorry'"}],
  "env": 1}
 
-{"proofState": 1, "goals": ["⊢ Nat"]}
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 1,
+ "goals": ["⊢ Nat"]}
 
-{"proofState": 2, "goals": ["⊢ Nat"]}
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 2,
+ "goals": ["⊢ Nat"]}
 
-{"proofState": 3, "goals": ["t : Nat\n⊢ Nat"]}
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 3,
+ "goals": ["t : Nat\n⊢ Nat"]}
 
-{"proofState": 4, "goals": ["t : Nat\n⊢ Nat"]}
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 4,
+ "goals": ["t : Nat\n⊢ Nat"]}
 
-{"proofState": 5, "goals": ["t : Nat\n⊢ Nat"]}
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 5,
+ "goals": ["t : Nat\n⊢ Nat"]}
 
-{"proofState": 6, "goals": []}
+{"proofStatus": "Completed", "proofState": 6, "goals": []}
 
diff --git a/test/pickle_scoped_notation.expected.out b/test/pickle_scoped_notation.expected.out
new file mode 100644
index 0000000..77c3f23
--- /dev/null
+++ b/test/pickle_scoped_notation.expected.out
@@ -0,0 +1,16 @@
+{"env": 0}
+
+{"env": 1}
+
+{"env": 2}
+
+{"env": 3}
+
+{"env": 4}
+
+{"env": 5}
+
+{"env": 6}
+
+{"env": 5}
+
diff --git a/test/pickle_scoped_notation_2.expected.out b/test/pickle_scoped_notation_2.expected.out
new file mode 100644
index 0000000..2d22671
--- /dev/null
+++ b/test/pickle_scoped_notation_2.expected.out
@@ -0,0 +1,9 @@
+{"env": 0}
+
+{"messages":
+ [{"severity": "error",
+   "pos": {"line": 1, "column": 18},
+   "endPos": {"line": 1, "column": 21},
+   "data": "unexpected token ':='; expected term"}],
+ "env": 1}
+
diff --git a/test/proof_step.expected.out b/test/proof_step.expected.out
index 2a26468..013889b 100644
--- a/test/proof_step.expected.out
+++ b/test/proof_step.expected.out
@@ -10,9 +10,13 @@
    "data": "declaration uses 'sorry'"}],
  "env": 0}
 
-{"proofState": 1, "goals": ["⊢ Int"]}
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 1,
+ "goals": ["⊢ Int"]}
 
-{"proofState": 2, "goals": ["t : Nat\n⊢ Nat"]}
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 2,
+ "goals": ["t : Nat\n⊢ Nat"]}
 
-{"proofState": 3, "goals": []}
+{"proofStatus": "Completed", "proofState": 3, "goals": []}
 
diff --git a/test/readme.expected.out b/test/readme.expected.out
index 71ab066..7ffa110 100644
--- a/test/readme.expected.out
+++ b/test/readme.expected.out
@@ -10,7 +10,9 @@
    "data": "declaration uses 'sorry'"}],
  "env": 0}
 
-{"proofState": 1, "goals": ["x : Unit\n⊢ Int"]}
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 1,
+ "goals": ["x : Unit\n⊢ Int"]}
 
-{"proofState": 2, "goals": []}
+{"proofStatus": "Completed", "proofState": 2, "goals": []}
 
diff --git a/test/self_proof_check.expected.out b/test/self_proof_check.expected.out
new file mode 100644
index 0000000..ba526f4
--- /dev/null
+++ b/test/self_proof_check.expected.out
@@ -0,0 +1,25 @@
+{"messages":
+ [{"severity": "error",
+   "pos": {"line": 1, "column": 8},
+   "endPos": {"line": 1, "column": 10},
+   "data":
+   "fail to show termination for\n  ex\nwith errors\nfailed to infer structural recursion:\nno parameters suitable for structural recursion\n\nwell-founded recursion cannot be used, 'ex' does not take any (non-fixed) arguments"}],
+ "env": 0}
+
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 1, "column": 22},
+   "goal": "⊢ False",
+   "endPos": {"line": 1, "column": 27}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 8},
+   "endPos": {"line": 1, "column": 10},
+   "data": "declaration uses 'sorry'"}],
+ "env": 1}
+
+{"proofStatus":
+ "Error: kernel type check failed: (kernel) declaration has free variables '[anonymous]'",
+ "proofState": 1,
+ "goals": []}
+
diff --git a/test/self_proof_check.in b/test/self_proof_check.in
new file mode 100644
index 0000000..aa1dac4
--- /dev/null
+++ b/test/self_proof_check.in
@@ -0,0 +1,5 @@
+{"cmd": "theorem ex : False := by exact ex"}
+
+{"cmd": "theorem ex : False := sorry"}
+
+{"proofState": 0, "tactic": "exact ex"}
diff --git a/test/self_proof_exact_check.expected.out b/test/self_proof_exact_check.expected.out
new file mode 100644
index 0000000..aaa3965
--- /dev/null
+++ b/test/self_proof_exact_check.expected.out
@@ -0,0 +1,29 @@
+{"messages":
+ [{"severity": "error",
+   "pos": {"line": 1, "column": 25},
+   "endPos": {"line": 1, "column": 31},
+   "data":
+   "`exact?` could not close the goal. Try `apply?` to see partial suggestions."}],
+ "env": 0}
+
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 1, "column": 22},
+   "goal": "⊢ False",
+   "endPos": {"line": 1, "column": 27}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 8},
+   "endPos": {"line": 1, "column": 10},
+   "data": "declaration uses 'sorry'"}],
+ "env": 1}
+
+{"proofStatus": "Incomplete: contains sorry",
+ "proofState": 1,
+ "messages":
+ [{"severity": "info",
+   "pos": {"line": 0, "column": 0},
+   "endPos": {"line": 0, "column": 0},
+   "data": "`exact?` could not close the goal. Try `apply?` to see partial suggestions."}],
+ "goals": []}
+
diff --git a/test/self_proof_exact_check.in b/test/self_proof_exact_check.in
new file mode 100644
index 0000000..3a76200
--- /dev/null
+++ b/test/self_proof_exact_check.in
@@ -0,0 +1,6 @@
+{"cmd": "theorem ex : False := by exact?"}
+
+{"cmd": "theorem ex : False := sorry"}
+
+{"proofState": 0, "tactic": "exact?"}
+
diff --git a/test/sorry_hypotheses.expected.out b/test/sorry_hypotheses.expected.out
index 6d876fa..d59e9b1 100644
--- a/test/sorry_hypotheses.expected.out
+++ b/test/sorry_hypotheses.expected.out
@@ -11,6 +11,7 @@
  "env": 0}
 
 {"sorries": [{"proofState": 1, "goal": "x : Int\n⊢ x = 1"}],
+ "proofStatus": "Incomplete: open goals remain",
  "proofState": 2,
  "goals": ["x : Int\nh : x = 1\n⊢ x = x"]}
 
diff --git a/test/tactic_mode_sorry.expected.out b/test/tactic_mode_sorry.expected.out
index d0135f4..15c007e 100644
--- a/test/tactic_mode_sorry.expected.out
+++ b/test/tactic_mode_sorry.expected.out
@@ -10,5 +10,8 @@
    "data": "declaration uses 'sorry'"}],
  "env": 0}
 
-{"sorries": [{"proofState": 1, "goal": "⊢ Nat"}], "proofState": 2, "goals": []}
+{"sorries": [{"proofState": 1, "goal": "⊢ Nat"}],
+ "proofStatus": "Incomplete: contains sorry",
+ "proofState": 2,
+ "goals": []}
 
diff --git a/test/trace_simp.expected.out b/test/trace_simp.expected.out
index 2a85844..2c08c46 100644
--- a/test/trace_simp.expected.out
+++ b/test/trace_simp.expected.out
@@ -24,11 +24,15 @@
    "data": "declaration uses 'sorry'"}],
  "env": 4}
 
-{"traces": ["37"], "proofState": 1, "goals": ["⊢ f = 37"]}
+{"traces": ["37"],
+ "proofStatus": "Incomplete: open goals remain",
+ "proofState": 1,
+ "goals": ["⊢ f = 37"]}
 
 {"traces":
  ["[Meta.Tactic.simp.rewrite] f_def:1000, f ==> 37",
   "[Meta.Tactic.simp.rewrite] eq_self:1000, 37 = 37 ==> True"],
+ "proofStatus": "Completed",
  "proofState": 2,
  "goals": []}