Tools

rocq_start_proof

Opens a proof session for a named theorem inside a .v file.

Returns the initial goal state. Automatically discovers and loads Rocq loadpaths from dune files in the workspace.

rocq_run_tactics

Executes a list of tactics on the current proof state. Stops at the first failure.

Returns the output of each tactic. If a tactic fails, the proof state is not advanced past the failure and the error message is included in the response.

rocq_try_tactics

Tries each tactic independently on the current proof state without modifying the session. Every tactic in the list is run from the same starting state, so you can compare alternatives even if some fail. Use rocq_run_tactics to commit the chosen tactic.

rocq_goals

Returns the current goal state for a session.

Returns focused goals, hypotheses, and any unfocused or shelved goals.

rocq_premises

Returns up to 20 premises (lemmas and definitions) available in the current proof context.

Useful for discovering what lemmas are in scope before deciding which tactic to apply.

rocq_file_toc

Returns the table of contents of a .v file: all definitions and theorems with their kind, line number, and structural details.

Each entry shows the declaration kind, line number, and full statement. For example:

- [Inductive] nat { O, S } (line 5)
    Inductive nat : Set :=  O : nat | S : nat -> nat.
- [Theorem] plus_comm (line 12)
    Theorem plus_comm : forall n m : nat, n + m = m + n.
- [Definition] double (line 20)
    Definition double := fun n : nat => n + n.
- [Record] point { x, y } (line 25)
    Record point : Set := mk_point { x : nat; y : nat }.

Use this to discover what theorems are available before starting a session.

rocq_diagnostics

Returns all diagnostic messages (errors, warnings, information, hints) for a .v file. Use the optional severity parameter to filter to a single level.

Each diagnostic is formatted as l<line>c<col>-l<line>c<col>, <severity>: <message>.

rocq_search

Searches for theorems, definitions, and other objects using Rocq's Search, SearchPattern, or SearchRewrite commands. The query is passed verbatim as the argument to the chosen command.

Provide either session_id (to search in a proof context) or file_path (to search from a file's root context). session_id takes precedence.

Query syntax (for kind="search")

• Pattern: (_ + _ = _ + _) — type pattern with holes _ or named metavariables ?n
• Name substring: "assoc" — quoted string, matches object names containing the substring
• Notation: "+" — quoted, finds objects whose type uses this notation
• Qualifiers: hyp:, concl:, head:, headhyp:, headconcl: before a pattern or string
• Negation: - query — exclude matching objects
• Kind filter: is:Lemma, is:Definition, is:Instance, is:Fixpoint, etc.
• Scope: ... inside ModuleName or ... outside ModuleName
• Disjunction: [ query1 | query2 ]

A pattern whose top level uses an infix operator -- e.g. the sumbool type {n < m} + {n = m} + {m < n} -- must be wrapped in parentheses, since Rocq's Search grammar otherwise splits unparenthesized whitespace-separated tokens into several conjunctive query items and the top-level + collides with that. If a query without outer parentheses hits this, rocq_search automatically retries it wrapped in (...) before giving up.

Examples

For kind="search_pattern": matches the conclusion shape only (not subterms). For kind="search_rewrite": finds rewrite lemmas where one side of an equality matches the pattern.

rocq_inspect

Inspect a Rocq term or object using Check, Print, About, Locate, or Print Assumptions. Returns type signatures, full definitions, documentation, location information, or the axioms a proof depends on.

Provide either session_id (to inspect in a proof context) or file_path (to inspect from a file's root context). session_id takes precedence.

Commands

assumptions is useful to confirm a proof development is axiom-free (no Axiom, Parameter, or admit/Admitted in its dependency chain) before closing it out, without leaving the MCP to shell out to rocq compile.

rocq_undo

Undoes the last N tactic steps, restoring an earlier proof state.

Returns the number of steps actually undone and the goal state after undoing.

rocq_proof_script

Returns the exact sequence of tactics committed so far in a session, in the order they were run, in a form valid to paste verbatim between Proof. and Qed. in the source file.

This is the actual committed record — each entry of tac_list ever passed to rocq_run_tactics that succeeded, in order — not a transcription from the conversation. Reconstructing a proof script by hand is a correctness hazard: a tac_list is not a proof script, since a ;-chained tactic that applies across several goals breaks if split into separate .-terminated sentences. Use this tool instead of retyping the script to splice the proof back into the .v file.

Committed proof script for 'plus_comm' in /path/to/Foo.v
All goals closed -- safe to close with Qed.

--- paste verbatim between `Proof.` and `Qed.` ---
induction n.
- simpl. auto.
- simpl. rewrite IHn. auto.

rocq_list_sessions

Lists all currently open proof sessions.

No parameters.

Returns, for each session: the session id, its proof status (complete, in progress, or unknown), the theorem name, and the file path.

Open sessions (2):
- foo: in progress (theorem 'plus_comm' in /path/to/Foo.v)
- bar: complete (theorem 'plus_assoc' in /path/to/Foo.v)

rocq_end_session

Closes a proof session and frees its state.

Installation

Boulodrome is not published to opam, so it must be installed from source. It depends on coq-lsp (>= 0.2.5), which must be available in your opam switch.

git clone https://github.com/vbergeron/boulodrome
cd boulodrome
opam install . --deps-only
dune build
dune install

After dune install, the boulodrome binary is available in your opam switch's bin directory ($(opam var bin)/boulodrome).

Requirements

• OCaml >= 5.2.1
• dune >= 3.21
• coq-lsp >= 0.2.5 (provides Petanque and Fleche)
• yojson, logs

Usage from Rocq projects

Run boulodrome from the root of your Rocq project (or pass the root as an argument). It will walk the directory tree looking for dune files containing (rocq.theory ...) or (coq.theory ...) stanzas and add the corresponding loadpaths automatically.

# From within the project root:
boulodrome

# Or explicitly:
boulodrome /path/to/your/rocq/project

The MCP client (your IDE or agent) connects over stdio. File paths passed to tools must be absolute.

Cursor / Claude configuration

Boulodrome is configured as an MCP server in your editor or agent. A ready-made rule file is provided in rules/boulodrome-mcp.mdc. Copy it into your Rocq project's .cursor/rules/ directory (or the equivalent rules directory for your editor):

cp rules/boulodrome-mcp.mdc /path/to/your/rocq/project/.cursor/rules/

The MCP server itself is registered in your editor's MCP settings:

Cursor (~/.cursor/mcp.json or the project-level .cursor/mcp.json):

{
  "mcpServers": {
    "boulodrome": {
      "command": "boulodrome",
      "args": ["/path/to/your/rocq/project"]
    }
  }
}

Claude Code (.mcp.json in the project root):

{
  "mcpServers": {
    "boulodrome": {
      "command": "boulodrome",
      "args": ["."]
    }
  }
}

License

Apache-2.0 — see LICENSE.

Changelog

See CHANGES.md for the full release history.