LLM4Rocq/rocq-mcp
If you are the rightful owner of rocq-mcp and would like to certify it and/or have it hosted online, please leave a comment on the right or send an email to henry@mcphub.com.
The Rocq MCP Server is a Model Context Protocol server that facilitates interaction with the Rocq/Coq proof assistant using the Petanque protocol.
Tools
Functions exposed to the LLM to take actions
rocq_start_proof
Start a proof session for a specific theorem in a Coq/Rocq file.
rocq_run_tactic
Execute tactics or commands on the current proof state.
rocq_get_goals
Get the current proof goals for a session.
rocq_get_premises
Get available premises (lemmas, definitions) for the current proof state.
rocq_parse_ast
Parse a command and return its Abstract Syntax Tree.
rocq_get_state_at_position
Get the proof state at a specific position in a file.
rocq_get_file_toc
Get table of contents (available definitions and theorems) for a Coq/Rocq file.
rocq_search
Search for theorems, definitions, and other objects in the current context.
Prompts
Interactive templates invoked by user choice
No prompts
Resources
Contextual data attached and managed by the client