Loading ToolBench
An MCP server that exposes Rocq/Coq proof-assistant sessions to AI agents (Claude Code, Codex, etc.). Built on top of Coqtail's XML-protocol client.
Server exposes 7 tools for Rocq/Coq proof assistant interaction. Tool naming follows verb_noun convention (rocq_start, rocq_close, rocq_step_to, rocq_goals, rocq_query, rocq_status, rocq_list), good. Descriptions are present and moderately detailed (rocq_start ~350 chars, rocq_close ~150 chars). However, rocq_step_to and rocq_query descriptions are truncated/incomplete in source. Input schemas are well-structured with types and descriptions for most parameters (rocq_start has 11 params with types and descriptions). Output schemas are NOT documented, critical gap. Error handling returns structured {ok, error} envelopes but lacks recovery guidance. No tool annotations (readOnlyHint, destructiveHint) despite clear risk levels (READ_ONLY, WRITE, DESTRUCTIVE). Parameter descriptions are generally good but some lack format/constraint details (e.g., session_id format, line/col ranges for rocq_step_to).
Close a session. The underlying coqidetop subprocess is terminated and its state is dropped. Safe to call on an unknown id (returns `ok: false` with an `error` reason).
Return the current goal and hypothesis context
List active sessions
Run a non-state-changing query (Check, Print, …)
Start a new Rocq session. Provide either `file_path` (loads the file) or `content` (use inline text). Either way, nothing is sent to Rocq yet — use `rocq_step_to` to execute sentences. `coq_path` is the directory containing the Rocq binaries. Leave `coq_prog` blank so the server auto-selects `coqidetop` on Rocq ≥ 8.9 (plain `coqtop` no longer speaks the IDE protocol on those versions and will hang). Project settings are auto-detected for `file_path` sessions. By default, `build_system='prefer-coqproject'` uses project files when found, otherwise it falls back to Dune. Project file search first checks `.` and `./theories`, then searches upward for `_CoqProject` and `_RocqProject`. `extra_args` are appended last and passed through to the Rocq process. `init_timeout` caps the initial handshake in seconds (default 60); pass 0 or a large number to disable it.
Output schemas undocumented for 5 of 7 tools (rocq_step_to, rocq_goals, rocq_query, rocq_status, rocq_list). LLMs cannot plan downstream calls or extract required fields without knowing return structure.
Descriptions for rocq_step_to, rocq_goals, rocq_query, rocq_status, rocq_list are truncated or minimal (<50 chars). Insufficient context for LLM tool selection. rocq_step_to description cuts off mid-sentence ('Advance or rewind the session so its state matches a position in').
No tool annotations (readOnlyHint, destructiveHint, idempotentHint) despite clear risk levels declared (READ_ONLY, WRITE, DESTRUCTIVE). Agents cannot infer safety/idempotency without explicit hints.
Inferred effective spec: <=2025-11-25.
| Scored | Grade | Overall | Spec posture | Rubric |
|---|---|---|---|---|
| 2026-09-23 | F | 42 | <=2025-11-25 | v2 |
Report whether one session is started
Advance or rewind the session so its state matches a position in
Error handling returns {ok: false, error: string} but lacks recovery guidance. Example: 'Session not found' does not suggest calling rocq_list() or rocq_start(). Errors should guide next steps.
Parameter descriptions lack format/constraint details. session_id format undefined (UUID? string?). rocq_step_to line/col ranges not specified (1-indexed per docstring, but not in param descriptions). max_chars constraint mentioned in code but not in schema.