boulodromeversion Documentation on ocaml.org
MCP server for Rocq/Coq proof assistance via Petanque
Boulodrome gives LLMs interactive access to the Rocq proof assistant through the Model Context Protocol (MCP). It exposes tools for starting proof sessions, running tactics, inspecting goals, searching the library, and undoing steps, turning theorem proving into a tool-calling loop.
| Author | Valentin Bergeron <dev.vbergeron@gmail.com> |
|---|---|
| License | Apache-2.0 |
| Published | |
| Homepage | https://github.com/vbergeron/boulodrome |
| Issue Tracker | https://github.com/vbergeron/boulodrome/issues |
| Maintainer | Valentin Bergeron <dev.vbergeron@gmail.com> |
| Dependencies | |
| Source [http] | https://github.com/vbergeron/boulodrome/archive/refs/tags/v0.6.1.tar.gz md5=e8c6dc40026ba1f6aac60e63b24acab1 sha512=51605d251ffc4dbd5d672142429cda2b785da61ea2e5e5a6f0b13a4a46be9edb5cd84928df541e5876c93487b9bef91955834e1c7b654b2ffe728de9945275ad |
| Edit | https://github.com/ocaml/opam-repository/tree/master/packages/boulodrome/boulodrome.0.6.1/opam |
No package is dependent
