🤖 rocq-piler

Let rocq-piler do the heavy lifting for your proofs.

Overview

rocq-piler is an MCP server for interactive Coq/Rocq proof development via coq-lsp. It provides a tool suite that lets AI agents explore, write, verify, and refine proofs with immediate feedback.

Related MCP server: lean-lsp-mcp

Tools

Workflow Discipline

The most effective approach for AI proof assistants:

1. edit_file first — write proofs and helper lemmas directly. Instant error + goal feedback per edit. No need for bash + coqc.

2. check_file for status — use mode: "errors" (compact) for quick verification, mode: "first" for tight feedback loops.

3. stratify to escalate — when a proof has too many cases to write by hand, split it with stratify. Returns hash-addressable admits for survivors.

4. close_admits to finish — batch-close survivors by hash. Tactics support multi-line scripts with bullets.

5. reset_proof when stuck — wipe and restart cleanly. Auto-detect thrashing after 5 consecutive same-error edits.

Benchmarks

Stats are updated as runs complete. All benchmarks use DeepSeek V4 Pro.

Architecture

rocq-piler uses a content-addressed admit system: every open goal has a unique hash computed from its goal text. Stratify and focus_proof return hashes for survivors, and close_admits targets them by hash — close all matching admits at once across any bullet depth.

edit_file → instant feedback → check_file → stratify → close_admits → Qed

Getting Started

Prerequisites

opam install coq-lsp

Installation

cd rocq-piler
npm install
npm run build
npm test                 # unit tests
npm run test:integration # integration tests

Usage with OpenCode

Add to ~/.config/opencode/opencode.json:

{
  "mcp": {
    "rocq-piler": {
      "type": "local",
      "command": ["node", "/path/to/rocq-piler/dist/index.js", "--coq-lsp-path", "coq-lsp"],
      "enabled": true
    }
  }
}

Running Benchmarks

# Single run
bash benchmarks/harness/run.sh --model deepseek/deepseek-v4-pro --problem pcf_ref

# Batch sweep
bash benchmarks/harness/batch.sh --problems insertion_sort,dep_vec,pcf_ref

# Evaluate
bash benchmarks/harness/evaluate.sh benchmarks/complete/pcf_ref.v

License

MIT