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 | {} |
Tools
Functions exposed to the LLM to take actions
| Name | Description |
|---|---|
| agda_server_infoA | Report the detected Agda installation, compatibility, and active workspaces |
| agda_load_moduleB | Load and typecheck one top-level Agda module from disk |
| agda_typecheckB | 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_constraintsB | Retrieve constraints for the active module in a workspace |
| agda_case_splitA | Preview a case split, or atomically apply and typecheck it with apply:true |
| agda_refineB | Preview a refinement, or atomically apply and typecheck it with apply:true |
| agda_autoA | Preview Agda proof search, or atomically apply and typecheck it with apply:true |
| agda_normalize_expressionB | Normalize an expression in workspace or goal-local scope |
| agda_infer_typeB | 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_statusA | 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 |
|---|---|
No resources | |
TDQS
Scored across 18 tools
Each tool targets a distinct aspect of Agda interaction: loading, typechecking, goal/context retrieval, constraints, proof actions (case split, refine, auto), expression/inference queries, and job management. Even similar-looking tools like agda_retrieve_context and agda_retrieve_contexts differ in singular vs batch semantics, and agda_retrieve_goals vs agda_query_metavariables distinguish visible vs all metavariables.
All tools follow the uniform pattern agda_<verb>_<noun>, with clear verbs like load, typecheck, retrieve, refine, normalize, infer, query, and job actions (await, cancel, list). The naming is predictable and consistent, making it easy to guess tool purposes.
18 tools is on the higher side (borderline heavy), but each tool maps to a necessary operation in the Agda proof assistant workflow. The count is justified by the breadth of features (module loading, typechecking, goal management, proof actions, metavariable queries, and async job handling) without redundant tools.
The toolset covers the core lifecycle of Agda development: loading/typechecking modules, inspecting goals/contexts/constraints, applying proof tactics (case split, refine, auto), normalizing/inferring expressions, and managing asynchronous jobs. Minor gaps include no explicit module list or workspace management, but the essential operations are present and no dead ends are apparent.