From 23ec463520df1e0673071cd73e5c1cb4d04f9fd7 Mon Sep 17 00:00:00 2001
From: rohan <rohanganapa@gmail.com>
Date: Mon, 2 Mar 2026 16:50:42 -0800
Subject: [PATCH] fix: validate proof state before accepting level completion

The server sets `completed` based on absence of diagnostics, not goal
state. During fast typing, diagnostics are transiently empty while the
server is still processing, causing false completion. Validate that the
last proof step has actual tactic info (column != null) and that the
initial step has goals before accepting completion client-side.

Fixes #453
---
 client/src/components/infoview/goals.tsx  | 30 +++++++++++++++++++++--
 client/src/components/infoview/rpc_api.ts |  4 +++
 2 files changed, 32 insertions(+), 2 deletions(-)

diff --git a/client/src/components/infoview/goals.tsx b/client/src/components/infoview/goals.tsx
index 5660826f..3fa3c14b 100644
--- a/client/src/components/infoview/goals.tsx
+++ b/client/src/components/infoview/goals.tsx
@@ -355,6 +355,27 @@ export const FilteredGoals = React.memo(({ headerChildren, goals }: FilteredGoal
     </div>
 })
 
+/**
+ * Check whether the proof goals actually demonstrate completion.
+ *
+ * The server sets `column` to a number when it found and processed tactic info
+ * at a position (`goalsAt?` returned results), and to null when it didn't
+ * (e.g. the tactic hasn't been elaborated yet during transient editing states).
+ * Zero goals with `column == null` means "no data" not "all goals solved".
+ */
+function isProofGoalsComplete(proof: ProofState): boolean {
+  if (proof.steps.length < 2) return false
+  if (proof.steps[0].goals.length === 0) return false
+  const lastIdx = lastStepHasErrors(proof)
+    ? proof.steps.length - 2
+    : proof.steps.length - 1
+  if (lastIdx < 1) return false
+  const lastStep = proof.steps[lastIdx]
+  // Zero goals AND column is set → tactic was processed and produced no goals (genuine completion)
+  // Zero goals AND column is null → no tactic info found (transient state, not completion)
+  return lastStep.goals.length === 0 && lastStep.column != null
+}
+
 export function loadGoals(
   rpcSess: RpcSessionAtPos,
   uri: string,
@@ -372,8 +393,13 @@ rpcSess.call('Game.getProofState',
 ).then(
   (proof : ProofState) => {
     if (typeof proof !== 'undefined') {
-      console.info(`received a proof state!`)
-      console.log(proof)
+      // The server determines `completed` from absence of diagnostics, but during
+      // fast editing diagnostics can be transiently empty (server still processing)
+      // or RPC responses can arrive out of order. Cross-validate against the actual
+      // goal state: a proof is only complete if the goals show it.
+      if ((proof.completed || proof.completedWithWarnings) && !isProofGoalsComplete(proof)) {
+        proof = { ...proof, completed: false, completedWithWarnings: false }
+      }
       setProof(proof)
       setCrashed(false)
     } else {
diff --git a/client/src/components/infoview/rpc_api.ts b/client/src/components/infoview/rpc_api.ts
index 3a6acbaa..e8aa3529 100644
--- a/client/src/components/infoview/rpc_api.ts
+++ b/client/src/components/infoview/rpc_api.ts
@@ -62,6 +62,10 @@ export interface InteractiveGoalsWithHints {
   goals: InteractiveGoalWithHints[];
   command: string;
   diags: InteractiveDiagnostic[];
+  line?: number;
+  /** Set to a number when the server found tactic info at this position.
+   *  null/undefined when no tactic info exists (e.g. during transient processing). */
+  column?: number;
 }
 
 /**