Skip to main content

skill-cslib-implementation-hard

Implement CSLib proofs with hard-mode contracts (H2 anti-analysis, H7 territory, H9 wrap-up with sorry_inventory). Invoke for --hard cslib implementation tasks.

설치로 이동

소스 정보

저장소
benbrastmckie/nvim
최근 소스 활동
2026년 9월 2일 17:04
감지된 SKILL.md 언어
영어
스타
443
포크
459

설치 방법

기본적으로 소스를 먼저 확인하는 Prompt가 선택됩니다. 직접 명령으로 전환하거나 로컬 사본을 다운로드할 수도 있습니다.

소스 파일 검토

설치 여부를 결정하기 전에 SKILL.md와 SkillsMP에 표시된 보조 파일을 읽어 보세요.

SKILL.md 표시 중

SKILL.md
소스 지침 · 읽기 전용 미리보기
name
skill-cslib-implementation-hard
description
Implement CSLib proofs with hard-mode contracts (H2 anti-analysis, H7 territory, H9 wrap-up with sorry_inventory). Invoke for --hard cslib implementation tasks.
allowed-tools
Agent, Bash, Edit, Read, Write
# CSLib Implementation Hard Skill Hard-mode wrapper that delegates CSLib proof implementation to `cslib-implementation-hard-agent` subagent. Extends `skill-cslib-implementation` with: - Single-phase dispatch context (H1): reads handoff JSON to identify next incomplete phase - Territory parameters (H7): includes territory contract when dispatched from orchestrate-hard - Anti-analysis contract (H2): passed in delegation context for agent enforcement - Wrap-up discipline (H9): sorry_inventory populated in orchestrator handoff **Relationship to base skill**: Structurally follows `skill-cslib-implementation` postflight pattern. Key difference: when `orchestrator_mode=true`, uses per-phase dispatch (H1) rather than whole-plan dispatch. **Maintenance note**: changes to `skill-cslib-implementation` postflight should be mirrored here. ## Context References Reference (do not load eagerly): - Path: `.claude/context/formats/return-metadata-file.md` - Metadata file schema - Path: `.claude/context/contracts/anti-analysis.md` - H2 contract (loaded by agent) - Path: `.claude/context/contracts/wrap-up.md` - H9 contract (loaded by agent) - Path: `.claude/context/contracts/territory.md` - H7 contract (when territory params present) - Path: `.claude/context/contracts/phase-closure.md` - depth-first phase closure: close one phase before opening the next (loaded by agent) - Path: `.claude/context/contracts/pre-edit-gate.md` - per-item evidence before applying a mechanical-list edit (loaded by agent) - Path: `.claude/context/patterns/postflight-control.md` - Marker file protocol - Path: `.claude/context/patterns/subagent-continuation-loop.md` - Continuation loop pattern ## Trigger Conditions This skill activates when: - `/implement N --hard` is invoked and task type is `cslib` - Routed here by `command-route-skill.sh` with `effort_flag="hard"` and task type `cslib` - Explicitly listed in `routing_hard.implement.cslib` in the cslib extension manifest - Note: `skill-orchestrate`'s own hard-mode dispatch (both effort modes, one engine — the formerly-separate hard-mode engine is deleted) resolves and dispatches the AGENT (`cslib-implementation-hard-agent`) directly via `command-route-agent.sh`, not this SKILL file; this skill's own activation is via the paths above. --- ## Execution Flow ### Stage 1: Input Validation ```bash task_data=$(jq -r --argjson num "$task_number" \ '.active_projects[] | select(.project_number == $num)' \ specs/state.json) if [ -z "$task_data" ]; then return error "Task $task_number not found" fi task_type=$(echo "$task_data" | jq -r '.task_type // "general"') status=$(echo "$task_data" | jq -r '.status') project_name=$(echo "$task_data" | jq -r '.project_name') description=$(echo "$task_data" | jq -r '.description // ""') if [ "$status" = "completed" ] || [ "$status" = "abandoned" ] || [ "$status" = "expanded" ]; then return error "Task is in terminal state [$status]" fi ``` --- ### Stage 1.5: Hard-Mode Cost Note ```bash session_flag_file="/tmp/.hard-mode-notified-${SESSION_ID:-$$}" if [ ! -f "$session_flag_file" ]; then echo "[hard-mode] Hard mode active (cslib implementation). Cost: ~3-5x standard." >&2 touch "$session_flag_file" fi ``` --- ### Stage 2: Preflight Status Update Source `skill-base.sh` once, then follow `@.claude/context/patterns/skill-preflight-flow.md`'s Stage 2 (preflight status update): ```bash source .claude/scripts/skill-base.sh padded_num=$(printf "%03d" "$task_number") skill_name="skill-cslib-implementation-hard" operation="implement" skill_preflight_update "$task_number" "$operation" "$session_id" ``` --- ### Stage 2b: Preflight Cache Warming Ensure Mathlib cache is warm before delegating to the agent: ```bash cd /home/benjamin/Projects/cslib && lake exe cache get 2>&1 || echo "Warning: cache fetch failed (non-fatal)" ``` This is non-blocking. Cache fetch failure does not prevent delegation. On a cache hit, this completes in ~1-2 minutes and prevents 30-45 minute Mathlib rebuilds during CI verification. --- ### Stage 3: Create Postflight Marker Follow `@.claude/context/patterns/skill-preflight-flow.md`'s Stage 3 (marker creation): ```bash skill_create_postflight_marker "$padded_num" "$project_name" "$session_id" "$skill_name" "$operation" ``` --- ### Stage 3a: Calculate Artifact Number ```bash next_num=$(jq -r --argjson num "$task_number" \ '.active_projects[] | select(.project_number == $num) | .next_artifact_number // 1' \ specs/state.json) if [ "$next_num" -le 1 ]; then artifact_number=1 else artifact_number=$((next_num - 1)) fi artifact_padded=$(printf "%02d" "$artifact_number") ``` --- ### Stage 3b: Single-Phase Dispatch Context (H1) When `orchestrator_mode=true`, determine the specific phase to dispatch: ```bash if [ "$orchestrator_mode" = "true" ]; then # Read handoff JSON to find next incomplete phase handoff_file="specs/.orchestrator-handoff.json" if [ -f "$handoff_file" ]; then phases_completed=$(jq -r '.phases_completed // 0' "$handoff_file") next_phase=$((phases_completed + 1)) echo "[hard-mode] Per-phase dispatch: targeting phase ${next_phase} (cslib)" >&2 else next_phase=1 echo "[hard-mode] No handoff found, dispatching cslib phase 1" >&2 fi fi ``` --- ### Stage 4a: Memory Retrieval (Auto) ```bash if [ "$clean_flag" != "true" ]; then memory_context=$(bash .claude/scripts/memory-retrieve.sh "$description" "$task_type" "" 2>/dev/null) || memory_context="" fi ``` ```bash # Literature briefing injection (independent of clean_flag) lit_context="" if [ "$lit_flag" = "true" ]; then lit_context=$(bash .claude/scripts/literature-briefing.sh 2>/dev/null) || lit_context="" fi # lit_context will be empty string if: # - lit_flag is not "true" (skipped) # - specs/literature/ sub-index is empty or missing # - script exited with error ``` **Note**: `lit_flag` is independent of `clean_flag`. Using `--clean --lit` suppresses memory retrieval but still injects literature briefing. Literature briefing is gated solely on `lit_flag == "true"`. --- ### Stage 4: Prepare Delegation Context Pass anti-analysis contract reference and territory params (when applicable): ```json { "session_id": "{session_id}", "delegation_depth": 1, "delegation_path": ["orchestrator", "implement", "skill-cslib-implementation-hard"], "timeout": 7200, "task_context": { "task_number": N, "task_name": "{project_name}", "description": "{description}", "task_type": "cslib" }, "artifact_number": "{artifact_number}", "effort_flag": "hard", "model_flag": "{model_flag from command}", "plan_path": "{plan_path}", "phase_number": "{next_phase when orchestrator_mode=true, null otherwise}", "territory": "{territory params from orchestrate-hard dispatch, null if not provided}", "orchestrator_mode": "{orchestrator_mode}", "metadata_file_path": "specs/{NNN}_{SLUG}/.return-meta.json", "dispatch_seq": "{dispatch_seq from this skill's own delegation context, forwarded unchanged; omit if absent}" } ``` **Forward `dispatch_seq` unchanged.** If this skill's own delegation context carries a `dispatch_seq` field, forward it into the sub-agent's delegation context above verbatim — the same pass-through treatment already given to `territory`. Never invent, increment, or recompute a value at this layer; only the orchestrator mints one. If absent, omit the field. See `context/patterns/dispatch-report-not-termination.md`. > **CRITICAL**: No source reading before delegation. The subagent handles all codebase exploration. --- ### Stage 4b: Read Format Specification ```bash format_content=$(cat .claude/context/formats/summary-format.md) ``` --- ### Stage 5: Invoke Subagent ``` Tool: Agent Parameters: - subagent_type: "cslib-implementation-hard-agent" - prompt: [task_context, delegation_context, format specification, memory_context, lit_context] - description: "Execute hard-mode CSLib implementation for task {N} phase {next_phase}" ``` - If `memory_context` is non-empty, include it as a `<memory-context>` block after the format specification. - If `lit_context` is non-empty, include it as a `<literature-briefing>` block after the memory context. - Do NOT inject empty blocks when content is empty. Include territory parameters in prompt when `territory` is non-null: ``` <territory-contract> This is a hard-mode parallel dispatch. Territory rules are mandatory: - Owned files: {territory.owned_files} - Read-only references: {territory.read_only_files} - See .claude/context/contracts/territory.md for full protocol </territory-contract> ``` --- ### Stage 5b: Self-Execution Fallback If Agent tool not used, write `.return-meta.json` with `status: "implemented"` before postflight. --- ### Stage 5c: Continuation Loop Init ```bash continuation_count=0 max_continuations=3 task_dir="specs/${padded_num}_${project_name}" cat > "${task_dir}/.continuation-loop-guard" << EOF { "session_id": "${session_id}", "continuation_count": 0, "max_continuations": 3 } EOF ``` --- ## Postflight (ALWAYS EXECUTE) ### Stage 6: Parse Subagent Return ```bash metadata_file="specs/${padded_num}_${project_name}/.return-meta.json" if [ -f "$metadata_file" ] && jq empty "$metadata_file" 2>/dev/null; then status=$(jq -r '.status' "$metadata_file") artifact_path=$(jq -r '.artifacts[0].path // ""' "$metadata_file") artifact_type=$(jq -r '.artifacts[0].type // ""' "$metadata_file") artifact_summary=$(jq -r '.artifacts[0].summary // ""' "$metadata_file") memory_candidates=$(jq -c '.memory_candidates // []' "$metadata_file") completion_summary=$(jq -r '.completion_data.completion_summary // ""' "$metadata_file") phases_completed=$(jq -r '.phases_completed // 0' "$metadata_file") phases_total=$(jq -r '.phases_total // 0' "$metadata_file") else status="failed" fi ``` --- ### Stage 7: Update Task Status (Postflight) ```bash if [ "$status" = "implemented" ]; then bash .claude/scripts/update-task-status.sh postflight "$task_number" implement "$session_id" --phase-check=warn fi # On partial: keep status as "implementing" for resume ``` --- ### Stage 7a: Propagate Memory Candidates and Completion Summary Same as `skill-cslib-implementation` Stage 7a + completion summary propagation. --- ### Stage 8: Link Artifacts Two-step jq pattern (Issue #1132 safety): 1. Filter out existing summary artifacts 2. Add new summary artifact Regenerate TODO.md after linking. --- ### Stage 8a: Lifecycle TTS Notification ```bash
GitHub에서 보기
이 SKILL.md는 매우 커서 SkillsMP가 여기에는 첫 섹션만 미리 보여줍니다. GitHub에서 보기