Print proof steps in validation logs in frontend format

- Add validate/format-proof-steps.ts (statementToString + reason names)
- run-validate.mjs uses formatProofStep for proof task output

Made-with: Cursor

Author: hamlet1234

run-validate.mjs

@@ -29,6 +29,7 @@ const DEFAULT_LOG_FILE = resolve(process.cwd(), 'logs', 'user_actions.log');
 
 const replay = require('./validate/replay.js');
 const tasks = require('./validate/tasks.js');
+const { formatProofStep } = require('./validate/format-proof-steps.js');
 
 const PROOF_TASKS = new Set(['prove-opposite-rays', 'prove-perpendicular-bisector']);
 
@@ -96,6 +97,14 @@ async function main() {
     }
   }
 
+  if (proofSteps?.length) {
+    console.log('Proof steps:');
+    proofSteps.forEach((step, i) => {
+      console.log('  ' + formatProofStep(step, i));
+    });
+    console.log('');
+  }
+
   const result = tasks.runTask(taskId, snapshot, { proofSteps, taskStatement });
 
   console.log(result.message);

validate/format-proof-steps.ts

@@ -0,0 +1,93 @@
+/**
+ * Format proof steps for validation logs in the same way the student sees them in the frontend.
+ * Mirrors client/proof/statements.ts statementToString and client/proof/reasons.ts REASONS names.
+ */
+
+import type { ProofStepLogEntry } from './types.js';
+
+/** Human-readable string for a statement (same as client/proof/statements statementToString). */
+function statementToString(s: { kind: string; pointNames: string[]; constant?: number }): string {
+  const n = s.pointNames;
+  switch (s.kind) {
+    case 'points-distinct':
+      return `${n[0]} ≠ ${n[1]}`;
+    case 'point-on-line':
+      return `${n[0]} ∈ line ${n[1]}${n[2]}`;
+    case 'point-on-segment':
+      return `${n[0]} ∈ ${n[1]}${n[2]}`;
+    case 'point-on-ray':
+      return `${n[0]} ∈ ray ${n[1]}${n[2]}`;
+    case 'line-equals-line':
+      return `line ${n[0]}${n[1]} = line ${n[2]}${n[3]}`;
+    case 'rays-form-line':
+      return `ray ${n[0]}${n[1]} ∪ ray ${n[2]}${n[1]} = line ${n[0]}${n[1]}`;
+    case 'unique-line':
+      return `∃₁ line through ${n[0]}, ${n[1]}`;
+    case 'intersection-equals':
+      return `${n[0]} = line ${n[1]}${n[2]} ∩ line ${n[3]}${n[4]}`;
+    case 'intersection-segment-equals':
+      return `${n[1]}${n[0]} ∩ ${n[2]}${n[3]} = ${n[0]}`;
+    case 'angle-equals-constant':
+      return `∠${n[0]}${n[1]}${n[2]} = ${(s as { constant?: number }).constant ?? '·'}°`;
+    case 'angle-equals-angle':
+      return `∠${n[0]}${n[1]}${n[2]} = ∠${n[3]}${n[4]}${n[5]}`;
+    case 'angle-less-than-angle':
+      return `∠${n[0]}${n[1]}${n[2]} < ∠${n[3]}${n[4]}${n[5]}`;
+    case 'angle-greater-than-angle':
+      return `∠${n[0]}${n[1]}${n[2]} > ∠${n[3]}${n[4]}${n[5]}`;
+    case 'angle-leq-angle':
+      return `∠${n[0]}${n[1]}${n[2]} ≤ ∠${n[3]}${n[4]}${n[5]}`;
+    case 'angle-geq-angle':
+      return `∠${n[0]}${n[1]}${n[2]} ≥ ∠${n[3]}${n[4]}${n[5]}`;
+    case 'segment-equals-segment':
+      return `${n[0]}${n[1]} = ${n[2]}${n[3]}`;
+    case 'segment-perpendicular':
+      return `${n[0]}${n[1]} ⊥ ${n[2]}${n[3]}`;
+    case 'triangles-congruent':
+      return `Δ${n[0]}${n[1]}${n[2]} ≅ Δ${n[3]}${n[4]}${n[5]}`;
+    case 'triangle-angles-sum-180':
+      return `angles of Δ${n[0]}${n[1]}${n[2]} sum to 180°`;
+    case 'point-midpoint-of-segment':
+      return `${n[0]} is midpoint of ${n[1]}${n[2]}`;
+    default:
+      return String(s.kind);
+  }
+}
+
+/** Reason id -> display name (same as client/proof/reasons REASONS[].name). */
+const REASON_NAMES: Record<string, string> = {
+  given: 'Given in task statement',
+  definition: 'New Definition',
+  'perpendicular-definition': 'Perpendicular definition',
+  'line-determination': 'Incidence axiom I1 (two points determine a unique line)',
+  'point-on-line-same-line': 'By I1 (point on line: line AC = line AB)',
+  'opposite-rays-form-line': 'Theorem: opposite rays lie on one line',
+  reflexivity: 'Reflexivity (AB = AB or ∠A = ∠A)',
+  'reflexivity-segment': 'Reflexivity (AB = AB or ∠A = ∠A)',
+  'transitivity-equals': 'Transitivity (=)',
+  'transitivity-less': 'Transitivity (<)',
+  'transitivity-greater': 'Transitivity (>)',
+  'transitivity-leq': 'Transitivity (≤)',
+  'transitivity-geq': 'Transitivity (≥)',
+  sas: 'Triangle congruence (SAS)',
+  asa: 'Triangle congruence (ASA)',
+  aas: 'Triangle congruence (AAS)',
+  sss: 'Triangle congruence (SSS)',
+  hl: 'Triangle congruence (HL)',
+  'from-congruence': 'From congruence (CPCTC): corresponding sides equal',
+  'sum-triangle-angles': 'Sum of triangle angles',
+  thales: 'Thales theorem',
+};
+
+/**
+ * Format one proof step as shown in the frontend: "1. statement (Reason name) [from: Given, Step 2]"
+ */
+export function formatProofStep(step: ProofStepLogEntry, index: number): string {
+  const statement = step.outcome ? statementToString(step.outcome) : '?';
+  const reasonName = (step.reasonId && REASON_NAMES[step.reasonId]) || step.reasonId || '?';
+  const refs = Array.isArray(step.prerequisiteRefs) && step.prerequisiteRefs.length;
+  const prereqStr = refs
+    ? ` [from: ${step.prerequisiteRefs.map((r) => (r === 'given' ? 'Given' : `Step ${r}`)).join(', ')}]`
+    : '';
+  return `${index + 1}. ${statement} (${reasonName})${prereqStr}`;
+}