Long-lived Isabelle session shared across every prove_isabelle and query_backend backend: "isabelle" call for the lifetime of the MCP server.

The first isabelle call pays the ~seconds HOL session-start cost; subsequent calls reuse the open session. If the underlying session dies (Isabelle crash, network drop), the next call transparently opens a fresh one.

Drop-in for AtpClient.Isabelle in AtpMcp's backends map: exposes the same query/2, prove_theory/3, verify/1, and label/0 entry points the tool dispatch in AtpMcp calls, so no call site changes.

Concurrency

Calls serialise through this GenServer's mailbox. IsabelleClient.Shared can only run one use_theories at a time per session anyway, so serialising at this level is not a throughput loss and keeps the session state simple.

Cancellation

When AtpMcp.Runtime kills a tool-call Task, this GenServer keeps processing the in-flight use_theories on behalf of the (now dead) caller. The reply is discarded and the session stays warm for the next call. Isabelle has no remote-cancel endpoint, so the theory runs to completion server-side either way; killing the session would only add a session-restart penalty and disrupt concurrent calls.