Skip to main content

skill-cslib-research

Research CSLib formalization patterns and Mathlib API for CSLib contributions. Invoke for cslib research tasks.

Zur Installation springen

Quellinformationen

Repository
benbrastmckie/nvim
Letzte Quellaktivität
12. August 2026 um 02:10
Erkannte Sprache von SKILL.md
Englisch
Sterne
443
Forks
459

Installationsoptionen

Standardmäßig ist der Prompt ausgewählt, der zuerst die Quelle prüft. Sie können zu einem direkten Befehl wechseln oder eine lokale Kopie herunterladen.

Quelldateien prüfen

Lesen Sie SKILL.md und alle von SkillsMP angezeigten Begleitdateien, bevor Sie sich für eine Installation entscheiden.

SKILL.md wird angezeigt

SKILL.md
Quellanweisungen · Schreibgeschützte Vorschau
name
skill-cslib-research
description
Research CSLib formalization patterns and Mathlib API for CSLib contributions. Invoke for cslib research tasks.
allowed-tools
Agent, Bash, Edit, Read, Write
# CSLib Research Skill Thin wrapper that delegates CSLib research to `cslib-research-agent` subagent. ## Trigger Conditions This skill activates when: - Task type is "cslib" - Research is needed for CSLib formalization, Lean 4 proof patterns, or Mathlib API - CSLib contribution standards or module patterns need to be gathered ## Execution Flow ### Stage 1: Input Validation Validate task_number exists and task_type is "cslib". ### Stage 2: Preflight Status Update Update status to "researching" BEFORE invoking subagent. ### Stage 3: Prepare Delegation Context Domain-specific context for the cslib-research-agent: - lean-lsp MCP tools for Mathlib search (lean_leansearch, lean_loogle, lean_local_search) - CSLib context files from `.claude/extensions/cslib/context/` - Local CSLib Lean files for pattern analysis ```json { "session_id": "sess_{timestamp}_{random}", "delegation_depth": 1, "delegation_path": ["orchestrator", "research", "skill-cslib-research"], "timeout": 3600, "task_context": { "task_number": N, "task_name": "{project_name}", "description": "{description}", "task_type": "cslib" }, "focus_prompt": "{optional focus}", "metadata_file_path": "specs/{NNN}_{SLUG}/.return-meta.json" } ``` ### Stage 4a: Memory and Literature Retrieval (Auto) Retrieve relevant memories and literature briefing to inject into the delegation context. **Skip memory if**: `clean_flag` is true (from `--clean` command flag). ```bash # Check clean_flag if [ "$clean_flag" != "true" ]; then memory_context=$(bash .claude/scripts/memory-retrieve.sh "$description" "$task_type" "$focus_prompt" 2>/dev/null) || memory_context="" fi # memory_context will be empty string if: # - clean_flag is true (skipped) # - memory-index.json missing or empty # - no keywords matched any entries # - script exited with error ``` ```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: Invoke Subagent Use Agent tool with subagent_type: "cslib-research-agent". Include `memory_context` and `lit_context` in the prompt if non-empty: - If `memory_context` is non-empty, include it as a `<memory-context>` block after the delegation context. - If `lit_context` is non-empty, include it as a `<literature-briefing>` block after the memory context. ### Stage 4b: Self-Execution Fallback **CRITICAL**: If you performed the work above WITHOUT using the Agent tool (i.e., you read files, wrote artifacts, or updated metadata directly instead of spawning a subagent), you MUST write a `.return-meta.json` file now before proceeding to postflight. Use the schema from `return-metadata-file.md` with the appropriate status value for this operation. If you DID use the Agent tool, skip this stage -- the subagent already wrote the metadata. ## Postflight (ALWAYS EXECUTE) The following stages MUST execute after work is complete, whether the work was done by a subagent or inline (Stage 4b). Do NOT skip these stages for any reason. ### Stage 5: Parse Subagent Return Read the metadata file from `specs/{N}_{SLUG}/.return-meta.json`. **Expected `status` vocabulary**: `researched` on success; otherwise `partial`, `failed`, or `blocked`. This is a closed set (`@.claude/context/formats/return-metadata-file.md` is normative) and near-synonyms are not accepted — see the `status` note in `cslib-research-agent.md`'s Stage 7 for the three consumers a variant breaks and the stranded-task failure mode it produces. If the value read here is outside the set, do NOT proceed to Stage 6 as if it were a success: report it and stop, so the task is not promoted on an unrecognized outcome. **No `.orchestrator-handoff.json`**: research agents never write one, in any mode, including under `orchestrator_mode: true` (`cslib-research-agent.md` Stage 7 states this as a prohibition). A dispatching orchestrator MUST NOT instruct this skill's subagent to write one either — `.return-meta.json` is the sole status channel for research, and `skill-orchestrate`'s Stage 5 already treats an absent handoff from a research dispatch as the expected outcome and recovers through `scripts/orchestrate-recover-outcome.sh`. **Defensive case, if this prohibition is ever reversed**: should a future variant of this skill's subagent write `.orchestrator-handoff.json`, it MUST echo `dispatch_seq` unchanged from its own delegation context — copy the value verbatim (never invent, increment, or recompute one), or omit it when the delegation context omits it. See `context/patterns/dispatch-report-not-termination.md`. ### Stage 6: Update Task Status (Postflight) Update state.json and TODO.md based on result. ### Stage 7: Link Artifacts Add research artifact to state.json. Update TODO.md per `@.claude/context/patterns/artifact-linking-todo.md` with `field_name=**Research**`, `next_field=**Plan**`. ### Stage 8: Git Commit Commit changes with session ID. ### Stage 9: Return Brief Summary ## Return Format Brief text summary (NOT JSON).
Auf GitHub ansehen