About Coqtail MCP
Coqtail MCP is an MCP server in the Other category: interactive Rocq / Coq Proofs for AI Agents.
Install
git clone https://github.com/park-sunho/Coqtail-mcpThis server has no ConduID identity, so agent calls to it are not receipted. Pin the version you install and review the source before granting it credentials.
Tools (7)
rocq_closeTerminate a session's subprocess and forget it.
Parameters not published.
rocq_goalsReturn the current proof goal and hypothesis context as a structured summary. Accepts optional `range`, `max_chars`, and `full_output_file` controls for large contexts.
Parameters not published.
rocq_listList active session ids.
Parameters not published.
rocq_queryRun a non-state-changing query (`Check`, `Print`, `Search`, …). Accepts optional `max_chars`, `full_output_file`, and `query_timeout` controls.
Parameters not published.
rocq_startSpawn a `coqidetop` subprocess. Accepts either `file_path` or inline `content`. Returns the session id and startup stderr.
Parameters not published.
rocq_statusReport whether one session is started.
Parameters not published.
rocq_step_toAdvance or rewind so the session's state matches `(line, col)`. Optionally re-reads the original `file_path` from disk (`reload_from_file`), admits opaque proofs (`admit`), and caps each Rocq sentence with `step_timeout`.
Parameters not published.
Ask AI
Ask AI about Coqtail MCP
Powered by Claude · Grounded in docs
Security checks
6 checks have not been run yet.