agda-mcp
Server Configuration
Describes the environment variables required to run the server.
| Name | Required | Description | Default |
|---|---|---|---|
| AGDA_MCP_OPTIONS | No | JSON object with server configuration options. See README for allowed fields. |
Instructions
Guidance the server publishes about itself, which clients place ahead of the tool catalog so the model reads it before choosing anything.
This server publishes no instructions, or was last inspected before Glama recorded them.
Capabilities
Features and capabilities supported by this server
Protocol revision2025-11-25
| Capability | Details |
|---|---|
| tools | {
"listChanged": true
} |
| logging | {} |
| resources | {
"listChanged": true
} |
| extensions | {
"io.modelcontextprotocol/skills": {}
} |
Tools
Functions exposed to the LLM to take actions
| Name | Description |
|---|---|
| agda_server_infoB | Report the detected Agda installation, compatibility, and active workspaces |
| agda_load_moduleA | Load and typecheck one top-level Agda module from disk; with --dynamic-workspaces, pass workspaceRoot to select its workspace at runtime |
| agda_typecheckC | Reload and typecheck the active module in a workspace |
| agda_retrieve_goalsC | Retrieve the current visible goals and opaque handles |
| agda_retrieve_contextC | Retrieve the type and local context for an opaque goal handle |
| agda_retrieve_contextsB | Retrieve types and local contexts for several goal handles in one round trip |
| agda_retrieve_constraintsC | Retrieve constraints for the active module in a workspace |
| agda_case_splitC | Case split using the server mutation policy; apply overrides that policy |
| agda_refineC | Refine using the server mutation policy; apply overrides that policy |
| agda_autoC | Run Agda proof search using the server mutation policy; apply overrides it |
| agda_normalize_expressionC | Normalize an expression in workspace or goal-local scope |
| agda_infer_typeC | Infer the type of an expression in workspace or goal-local scope |
| agda_query_metavariablesC | Query visible and interaction-backend invisible metavariables |
| agda_job_awaitA | Collect the result of a pending Agda job, waiting up to waitMs; returns pending again if still running |
| agda_job_await_anyA | Wait for the FIRST of several pending jobs to finish; use after fanning work out across workspaces |
| agda_job_statusB | Report the state of a pending Agda job without waiting for it |
| agda_job_cancelA | Abort a pending Agda job and release its Agda command slot |
| agda_job_listA | List Agda jobs that are still running or awaiting collection |
Prompts
Interactive templates invoked by user choice
| Name | Description |
|---|---|
No prompts | |
Resources
Contextual data attached and managed by the client
| Name | Description |
|---|---|
| agda-proof | Develop and inspect on-disk Agda proofs with agda-mcp: typecheck modules, inspect holes and constraints, infer or normalize expressions, and refine, case split, or search for proofs. Use for Agda source and interaction failures; not Lean, Coq, general dependent-type explanations, or development of the MCP server itself. |
| agents/openai.yaml | |
| references/tools.md |
TDQS
Scored across 18 tools
Most tools map to clearly distinct actions: job lifecycle (cancel/list/await/await_any/status), retrieval (goals/context/contexts/constraints), and mutations (case_split/refine/auto) are well separated. Minor confusion risks remain between agda_retrieve_context vs agda_retrieve_contexts (singular/plural one-vs-many) and between agda_retrieve_goals vs agda_query_metavariables, since goals are metavariables in Agda.
Nearly all names follow the agda_<verb>_<noun> snake_case pattern and job-related tools share a coherent agda_job_* prefix. A few deviate to noun-only or bare-verb forms (agda_server_info, agda_job_status, agda_typecheck, agda_auto), which is readable but slightly inconsistent.
18 tools is on the heavy side but each maps to a real Agda interaction-protocol operation, and the job-management cluster is needed for async/multi-workspace use. Nothing appears obviously redundant, though a few retrieval tools could conceivably be folded together.
The core proof-interaction lifecycle is covered (load, typecheck, goals, context, constraints, case split, refine, auto, normalize, infer, metavariable queries, job control). However, notable Agda operations are missing: 'give' (fill a goal with an expression, distinct from refine) and 'search/about' for lemma discovery, plus no explicit combined goal type-and-context call.