peterthiemann/agda-mcp

v0.5.0MIT

Develop on-disk Agda proofs with semantic MCP tools and an incremental proof workflow.

Changelog

This file records notable changes to agda-mcp, with the most recent release first.

Bundled agda-proof Agent Skill and references in the npm package, with incremental proof development preferring guarded MCP mutations.
Server-side skill discovery: skills/list, skills/get, and ordinary MCP resources, with complete byte sizes/SHA-256 manifests and process-lifetime content snapshots. Discovery works without Agda or a loaded module.
Modern MCP 2026-07-28 support through the official v2 server SDK, retaining initialization-era clients through the same stdio executable. Includes per-request version/capability metadata, modern discovery/result formats, multi-round-trip workspace roots, cancellation and EOF cleanup.
A request-version guard rejects unsupported claims even after the stdio connection is pinned; v1 clients remain independent regression fixtures.
Portable plugin manifests, pinned npm command, installation/update guidance, repeatable ZIP packaging, and packed-install/live proof smoke checks.

Added MCP initialization instructions that teach clients the core Agda workflow, including policy discovery, dynamic workspace loading, compound context retrieval, fresh opaque-handle use, and transformation mutation overrides. The complete guidance fits within Codex's first 512 characters.

Added the --dynamic-workspaces startup flag and matching allowDynamicWorkspaces initialization option. When enabled, agda_load_module accepts an absolute workspaceRoot, allowing the model to select and lazily start a workspace without per-project MCP configuration.
Added capabilities.workspaceSelection to agda_server_info so clients can distinguish configured-root and request-selected workspace policies.
Added the --apply-edits startup flag and matching applyEditsByDefault initialization option. When enabled, case split, refine, and auto atomically update and typecheck the active source without a per-call apply: true; apply: false retains an explicit preview escape hatch.
Added capabilities.transformationDefault to agda_server_info so clients can discover whether omitted transformation policy means preview or apply.

Extended unit, property-based, and live-Agda coverage for server-wide mutation policy, per-call overrides, and all supported literate formats.
Extended canonical-path, schema, CLI, and MCP-service coverage for dynamic workspace authorization and containment.

Added includeContexts to agda_load_module and agda_typecheck so the newly returned goals and their local contexts can be collected in one MCP operation.
Added opt-in apply: true transactions for case split, refine, and auto. Proposed edits are fingerprint-checked, atomically written, and immediately typechecked; non-mutating preview remains the default.

Made the fast-response policy the default: slow calls defer after one second, native Agda events are omitted unless requested, MCP text content is compact, and the full normalized result is sent once in structuredContent.
Extended unit, live-Agda, property-based, and fuzz coverage for compound inspection, response shaping, multi-edit application, source races, and guarded direct transformations across all supported source formats.

Added opt-in non-blocking Agda operations. Calls can defer to bounded background jobs globally through asyncMode or per call through async and deferAfterMs.
Added agda_job_await, agda_job_await_any, agda_job_status, agda_job_cancel, and agda_job_list for collecting and managing deferred work.
Added MCP progress heartbeats and completion notifications for long-running operations.
Added per-call timeoutMs, includeRaw, and diagnosticsOnly controls while preserving the original synchronous, native-raw defaults.
Added agda_retrieve_contexts for bounded, ordered retrieval of several goal contexts in one MCP round trip, including per-goal success or failure.
Added configuration limits for job retention and capacity, wait and deferral windows, abort grace, Agda installation probes, handle entropy, progress intervals, response shaping, and context batch size.

Strengthened opaque goal handles with configurable cryptographic entropy and load-generation binding. Every load, typecheck, module switch, process recovery, and edit-preview restoration now invalidates older handles, even when the top-level source bytes are unchanged.
Raw Agda events can now be omitted without losing truncation and completeness metadata. Batched responses share one bounded raw-event budget.
Agda installation probes now use dedicated timeout and output-buffer limits instead of sharing the general command timeout.
Expanded unit, integration, property-based, and fuzz coverage for job lifecycle behavior, queue policy, response shaping, batching, handle safety, cancellation, and event-loop liveness.
Extended the tagged-release workflow to publish to npm through an OIDC trusted publisher and attach the package tarball and SHA-256 checksum to the GitHub release.

Initial public release of the standalone TypeScript MCP server.
Added long-lived agda --interaction-json subprocesses, one loaded top-level module per active workspace, and a transport-independent application layer exposed over stdio.
Added tools for loading and typechecking modules, retrieving goals, contexts, and constraints, previewing case split, refine, and auto operations, normalizing expressions, inferring types, and querying metavariables.
Added normalized responses with bounded native Agda events in raw, opaque workspace and goal handles, serialized per-workspace commands, cancellation, output limits, and process recovery.
Added non-mutating, reload-after-preview edit transactions for .agda, .lagda, and .lagda.md source files.
Added Agda installation and project discovery, including .agda-lib files, registered libraries, workspace overrides, and conservative compatibility handling for Agda versions other than the verified 2.8.0 adapter.
Added unit, integration, property-based, mutation-fuzz, live-Agda, MCP stdio, smoke, and packed-install tests.