proof-repair

Inputs

Consume the run-contract/v1 dispatch record (record == "dispatch"): read target, the context envelope, and parameters.error (the structured error to repair). proof-repair is patch-only — it does not edit, so it takes no owned_files custody. It receives the parent's file_baseline non-custodially (it never checks or advances it) and echoes it back unchanged in its handoff; the parent applies and advances the returned diff.

parameters.error shape:

{
  "errorType": "type_mismatch|unsolved_goals|unknown_ident|synth_instance|timeout",
  "message": "...",
  "file": "Foo.lean",
  "line": 42,
  "goal": "⊢ Continuous f",
  "localContext": ["h1 : Measurable f"]
}

Actions

1. Classify error — lean_goal(file, line) + lean_diagnostic_messages(file) first, then match errorType

   MCP canary: If lean_goal and lean_diagnostic_messages are both unavailable (tool-not-found, missing from context, or otherwise inaccessible), return no diff and let the caller escalate (same mechanism as the header-fence constraint).

   No-MCP hygiene (if canary fails): MCP tools are tool calls, not shell commands — never invoke them via Bash. Do not probe MCP availability via Bash (which, env, ls) — the canary is authoritative. Stop retrying MCP for this run. Use Read/Grep to inspect files (never write scripts or temp files just to view source). Start from pre-collected context in the parent prompt.

2. Apply error-specific strategy (see table below)

3. Search if needed (LSP-first; fall back to scripts only when LSP is unavailable, rate-limited, or inconclusive after bounded attempts):

   • lean_leanfinder("query") or lean_local_search("keyword") first
   • Script fallback: lean4-skills-search-mathlib only after LSP exhausted

4. Generate minimal diff (1-5 lines)

5. Return the diff in a run-contract/v1 handoff — the unified diff in artifacts (kind: unified-diff), no prose in the diff content (see Output)