AtpMcp (atp_mcp v0.3.0)

Copy Markdown View Source

MCP stdio server wrapping every AtpClient backend.

Started by Claude Code (or any other MCP host) as a child process; reads newline-delimited JSON-RPC 2.0 from stdin and writes responses to stdout.

Tools

Generic, multi-backend (use the unified AtpClient.Backend contract):

  • list_backends — enumerate configured backends and their labels;
  • verify_backend — probe a backend's configuration / reachability;
  • query_backend — submit a TPTP problem to any backend and get a normalized SZS result.

Backend-specific, kept because they expose surface the unified contract does not (system enumeration, multi-system fan-out, hand-written theories, source diagnostics):

Cancellation and progress

Long-running tool calls (run_prover, compare_provers, query_backend, prove_isabelle) run inside their own Task in AtpMcp.Runtime. The MCP host can:

  • Send notifications/cancelled carrying the in-flight request id to abort a call. The Task is killed, and each AtpClient backend tears down its upstream work in response (see AtpMcp.Runtime's moduledoc for per-backend details). SOTPTP is the only backend that cannot truly cancel server-side — its :time_limit_sec is the only bound on remote work.
  • Set _meta.progressToken on tools/call to receive periodic notifications/progress frames while the call is in flight (heartbeat every five seconds by default; configurable via :atp_mcp, :heartbeat_ms).

Forward note: MCP experimental Tasks primitive

The 2025-11-25 MCP revision incubates a Tasks primitive for long-running invocations (call-now / fetch-later, with a task handle for status polling and deferred result retrieval). That maps almost exactly onto ATP workflows. When the primitive stabilises, the long-running tools here should grow a task-returning variant and a StarExec-style submit/await pair becomes a natural addition.

Protocol

Speaks MCP revision 2025-11-25. The initialize handshake, ping, tools/list, and tools/call are implemented; notifications are accepted and silently acknowledged.

Summary

Functions

classify(arg1)

Decide what to do with one decoded JSON-RPC message. Pure: returns a tag that handle_rpc/1 (synchronous) and AtpMcp.Runtime (asynchronous) interpret in their own way.

execute_tool(name, args)

Run a tool by name. Catches exceptions and returns an Error: … string in their place, matching the tool-result error convention.

handle_rpc(line)

Parse one JSON-RPC line and return the encoded response, or nil for notifications and blank lines. Provided for tests that drive the protocol synchronously without spinning up AtpMcp.Runtime.

main(args \\ [])

Functions

classify(arg1)

@spec classify(map()) ::
  {:reply, map()}
  | {:tool_call, term(), String.t() | nil, map(), term() | nil}
  | {:cancel, term()}
  | :noop

Decide what to do with one decoded JSON-RPC message. Pure: returns a tag that handle_rpc/1 (synchronous) and AtpMcp.Runtime (asynchronous) interpret in their own way.

execute_tool(name, args)

@spec execute_tool(String.t() | nil, map()) :: String.t()

Run a tool by name. Catches exceptions and returns an Error: … string in their place, matching the tool-result error convention.

handle_rpc(line)

@spec handle_rpc(String.t()) :: String.t() | nil

Parse one JSON-RPC line and return the encoded response, or nil for notifications and blank lines. Provided for tests that drive the protocol synchronously without spinning up AtpMcp.Runtime.

main(args \\ [])