Diagnosing stale LSP state in long-running sessions

[jessealama]

Problem

In long-running sessions (e.g., when using lean-lsp-mcp with Claude Code), the diagnostics returned by the LSP can become stale. Specifically, diagnostics may differ from what a fresh lake build <file> produces on the same file.

This issue is hard to reproduce reliably, but seems to occur when:

1. Files are edited externally (e.g., by an AI coding assistant)
2. leanclient syncs the new content via textDocument/didChange
3. Diagnostics are retrieved, but they don't reflect the true compilation state

Running lake build externally and then querying diagnostics can produce different (often more accurate) results.

Where does the problem originate?

This may be a layered issue:

Lean LSP server (incremental elaboration)
        ↑
   leanclient (Python LSP client)
        ↑
  lean-lsp-mcp (MCP wrapper)
        ↑
   Claude Code (edits files)

Lean LSP server: Uses incremental elaboration for performance. When textDocument/didChange is received, it re-elaborates the file but may use cached/stale internal state for imports and dependencies. This is likely the root cause.

leanclient: Correctly syncs file content to the LSP server. However, there may be limited options for forcing a full re-elaboration vs. incremental.

lean-lsp-mcp: Could detect staleness and trigger rebuilds, but this is a workaround rather than a fix.

Questions

1. Is there an LSP protocol mechanism to force the Lean LSP server to fully re-elaborate a file (not incrementally)?

2. Does closing and reopening a file (force_reopen=True) help clear the LSP server's internal state?

3. Should this be raised as an issue with the Lean project if the root cause is in the LSP server's incremental elaboration?

Potential mitigations

In leanclient

• Track file modification times to detect when external edits occurred
• Expose staleness detection so consumers can decide how to respond
• Test whether force_reopen=True helps vs. just didChange

In lean-lsp-mcp

• Detect staleness before returning diagnostics
• Auto-trigger lean_build when stale state is detected (slow but reliable)

Notes

• The issue primarily manifests in long-running agentic sessions with many edits
• Current workaround is periodic lean_build calls, but this is slow
• Understanding whether this is fixable at the client level or requires Lean changes would help prioritize the right solution

[oOo0oOo]

I need to give this some more thought.
In an agentic setup, we have a disconnect: The agent is directly editing files and not via leanclient.

We could implement filesystem watching but it feels hacky.
Currently I tend towards file modification times, its the most pragmatic solution. If we do this I would not expose this to the user by default.

Regarding your questions:

1. Close, re-open with dependencyBuildMode: once. This should restart the FileWorker for that file.
2. Yes. Even force_reopen=False works. I think the issue is edits happening after the file is already open.
3. I don't think so. Lean's LSP handles staleness correctly via $/lean/staleDependency. This feels client-side.

I agree that lake build is a bad solution.

[jessealama]

While investigating empty diagnostics in lean-lsp-mcp, I found a specific timing issue in _wait_for_line_range() that may be related.

The Problem

1. Full-file queries via _wait_for_diagnostics() send the textDocument/waitForDiagnostics RPC (Lean-specific extension) and set wait_for_diag_done=True
2. Range queries via _wait_for_line_range() do NOT send this RPC - they only poll state
3. is_ready() falls back to the 0.5s grace period (DIAGNOSTICS_GRACE_PERIOD) when wait_for_diag_done=False
4. If publishDiagnostics takes longer than 0.5s after fileProgress: [], the wait exits prematurely with empty diagnostics

Reproduction Scenario

1. File is edited externally (by Claude Code)
2. open_file() syncs content via didChange
3. Immediately call get_diagnostics(start_line=X, end_line=Y)
4. LSP processes quickly, sends fileProgress: []
5. 0.5s passes before publishDiagnostics arrives
6. is_ready() returns True (grace period elapsed), loop exits with empty diagnostics
7. Later, full-file query returns the errors correctly

Proposed Fix

Make _wait_for_line_range() also send the textDocument/waitForDiagnostics RPC to set wait_for_diag_done=True. This ensures the wait doesn't rely solely on the grace period.

In the meantime, I'll implement a workaround in lean-lsp-mcp that falls back to full-file query + manual filtering when a range query returns empty.

[oOo0oOo]

Happy new year! I'm back and will start to slowly work my way through the backlog...

Just a preliminary answer on this:
Unfortunately, waitForDiagnostics kinda defeats the purpose of _wait_for_line_range. It waits until diagnostics for the whole file have been received. We should investigate more, if there is another way to make _wait_for_line_range work.
Otherwise we might just replace it with _wait_for_diangostics.