メニュー
Close a wave deterministically — run the gate prerequisites, dispatch the fresh-context adversarial review, and record the close. Use once per wave when the wave's bricks are shipped and validate is green.
Codex または Claude でインストール この Prompt をコピーして Codex、Claude、または他のアシスタントに貼り付けると、Skill ページを確認してインストールできます。
SOC 職業分類に基づく
In-loop development guidance for an autonomous /goal Lean-proof loop in SK_EFT_Hawking. This skill should be used when developing Lean 4 proofs inside a goal loop, deciding whether to fan work out to parallel worktree slots or stay solo, resetting a worktree slot, hitting a recurring Lean tactic/ elaboration friction, or sharding the lab notebook. It surfaces the MCP-first proof loop, kernel-purity rules, the worktree fan-out flow, and a symptom-indexed friction catalog. Invoke it at the start of a development stretch and whenever you hit proof-mechanics friction or need the parallel-dev recipe.
Goal-mode LAUNCH + always-on posture for an autonomous /goal dev loop. On invocation it composes the /goal condition AND registers the session with the harness; its core posture re-attaches after compaction. Use when STARTING a managed /goal dev loop, or writing/refining a goal prompt + acceptance criteria. (For IN-LOOP development guidance — the MCP proof loop, worktree fan-out, friction catalog — use the goal-dev skill instead.)
Off-hot-loop System-2 harvest. Reads each managed /goal session's transcript from a byte-offset watermark, extracts process/harness signal (Haiku) — crossing the compact boundary for the pre-vs-post-compact delta and ingesting the guard's blocked-question log — and a register-AWARE Opus consolidator files/combines it into the four-section register (Open / Process Wins / Closed / Misfiled) — re-opening a recurring closed finding, grouping semi-related ones, filing real wins to Process Wins (capped at agent-reviewed, never injected), and dropping noise (never writing Misfiled — that is /debrief's human sweep) — then refreshes the open-only active-issues view. Invoked by a Desktop scheduled task or a second-session /loop — never inside a /goal session.
Interactively review the System-2 dev-process harvest — promote agent-reviewed findings to human-reviewed (or close them), and triage GAP-A gate proposals. Runs over the register-aware harvest's already-synthesized register (it files/combines/re-opens continuously); debrief is the human governor — only it promotes to human-reviewed. Use when you want to sign off on what the autonomous loop learned about HOW it ran.
Run the full mechanical Stage-12 sync (counts, tables, deps, citation cache) in one command. Use before a wave gate, or whenever counts/tables/figures may have drifted from the Lean/Python sources.
| name | wave-close |
| description | Close a wave deterministically — run the gate prerequisites, dispatch the fresh-context adversarial review, and record the close. Use once per wave when the wave's bricks are shipped and validate is green. |
| argument-hint | <wave-or-bundle-id> |
| allowed-tools | Bash(git rev-parse *), Bash(cd *), Bash(uv run python *), Agent |
Close wave $ARGUMENTS in one deliberate pass. Do NOT do this per-task — once per wave.
Resolve the repo root (cwd-robust — works from the workspace root OR inside the repo) (NOT
${CLAUDE_PROJECT_DIR} — not a skill substitution):
!`R=$(uv run --no-sync python "${CLAUDE_PLUGIN_ROOT}/scripts/harness_common_cli.py" repo-root 2>/dev/null); test -n "$R" || R=$(git rev-parse --show-toplevel 2>/dev/null); echo "${R:-UNRESOLVED}"`. This uses the harness
repo_root() (the SAME resolver the hooks use), falling back to git rev-parse, so it resolves whether CC was
launched from the workspace root (the lean-lsp launch point) or inside the repo. UNRESOLVED only if
launched entirely outside the workspace — then tell the user to cd into SK_EFT_Hawking/ and re-run. Use
<repo-root> for the paths below.
Full sync + gate prereqs (deterministic). Run via Bash (the scripts self-locate their own ROOT;
sync.py's shared-artifact regen is serialized by the Task-7 regen concurrency lock, so a concurrent
worktree/worker can't race the same regen — spec 12):
cd "<repo-root>" && uv run python scripts/sync.py --fullcd "<repo-root>" && uv run python scripts/gate_precheck.py s13
(cd into the resolved repo so uv finds its project — a bare uv run from the workspace root runs an ephemeral interpreter WITHOUT the repo's deps (e.g. src.core fails to import); cd into the repo gives it the project env.) If gate_precheck s13 is FAIL, STOP — fix the red checks first; do not spend an
Opus review on a failing tree.Dispatch the fresh-context review (a real model call, the GAP-B safeguard the
self-audit blind spot requires): invoke the skeft-qa:adversarial-reviewer
(and skeft-qa:claims-reviewer for paper-shaped output) on $ARGUMENTS in a
fresh context. It must run with zero BLOCKER findings surfaced in the
transcript before the wave can be called closed.
Record the close. Write docs/dev-loops/<roadmap>/<wave>_close.md with: the
validate result, the reviewer report path, the BLOCKER count (must be 0), and the
commit range. Never edit CLAUDE.md / hooks / roadmaps here.
State plainly whether the wave is closeable (zero BLOCKERs, green tree) or what
remains. This is the explicit complement to the /goal acceptance-criteria path
(the goal-prompt skill bakes the same zero-BLOCKER requirement into the loop).