package boulodrome

  1. Overview
  2. No Docs
MCP server for Rocq/Coq proof assistance via Petanque

Install 

dune-project
 Dependency

github.com Edit opam file Versions (1)

Authors

  1. V
    Valentin Bergeron <dev.vbergeron@gmail.com>

Maintainers

  1. V
    Valentin Bergeron <dev.vbergeron@gmail.com>

Sources

v0.6.1.tar.gz
md5=e8c6dc40026ba1f6aac60e63b24acab1
sha512=51605d251ffc4dbd5d672142429cda2b785da61ea2e5e5a6f0b13a4a46be9edb5cd84928df541e5876c93487b9bef91955834e1c7b654b2ffe728de9945275ad

Description

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.

Added to opam-repository:

Dependencies (5)

  1. coq-lsp >= "0.2.5+9.1"
  2. logs
  3. yojson
  4. ocaml >= "5.2.1"
  5. dune >= "3.21"

Dev Dependencies (1)

  1. odoc with-doc

Used by

None

Conflicts

None