Add Claude Code skill and AI Agents docs section#3
Conversation
There was a problem hiding this comment.
Pull request overview
Adds agent-facing documentation and a Claude Code skill for calling the PhyslibSearch API, and exposes this in the /docs page.
Changes:
- Add an AI Agents section to the docs page, including install/invocation instructions for a Claude Code skill.
- Add a new
.claude/skills/physlibsearch/SKILL.mdfile documenting PhyslibSearch endpoints, usage tips, and rate limits.
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated 5 comments.
| File | Description |
|---|---|
| frontend/src/app/docs/page.tsx | Adds “AI Agents” section and TOC entry with install instructions and links. |
| .claude/skills/physlibsearch/SKILL.md | Introduces a Claude Code skill document describing how agents should use the PhyslibSearch API. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| Claude Code | ||
| </a>{" "} | ||
| skill that teaches any Claude agent how to call the API. Once installed, the agent can | ||
| search Physlib, fetch declarations by name, and expand queries with HyDE — without any |
There was a problem hiding this comment.
In this new section the library name is written as “Physlib” (e.g., “search Physlib…”), but the rest of the docs consistently use “PhysLib” (see earlier on this page). For consistency and to avoid confusion, update the capitalization here (and anywhere else in this section) to match the project’s standard branding.
| search Physlib, fetch declarations by name, and expand queries with HyDE — without any | |
| search PhysLib, fetch declarations by name, and expand queries with HyDE — without any |
| <p className="text-foreground/50">Install the skill (one-time, any project):</p> | ||
| <CodeBlock | ||
| lang="bash" | ||
| code={`mkdir -p ~/.claude/skills/physlibsearch && curl -fsSo ~/.claude/skills/physlibsearch/SKILL.md \\ | ||
| https://raw.githubusercontent.com/Kernel-Science/physlibsearch-skill/main/SKILL.md`} | ||
| /> |
There was a problem hiding this comment.
The install command pulls SKILL.md from the separate physlibsearch-skill repo, but this PR also adds the skill file into this repo under .claude/skills/physlibsearch/SKILL.md. Having two sources of truth risks drift; consider either (a) referencing the in-repo file in the install instructions, or (b) removing the in-repo copy and treating the external repo as canonical. If you keep the curl-based install, pinning to a tag/commit (instead of main) would also make installs reproducible and reduce supply-chain risk.
| name: physlibsearch | ||
| description: Semantic search over Physlib, a formal Lean 4 library of physics theorems and definitions. Use when asked to find Lean 4 declarations related to physics or mathematics, look up formal proofs, retrieve theorem signatures, or browse the Physlib module hierarchy. | ||
| --- |
There was a problem hiding this comment.
The project consistently refers to the upstream library as “PhysLib” (e.g., README and frontend docs), but this skill’s description uses “Physlib”. Please align capitalization/branding throughout this skill to “PhysLib” for consistency.
| **Request** | ||
| ```json | ||
| { | ||
| "query": [ | ||
| ["Physlib", "Mechanics", "Newton", "secondLaw"], | ||
| ["Physlib", "QuantumMechanics", "HarmonicOscillator", "energy"] | ||
| ] | ||
| } |
There was a problem hiding this comment.
The /fetch endpoint in this repo’s FastAPI server accepts a raw JSON array of Lean names as the request body (see server.py where the handler parameter is query: list[LeanName] and it’s the only body param). This skill currently documents /fetch as an object with a query field, which won’t match the actual API shape (and also differs from the existing frontend docs). Please update the request format here (or change the API to accept the wrapped object consistently).
|
|
||
| ### 4. List Modules — `GET /modules` | ||
|
|
||
| Returns all top-level Physlib modules with a count of searchable declarations. |
There was a problem hiding this comment.
GET /modules is described here as returning “all top-level Physlib modules”, but the server groups by declaration.module_name, so it can return any indexed module path (not only top-level). Consider rewording to “all indexed modules” to match actual behavior and the OpenAPI description.
| Returns all top-level Physlib modules with a count of searchable declarations. | |
| Returns all indexed Physlib modules with a count of searchable declarations. |
Summary
.claude/skills/physlibsearch/SKILL.md— a Claude Code skill that teaches any agent how to call the PhyslibSearch API (all endpoints, query tips, rate limits, result interpretation)/docswith a one-liner install command pointing to the standalone skill repo