Fix fetch failed on long-running MCP TLC tool calls#524
Merged
Conversation
Long-running TLC runs invoked through the MCP server (e.g.
`tlaplus_mcp_tlc_check` on a non-trivial spec) failed in Cursor with
`{"error":"fetch failed"}` after roughly a minute. MCP clients using
Streamable HTTP wrap each tool call in a single fetch() against the
SSE response stream; if the server stays silent for too long the
client aborts the underlying socket even though TLC is still
model checking.
Declare the `logging` capability on the MCP server, thread the SDK's
`RequestHandlerExtra` into runTLCInMCP, and emit a `notifications/message`
event every 10s while a TLC tool is running. The ping uses level
`debug` so MCP clients (Cursor, Claude Code, ...) do not surface it
in chat. The timer is cleared on process `close` so we never keep
pinging a stream after the run ends. A focused test in
`tests/suite/lm/mcpServer.test.ts` pins down both halves of that
contract: the timer must fire repeatedly while TLC runs and must
stop once the run finishes.
Also leave a TODO on runTLCInMCP for streaming TLC's partial output
to the MCP client at runtime (orthogonal to the keep-alive). The LLM
currently only sees TLC's stdout/stderr after the process exits,
which is too late for diagnosing runaway runs / state-space
explosion: those need TLC's periodically emitted coverage and
progress lines while TLC is still running.
We also explored implementing cancellation for MCP-driven TLC runs
on top of the same SDK plumbing, but manual testing showed it does
not help in Cursor today: Cursor's chat "Cancel" button is purely
client-side. It neither sends `notifications/cancelled` nor closes
the SSE socket, so the server is never told that the user wanted to
stop, and the AbortSignal that the SDK threads through
`RequestHandlerExtra.signal` never fires. This is reported upstream
and may be a regression in recent Cursor builds (Cursor's MCP-side
quality has been noticeably uneven lately):
https://forum.cursor.com/t/cursor-doesnt-send-mcp-cancellation-notifications-when-user-clicks-cancel-button/138669
Until that is fixed, users who want to abort a runaway TLC run
started by an MCP client should hit the stop button in the TLA+
model checking pane, which already terminates the underlying TLC
process.
Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Updated the CheckModel cancellation tests to create temporary TLA+ and CFG files dynamically, improving isolation and reliability. The tests now ensure proper cleanup of temporary files and diagnostic collections after execution. This change enhances the robustness of the test suite by avoiding potential conflicts with existing files and ensuring a clean testing environment. Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
lemmy
marked this pull request as ready for review
May 7, 2026 01:02
lemmy
changed the title
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Long-running TLC runs invoked through the MCP server (e.g.
tlaplus_mcp_tlc_checkon a non-trivial spec) would fail in Cursor with{"error":"fetch failed"}after roughly a minute, and a TLC process orphaned by a cancelled tool call would keep running on the side until it finished on its own.