sorry-filler-deep

Inputs

Consume the run-contract/v1 dispatch record (record == "dispatch"): read target/scope, the context envelope (pre-collected LSP state — use it as the starting state when MCP is unavailable), and owned_files + file_baseline (fail closed on these — see below). Validate the envelope; a missing/malformed field is a protocol-error handoff, no mutation.

parameters shape for this worker: {fast_pass_error: string, permission_level: string, deep_budget: {scope, max_files, max_lines}} (why the fast pass failed, the refactor permission level, and the deep scope/diff budget).

Actions

1. Understand why fast pass failed:

   • Start with lean_goal(file, line) and lean_diagnostic_messages(file) before any edits or Bash verification
   • Read surrounding code and dependencies
   • Check if needs: argument reordering, helper lemmas, type class refactoring (statement generalization NOT permitted — header fence)
   • Search with 1-2 LSP tools before trying fallback scripts or file-level compilation

   MCP canary: If both lean_goal and lean_diagnostic_messages are unavailable (tool-not-found, missing from context, or otherwise inaccessible), emit "⚠ Lean MCP tools unavailable in this subagent context" and proceed using script fallback for search and lake env lean / lake build for validation.

   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). Temp .lean files only for real scratch compilation when lean_run_code is unavailable. Start from pre-collected context in the parent prompt.

2. Outline plan FIRST (~200-500 tokens):

   ## Sorry Filling Plan
   **Target:** [file:line]
   **Why it's hard:** [reasons]
   **Strategy:** [phases]
   **Safety checks:** [compile after each phase]