List the Verso documentation sites this server is configured to serve.

Each site has an alias — pass it as the site argument to search, list_kinds, or fetch_page to target that site. Sites are configured via the VERSO_MCP_SITES environment variable. Read-only.

Args: response_format: "markdown" (default) or "json".

Returns: markdown: one line per site (alias, default marker, root URL). json: {"default": str, "sites": [{"alias","root","indexed"}, ...]}

List the kinds of entries indexed for a Verso site, with counts.

Kinds are derived from the site's cross-reference index — they vary per site (a language reference has tactics and options; a textbook has sections and terms). Use the returned kind values to filter search. Read-only.

Args: site: which configured site (alias from list_sites); omit for the default. response_format: "markdown" (default) or "json".

Returns: markdown: a table of kind, count, and human-readable description. json: {"site": str, "root": str, "total_entries": int, "kinds": [{"kind","count","description"}, ...]}

Search a Verso documentation site's cross-reference index by name.

Matches entry names and display names (not free text inside pages — use fetch_page to read a page). Results are ranked by match quality and paginated. Read-only.

Args: query: free-text query matched against canonical and user-facing names. site: which configured site (alias from list_sites); omit for the default. kind: optional kind filter — one of the values from list_kinds. limit: maximum results per page, 1-100 (default 20). offset: number of results to skip, for pagination (default 0). response_format: "markdown" (default) or "json".

Returns: markdown: a header ("N matches … showing X-Y") then one bullet per hit ("- [kind] display — url"), plus a hint to re-call with a higher offset. json: {"site","query","kind","total","count","offset","has_more", "next_offset","results":[{"kind","name","display","url",...}]}

Examples: - "Find the simp tactic" -> search(query="simp", kind="tactic") - "Search the FPiL book for monads" -> search(query="monad", site="fpil") - "Next page of results" -> search(query=..., offset=20)

Fetch a page from a Verso documentation site and return it as Markdown.

Converts the site's HTML to Markdown. With an #anchor, only that single entry/section is returned (not the whole chapter). A relative path is resolved against site; an absolute URL is accepted only if it falls under a configured site root. Plain http://, off-site URLs, and path-traversal segments are rejected. Read-only.

Args: url_or_path: absolute URL on a configured site, or a site-relative path. May include an "#anchor" (e.g. ".../Tactic-Reference/#induction"). site: site to resolve a relative path against (alias from list_sites); omit for the default. Ignored when url_or_path is absolute. response_format: "markdown" (default) for the page text, or "json" for text plus metadata.

Returns: markdown: a "" header line, then the page/section as Markdown (capped at ~200 KB with a truncation marker). json: {"site","url","anchor","content","truncated"} On failure: an error string, or {"error": "..."} when response_format="json".

Examples: - Read one entry -> fetch_page(url_or_path=".../Tactic-Reference/#induction") - Read a chapter -> fetch_page(url_or_path="/Tactic-Proofs/Tactic-Reference/") - Resolve a hit -> pass the url field of a search result here.