cleanup-all

/cleanup-all — Project-Wide Cleanup (Orchestrator Mode)

Run the full /cleanup workflow over every .lean file in the project, sustained across hours or days, without exhausting the orchestrator's context.

The trick: the main session is an orchestrator, not an implementer. The orchestrator dispatches batched Agent calls, each with a tight prompt and a concrete target, then narrates progress in one-line scoreboards between dispatches. The file reading, the LSP calls, the edits, and the per-declaration golf all happen in subagent contexts — each starts fresh, does its batch, returns a summary. The orchestrator never holds the work in its own context.

This pattern was observed in a real production session that ran for 28 days across 23 active days, dispatched 395 Agent calls, spawned 790 subagent contexts (workers spawning sub-workers), and survived 3 auto-compactions without losing the through-line. The mechanism is the orchestrator/worker split, not heroic context management.

Usage

/cleanup-all [directory]

If no argument, processes all .lean files under the project root (excluding .lake/, build/, .git/).

---

The orchestrator's role (binding)

You are the orchestrator. Your job is to dispatch and track. You do NOT:

• Read project .lean files — workers do that, they need the fresh context for it
• Run lean_diagnostic_messages, lean_goal, lean_multi_attempt, or any lean_* LSP query
• Use Edit or Write on project files
• Run lake build yourself (workers do that as the first check of every batch)
• Spot-check the worker's diff or rerun their LSP queries

You DO:

• Enumerate files (one find call, once)
• Bucket files by size for batched dispatch
• Dispatch Agent calls following the verbatim prompt template below
• Maintain a one-line scoreboard between dispatches
• Collect per-batch summaries from the workers' reports
• Dispatch one final verification Agent at the end
• Print the consolidated report at the very end