Add proofStatus field in ProofStepResponse + update tests

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. -/

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 []

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. -/

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},

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"]}

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},

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": []}
 

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",

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"]}
 

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"]}
 

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": []}
 

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"]}
 

test/import_lean.expected.out

@@ -0,0 +1,2 @@
+{"env": 0}
+

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": []}
 

test/name_generator.expected.out

@@ -11,39 +11,49 @@
  "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},
    "endPos": {"line": 0, "column": 0},
    "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},