# Rocq Piler

> MCP server for Coq LSP

- **Type:** MCP server
- **Install:** `agentstack add mcp-scidonia-rocq-piler`
- **Verified:** Yes — security-reviewed for prompt injection and unsafe behavior
- **Seller:** [scidonia](https://agentstack.voostack.com/s/scidonia)
- **Installs:** 0
- **Category:** [Integrations](https://agentstack.voostack.com/c/integrations)
- **Latest version:** 0.1.0
- **License:** Apache-2.0
- **Upstream author:** [scidonia](https://github.com/scidonia)
- **Source:** https://github.com/scidonia/rocq-piler

## Install

```sh
agentstack add mcp-scidonia-rocq-piler
```

Requires the [AgentStack CLI](https://agentstack.voostack.com/docs/cli). Works with Claude Code, Cursor, and any MCP-compatible agent.

## About

# 🤖 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
```bash
opam install coq-lsp
```

### Installation
```bash
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`:
```json
{
  "mcp": {
    "rocq-piler": {
      "type": "local",
      "command": ["node", "/path/to/rocq-piler/dist/index.js", "--coq-lsp-path", "coq-lsp"],
      "enabled": true
    }
  }
}
```

## Running Benchmarks

```bash
# 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](https://github.com/scidonia)
- **Source:** [scidonia/rocq-piler](https://github.com/scidonia/rocq-piler)
- **License:** Apache-2.0

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

## Pricing

- **Free** — Free

## Security capabilities

Automated source analysis of v0.1.0 — what this tool can access:

- **Network access:** no
- **Filesystem access:** no
- **Shell / process execution:** no
- **Environment & secrets:** no
- **Dynamic code execution:** no

*"Yes" means the capability is present in the source — more access means more to trust, not that it is unsafe.*


## Versions

- **0.1.0** — security scan: passed — Imported from the upstream source.

## Links

- Listing page: https://agentstack.voostack.com/l/mcp-scidonia-rocq-piler
- Seller: https://agentstack.voostack.com/s/scidonia
- Browse the marketplace: https://agentstack.voostack.com/browse

---
Listed on AgentStack — the marketplace for AI agent skills and MCP servers. Every listing is security-reviewed. Creators keep 70%.