罗克·麦克普
将AI代理连接到的MCP服务器 洛克 证据助理。 它包起来了 vsrocqtop （Rocq LSP服务器）并通过MCP公开证明检查工具， 这样代理就可以打开 .v 文件，遍历证明，检查目标，并交互式地修复错误。
工具
| 工具 | 说明 |
|---|---|
rocq_open | 打开a .v 校样检查器中的文件 |
rocq_close | 关闭文件并释放资源 |
rocq_sync | 编辑后从磁盘重新读取文件 |
rocq_check | 检查到某个位置；返回目标和诊断 |
rocq_check_all | 检查整个文件 |
rocq_step_forward | 向前走一句话 |
rocq_step_backward | 后退一句话 |
输出格式
所有证明操作都返回相同的格式：完整的当前重点目标， 包括任何未集中注意力/搁置/放弃的目标、证明信息和 诊断。
安装
先决条件
安装 vsrocqtop:
opam install vsrocq-language-server安装
go install github.com/sanjit/rocq-mcp@latest用法
配置你的项目
添加一个 .mcp.json 到您的Rocq项目根目录：
{
"mcpServers": {
"rocq": {
"command": "./etc/run-rocq-mcp.sh"
}
}
}创建 etc/run-rocq-mcp.sh:
#!/usr/bin/env bash
ARGS=$(sed -E -e '/^#/d' -e "s/'([^']*)'//g" -e 's/-arg //g' _RocqProject)
exec rocq-mcp $ARGS这读你的 _RocqProject 文件并将标志（加载路径、警告等）传递给 vsrocqtop.
允许在Claude代码中使用MCP工具
在 .claude/settings.local.json:
{
"permissions": {
"allow": [
"mcp__rocq"
]
},
"enabledMcpjsonServers": [
"rocq"
]
}添加工作流技能
复制 .claude/skills/rocq-build/ 进入你的项目。这将教会代理打开/检查/编辑/同步工作流。
示例项目
看 防滑 用于工作设置。