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
insertion_sort	206s	$0.03	search(10), check(5), edit(5)
dep_vec	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 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