park-sunho

park-sunho/Coqtail-mcp

Plugin Claude Code

Plugin marketplace listing 1 plugin: coqtail-mcp.

park-sunho/Coqtail-mcp

Plugin Claude Code

Drive a live Rocq/Coq proof session through coqtail-mcp. Bundles the skill (server mechanics + proof recipes) and four named subagents (proof-repair, admitted-filler-deep, axiom-auditor, proof-golfer).

park-sunho/Coqtail-mcp

Agent

Strategic resolution of a stubborn Admitted in a .v file via the coqtail-mcp server. Use when a fast pass has failed (3+ failed candidates with the same approach), when the proof needs a helper lemma or multi-step structuring, or when the goal requires careful library exploration. May refactor within the file's header…

park-sunho/Coqtail-mcp

Agent

Audit Print Assumptions of theorems in a .v file or directory via the coqtail-mcp server, and (optionally) eliminate non-standard axioms. Use to verify proof hygiene before a checkpoint, after a long proof session that may have introduced axioms, or when a theorem's trustworthiness needs explicit justification.

park-sunho/Coqtail-mcp

Agent

Golf compiling Rocq proofs via the coqtail-mcp server — improve directness, clarity, performance, and brevity without changing semantics. Use only on files that currently type-check end-to-end (no Admitted in scope, step-to-EOF passes). Typical reduction 20–40%; reverts immediately on any verification failure.

park-sunho/Coqtail-mcp

Agent

Compiler-guided iterative proof repair via the coqtail-mcp server, with two-stage budget (6 fast attempts → 18 strategic). Use when stepping a .v file produces a tactic error, type mismatch, unification failure, missing reference, syntax error, or unsolved goals. Outputs only a unified diff or REPAIR FAILED — no prose.

park-sunho/Coqtail-mcp

Skill Claude CodeCodex

Drive a live Rocq/Coq proof session through the coqtail-mcp MCP server — start a session from a .v file, step forward/backward to any line, inspect the current goal and hypothesis context, and run read-only queries (Check, Print, Search). Trigger when the user wants to step through a Rocq proof interactively, inspect…