coqtail-mcp

name

coqtail-mcp

description

Drive a live Rocq/Coq proof session through the coqtail-mcp MCP server — start a session from a .v file, step forward/backward to any line, inspect the current goal and hypothesis context, and run read-only queries (Check, Print, Search). Trigger when the user wants to step through a Rocq proof interactively, inspect proof state at a specific buffer position, run non-advancing queries, or otherwise drive coqidetop from an agent. Do NOT trigger for Lean 4, Agda, Isabelle, HOL4, Mizar, Idris, or other non-Rocq provers.

coqtail-mcp

This skill teaches the agent how to use the coqtail-mcp MCP server, which spawns coqidetop subprocesses and exposes a session-oriented view over Coqtail's XML protocol. Each session is one live Rocq process; you advance or rewind it by specifying buffer positions.

The skill covers two things: (1) driving the server correctly — session lifecycle, position semantics, rewind boundaries, error envelopes — and (2) using it well for actual proof work — the search-first habit, tactic cascade, goal-pattern → tactic table, common-error fixes, axiom hygiene, and patterns for delegating parallel work to subagents.

Tool summary

All tools accept JSON and return JSON. Rejected tool calls never raise — they return {ok: false, error: "brief reason"}. Always check ok before reading success-specific fields.

Tool	Purpose
rocq_start	Spawn a Rocq session. Pass either file_path OR content.
rocq_close	Terminate and forget a session.
rocq_step_to	Advance OR rewind so the state matches (line, col).
rocq_goals	Current focused goal + hypotheses, as a structured summary. Optional range, max_chars, and full_output_file controls for large contexts.
rocq_query	Non-state-changing query (Check, Print, Search, …). Optional max_chars and full_output_file controls for large output.
rocq_status	Report whether one session is started.
rocq_list	List open session ids.

Session lifecycle (must be followed in order)

rocq_start ─► rocq_step_to* ─► rocq_goals / rocq_query (any order, any time)
                                        │
                                        └─► rocq_step_to (advance further or rewind)
                                                │
                                                ▼
                                          rocq_close

Every tool except rocq_start and rocq_list requires a session_id that rocq_start returned. rocq_close is mandatory on exit — a leaked session keeps a coqidetop subprocess alive.

Position convention

• line and col at the tool boundary are 1-indexed (line 1 is the first line of the file; col 1 is the first column).
• line=-1 is an explicit EOF target that ignores col. Use it when you want to run through the whole buffer, especially for files with trailing blank lines.
• line values past the end of the buffer are accepted and clamped to EOF.
• col is optional on rocq_step_to; when omitted, the server targets end-of-line (inclusive of any terminating .).
• Coqtail's semantics are preserved on both sides: a sentence is kept iff its closing . is at or before (line, col). On rewind, anything strictly after that boundary is popped via a single Edit_at.
• endpoint in responses is 1-indexed [line, col_after_dot] (i.e. one past the terminator), or null if nothing has been executed.

Working principles

These are not server-enforced — they are practitioner conventions that make the difference between using this server well and fighting it.

1. Search before you prove. rocq_query("Search ...") / rocq_query("Check ...") / rocq_query("Print ...") are free — they don't consume state. Run at least one search before writing any non-trivial tactic. The most common agent failure mode is reproving a stdlib lemma from scratch.
2. Step, don't compile. Inside the proof loop, prefer rocq_step_to(line=-1, reload_from_file=true) over coqc / make / dune build. Each external compile re-checks the entire file from scratch; stepping only re-checks the diff. (See examples/AGENTS_CLAUDE.md for the rationale; it's a project convention, not a server limit.)
3. Goal-driven, not guess-driven. Read rocq_goals before choosing a tactic. The hypothesis list and conclusion shape almost always determine the right move. See proof-recipes.md § 4 for a goal-pattern → tactic table.
4. The file is the source of truth. There's no "send a sentence" primitive. Tactics get tested by editing the .v file and asking the server to reload (reload_from_file=true). One implication: keep the file on disk in sync with what you want Rocq to see.
5. Don't change theorem statements. Headers, signatures, and doc comments are off-limits without explicit user approval. Same for introducing new global Axiom / Parameter / Conjecture — if a proof seems to need one, stop and ask.
6. 80-char line width. Standard Coq/Rocq formatting.

For full proof-craft guidance (search-first protocol, tactic cascade, error-pattern fixes, axiom hygiene, completion criteria), read references/proof-recipes.md.

Canonical workflows

Open a file and inspect the goal mid-proof

rocq_start(session_id="t1", file_path="/abs/path/to/proof.v",
           coq_path="/abs/path/to/_opam/bin")
  → { ok: true, session_id: "t1" }

rocq_step_to(session_id="t1", line=12)
  → { ok: true, success: true, endpoint: [12, 8] }

rocq_goals(session_id="t1")
  → { ok: true,
      summary: { in_proof: true, fg: [{hypotheses: ["n : nat"],
                                       conclusion: "n + 0 = n"}], ... } }

rocq_goals(session_id="t1", range=[-5, -1])
  → returns only the final five hypotheses in each focused goal. Positive
    values are 1-indexed; negative values count from the bottom. Each focused
    goal also includes `hypothesis_count`.

rocq_goals(session_id="t1", range=[-5, -1], max_chars=500)
  → every string in the goal response is capped at 500 characters.

rocq_goals(session_id="t1", range=[-5, -1], max_chars=500,
           full_output_file="/tmp/t1-goals.json")
  → response stays capped/ranged, while the file receives the full JSON
    tool payload before range/max_chars are applied.

rocq_close(session_id="t1")

summary.fg[i] gives the hypothesis list and conclusion as separate strings if you need to reason about them programmatically. If the full context might be large, first consider calling rocq_goals(..., range=[-20, -1]) or another narrow hypothesis range to save context. Add max_chars when individual hypotheses or conclusions may be large. Use full_output_file when the complete context may be useful but too large for the tool response.

Stream through a proof one tactic at a time

Do not send a full Add for each keystroke — instead, write each new tactic into the .v file on disk and ask rocq_step_to to catch up with reload_from_file=true. The server re-reads the file_path that was supplied to rocq_start, diffs it against the in-memory buffer, and rewinds only what's necessary.

# ...edit the .v file on disk...
rocq_step_to(session_id="t1", line=15, reload_from_file=true)
rocq_goals(session_id="t1")
# decide next tactic based on the goal, edit file, repeat

This requires the session to have been opened with file_path (not inline content). For inline-content sessions, open a fresh session when the source changes.

Query without disturbing state

rocq_query does not advance the session. Use it for Check, Print, Search, Locate, About, Compute, etc.

When you need to find a specific hypothesis or fact in a large context, prefer a targeted rocq_query (Search, Check, About, etc.) before asking rocq_goals for the full context. Use max_chars on broad queries such as Search to guarantee the message string stays within a fixed character budget. Use full_output_file to keep the in-band response small while writing the complete query result to disk.

rocq_query(session_id="t1", query="Search (_ + 0 = _).")
rocq_query(session_id="t1", query="Check plus_n_O")   # trailing dot optional
rocq_query(session_id="t1", query="Search (_ + 0 = _).", max_chars=1000,
           full_output_file="/tmp/t1-search.json")

Skip past an opaque proof you don't want to re-check

rocq_step_to takes admit=true, which rewrites any opaque (Qed./Admitted.) proof encountered during the advance into a single Admitted.. Useful when stepping far into a file that has expensive proofs earlier.

rocq_step_to(session_id="t1", line=200, admit=true)

Compact responses

The MCP tools intentionally return small envelopes:

• rocq_start: ok, session_id, startup_stderr
• rocq_step_to: ok, success, endpoint, error, error_range, stderr
• rocq_step_to timeout fields: timed_out, timeout_seconds when a per-sentence step_timeout fires
• rocq_goals: ok, summary, stderr, full_output_written_to
• rocq_query: ok, success, message, stderr, full_output_written_to
• rocq_query timeout fields: timed_out, timeout_seconds when query_timeout fires
• rocq_status: ok, started
• Rejected tool calls: ok, error

Optional fields are omitted when empty or absent. For example, successful steps omit error, error_range, and empty stderr; rocq_start omits empty startup_stderr; unnamed goals omit name. If ok is false, no other fields are returned. For rocq_goals and rocq_query, max_chars is a positive integer that caps each emitted string value independently. Truncated strings end with ..., with the suffix included inside the character limit. Pass full_output_file to write the complete tool payload as UTF-8 JSON before range or max_chars are applied. The response includes full_output_written_to with the resolved side-file path.

Per-sentence info-panel messages are kept internally by the session layer but are not exposed through the MCP tool response.

Example:

rocq_step_to(session_id="t1", line=5)   # file has: idtac "checkpoint reached".
  → {
      ok: true, success: true,
      endpoint: [5, 35]
    }

rocq_query(session_id="t1", query="Check no_such_name")
  → {
      ok: true, success: false,
      message: "The reference no_such_name was not found …"
    }

Error handling

ok: false means the MCP tool itself refused the call (unknown session, bad argument, …). The response includes a compact error string with the reason.

ok: true with success: false means Rocq accepted the call but rejected the input — e.g. a tactic failure or a syntax error. In that case error holds Rocq's message and error_range points at the byte range in the buffer (1-indexed [[sl, sc], [el, ec]]). Do not retry blindly; inspect error and adjust the buffer or tactic before calling rocq_step_to again.

If timed_out: true on rocq_step_to, the server intentionally interrupted the current Rocq sentence after step_timeout seconds. The endpoint is the current cursor position. Retry the same rocq_step_to call once to test progress; if the endpoint advances, continue, and if it stays fixed, inspect the next sentence for a non-terminating tactic or rerun with a larger step_timeout. If the timed-out sentence is Qed., Defined., or Admitted., prefer a larger timeout or step_timeout=0; proof closing often takes a long time and is less likely to be an infinite tactic loop.

If timed_out: true on rocq_query, the query was interrupted after query_timeout seconds. Queries do not advance state. Retry with a larger query_timeout, use query_timeout=0, or narrow broad queries such as Search / Compute.

{ ok: true, success: false,
  error: "The reference foo was not found in the current environment.",
  error_range: [[42, 1], [42, 12]],
  endpoint: [41, 14] }

If a rocq_step_to fails mid-batch, the endpoint reflects the last successful sentence — the Rocq state is consistent with that endpoint, and subsequent rocq_goals / rocq_query calls will work against it.

Gotchas

1. coq_prog should almost always be left blank. On Rocq ≥ 8.9, plain coqtop no longer speaks the IDE protocol and will silently hang. The server's auto-detection picks coqidetop on those versions. Pass coq_prog only if you know the binary name differs. init_timeout (default 60s) protects against that mistake.

2. step_timeout is per sentence, not per file. The default is 30s or $COQTAIL_MCP_STEP_TIMEOUT; pass step_timeout=0 to disable. A timeout returns timed_out: true with the last successful endpoint. If this happens at Qed., Defined., or Admitted., try a larger timeout before treating it as a loop.

3. query_timeout is per query. The default is 30s or $COQTAIL_MCP_QUERY_TIMEOUT; pass query_timeout=0 to disable. Query timeouts do not change the session state.

4. file_path must be absolute and must exist — the server refuses relative paths (they can be ambiguous in an MCP client whose CWD is not the user's working directory). If you only have a relative path, resolve it first with Read/LS or pass content directly.

5. Provide file_path OR content, not both. Rocq uses the path only to set the top-module name via -topfile; it does not re-read the file from disk. If you pass content, the server writes it to an internal buffer and makes up a safe module name.

6. One session per file (and per Rocq process). Reusing a session_id across files gives you Rocq state that thinks it's inside the first file's module. Open a fresh session for a different .v file.

7. The session's buffer is independent from the agent's Read cache. After you edit a file on disk with Edit/Write, subsequent rocq_step_to calls still see the buffer the server loaded. Pass reload_from_file=true on rocq_step_to (or open a new session) to push changes. reload_from_file only works when the session was started with file_path; inline-content sessions must be reopened.

8. Project settings are auto-detected for file_path sessions. The default build_system="prefer-coqproject" uses _CoqProject or _RocqProject files when found, otherwise it falls back to Dune. Project-file search first checks . and ./theories relative to the current working directory, then searches upward from the file:

   rocq_start(..., file_path="/abs/proj/src/foo.v")
   

   Use build_system="prefer-dune", "dune", or "coqproject" to control precedence. Pass extra_args for final overrides.

9. Rocq output strings are plain text. Richpp tags (syntax highlighting spans) are stripped from conclusions, hypotheses, query messages, and errors.

10. The file on disk is the unit of work — there is no "send a sentence" primitive. Tactics get tested by editing the .v file and asking the server to reload it (rocq_step_to(..., reload_from_file=true)). The server diffs the new buffer against the in-memory one and rewinds the minimum needed to stay consistent.

• Run a tactic at line L → edit the file, then rocq_step_to(line=L, reload_from_file=true).
• Backtrack → step to an earlier (line, col). Rewinds are position-based; reload_from_file=true handles diff-based rewinds automatically.
• Type-check the whole file interactively → rocq_step_to(line=-1, reload_from_file=true). Inside the proof loop this is preferred over coqc / make / dune build, which re-check from scratch every time and are catastrophic for tactic search. Reserve those for final/CI confirmation (see examples/AGENTS_CLAUDE.md).
• Verify a finished proof → step to EOF, then rocq_query("Print Assumptions name.") to confirm only standard axioms are used.
• Test N tactic candidates "in parallel" → see subagents.md; each subagent owns its own session.

Quality gate

A proof is complete (in this server) when all of the following hold:

1. rocq_step_to(session_id="...", line=-1, reload_from_file=true) returns success: true on the file as written. The session is the type-checker — there's no separate compile step.

2. No Admitted / admit remains in the agreed scope. (The server doesn't track this; do a text scan with Grep.)

3. rocq_query("Print Assumptions theorem_name.") lists only standard axioms — namely:

   • classic, NNPP (Coq.Logic.Classical_Prop)
   • functional_extensionality (Coq.Logic.FunctionalExtensionality)
   • propositional_extensionality (Coq.Logic.PropExtensionality)
   • proof_irrelevance (Coq.Logic.ProofIrrelevance)
   • JMeq_eq (Coq.Logic.JMeq)
   • real-number axioms (Coq.Reals.Rdefinitions / Raxioms)

   Anything else — especially project-local Axiom / Parameter / Conjecture — should be surfaced to the user.

4. No theorem / lemma statement was modified without explicit approval.

For final CI verification outside the interactive session, coqc or make / dune build is appropriate. Inside the loop, use rocq_step_to — see the working principles above.

When this skill is NOT the right answer

• One-shot file compilation (coqc is faster and simpler) — only use this server when you need interactive state.
• Parsing .v files statically — use Grep/Read directly; do not spawn a session just to read the buffer back.
• Non-Rocq provers — do not attempt to drive Lean, Agda, Isabelle, etc. through this server.

Capability check

Before using the skill's guidance, verify the server is reachable. The cheapest probe is a no-op that always returns quickly:

rocq_list()  → { ok: true, session_ids: [...] }

If this call fails at the MCP level, the server isn't registered. Tell the user to register it (see examples/mcp_config.json in the Coqtail-mcp repo) and stop — do not fall back to silently trying other tools.

References

• tools — per-tool argument and response details (envelope shapes, optional fields, common failures)
• workflows — extended tool-call recipes beyond the canonical examples above (audit, bisect, iterate, candidate testing, axiom audit, …)
• proof-recipes — proof-craft guidance using only this server's primitives (search-first, tactic cascade, goal-pattern table, error fixes, axiom hygiene, completion criteria, house conventions)
• subagents — when and how to delegate to subagents to compensate for the server's serial primitives (parallel candidate testing, background compilation, multi-file audits, search delegation)