coqtail-mcp
CommunityDrive live Rocq/Coq sessions via MCP.
Authorpark-sunho
Version1.0.0
Installs0
System Documentation
What problem does it solve?
This skill enables automated, session-based interaction with Coq via the coqtail-mcp MCP server, letting an agent drive a live Rocq/Coq proof session from file or content.
Core Features & Use Cases
- Start and manage a Rocq/Coq session with rocq_start, reload and synchronize state with rocq_step_to, and inspect the current goal and hypotheses with rocq_goals.
- Perform non-state-changing queries using rocq_query, or check status with rocq_status and list sessions with rocq_list.
- Keep sessions isolated per file and control lifecycle, including closing sessions with rocq_close to avoid orphaned processes.
Quick Start
Start a session with rocq_start and then drive progression with rocq_step_to while inspecting goals via rocq_goals and issuing read-only queries with rocq_query.
Dependency Matrix
Required Modules
None requiredComponents
references
💻 Claude Code Installation
Recommended: Let Claude install automatically. Simply copy and paste the text below to Claude Code.
Please help me install this Skill: Name: coqtail-mcp Download link: https://github.com/park-sunho/Coqtail-mcp/archive/main.zip#coqtail-mcp Please download this .zip file, extract it, and install it in the .claude/skills/ directory.
Agent Skills Search Helper
Install a tiny helper to your Agent, search and equip skill from 471,000+ vetted skills library on demand.