Rocq Piler

🤖 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.

Tools

| Tool | Description | |------|-------------| | search_lemmas | Find relevant lemmas in the Coq environment by name or pattern | | edit_file | Write or modify .v files — auto-reports errors and goal state after each edit | | check_file | Full file verification with modes: full/errors/first for compact feedback | | stratify | Case-split a proof and auto-close easy cases; returns hash-addressable admits for survivors | | close_admits | Batch-close surviving admits with a portfolio of tactics (supports multi-line with bullets) | | reset_proof | Wipe a proof body and start fresh | | focus_proof | Inspect proof state: goals, bullet stack, admit hashes, proof script |

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

| Problem | Duration | Cost | Tools | |---------|----------|------|-------| | insertionsort | 206s | $0.03 | search(10), check(5), edit(5) | | depvec | 565s | $0.07 | edit(14), check(6) | | mergesort | 1018s | $0.19 | — |

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 focusproof return hashes for survivors, and closeadmits 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

Source & license

This open-source MCP server is cataloged on AgentStack and links to its original source — we do not rehost the code.

• Author: scidonia
• Source: scidonia/rocq-piler
• License: Apache-2.0

Install and usage instructions live in the source repository linked above.