Initial fix (incomplete)

REPL/Main.lean

@@ -125,11 +125,56 @@ def tactics (trees : List InfoTree) : M m (List Tactic) :=
       let proofStateId ← proofState.mapM recordProofSnapshot
       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
+    }
+
 /-- 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 messages ← messages.mapM fun m => Message.of m
+  let mut messages ← messages.mapM fun m => Message.of m
   let traces ← proofState.newTraces old?
   let trees := proofState.newInfoTrees old?
   let trees ← match old? with
@@ -142,6 +187,9 @@ def createProofStepReponse (proofState : ProofSnapshot) (old? : Option ProofSnap
   -- trees.forM fun t => do IO.println (← t.format)
   let sorries ← sorries trees none
   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}"

REPL/Snapshots.lean

@@ -108,6 +108,7 @@ structure ProofSnapshot where
   termContext   : Term.Context
   tacticState   : Tactic.State
   tacticContext : Tactic.Context
+  initialGoals  : List MVarId
 
 namespace ProofSnapshot
 
@@ -206,7 +207,8 @@ def create (ctx : ContextInfo) (lctx? : Option LocalContext) (env? : Option Envi
       termState := {}
       termContext := {}
       tacticState := { goals }
-      tacticContext := { elaborator := .anonymous } }
+      tacticContext := { elaborator := .anonymous }
+      initialGoals := goals }
 
 open Lean.Core in
 /-- A copy of `Core.State` with the `Environment`, caches, and logging omitted. -/
@@ -270,18 +272,19 @@ def pickle (p : ProofSnapshot) (path : FilePath) : IO Unit := do
      p'.termState,
      ({ p'.termContext with } : CompactableTermContext),
      p'.tacticState,
-     p'.tacticContext)
+     p'.tacticContext,
+     p'.initialGoals)
 
 /--
 Unpickle a `ProofSnapshot`.
 -/
 def unpickle (path : FilePath) (cmd? : Option CommandSnapshot) :
     IO (ProofSnapshot × CompactedRegion) := unsafe do
   let ((imports, map₂, coreState, coreContext, metaState, metaContext, termState, termContext,
-    tacticState, tacticContext), region) ←
+    tacticState, tacticContext, initialGoals), region) ←
     _root_.unpickle (Array Import × PHashMap Name ConstantInfo × CompactableCoreState ×
       Core.Context × Meta.State × CompactableMetaContext × Term.State × CompactableTermContext ×
-      Tactic.State × Tactic.Context) path
+      Tactic.State × Tactic.Context × List MVarId) path
   let env ← match cmd? with
   | none =>
     enableInitializersExecution
@@ -296,7 +299,8 @@ def unpickle (path : FilePath) (cmd? : Option CommandSnapshot) :
     termState
     termContext := { termContext with }
     tacticState
-    tacticContext }
+    tacticContext
+    initialGoals }
   let (_, p'') ← p'.runCoreM do
     for o in ← getOpenDecls do
       if let .simple ns _ := o then

test/by_cases.expected.out

@@ -21,5 +21,10 @@
  [{"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"}],
  "proofState": 5,
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 0, "column": 0},
+   "endPos": null,
+   "data": "Proof contains sorry"}],
  "goals": []}
 

test/invalid_tactic.expected.out

@@ -15,6 +15,10 @@
  [{"severity": "error",
    "pos": {"line": 0, "column": 0},
    "endPos": {"line": 0, "column": 0},
-   "data": "unknown identifier 'my_fake_premise'"}],
+   "data": "unknown identifier 'my_fake_premise'"},
+  {"severity": "warning",
+   "pos": {"line": 0, "column": 0},
+   "endPos": null,
+   "data": "Proof contains sorry"}],
  "goals": []}