Normalize and consolidate shared LSP calls

[Deicyde]

Stack status: ready for human review as a follow-up to #168, but do not merge into its feature branch. Merge-commit #168 first, retarget #111 to main, confirm the diff remains +133/−58, rerun CI, then squash-merge #111. If #168 is squash- or rebase-merged, restack #111 on the resulting main before retargeting.

Small follow-up to #168. That PR now owns verified process-group cleanup, retained cache retirement, startup handoff, and failed-session fencing; this restack removes the superseded implementation from #111.

Changes

• Add one _admitted wrapper for diagnostics and hover. It preserves the established ordering: hover input is read before admission, queue/deadline failures do not poison a healthy session, and an admitted failure marks retirement before releasing the operation lock.
• Add one _lsp_operation runtime wrapper for both public LSP methods. It preserves Retain Lean project ownership through verified cleanup #168's canonical lease_resolved/invalidate_resolved keys, state-based error routing, successful-but-poisoned retirement, and asynchronous cleanup ownership.
• Normalize every JSON decoder failure to LspProtocolError. CPython raises a plain ValueError (not JSONDecodeError) when an integer exceeds its configured digit limit, and RecursionError when arrays or objects nest past its recursion limit.

Regression coverage

• a failed operation fences a queued caller before protocol dispatch;
• post-admission budget exhaustion leaves the session healthy;
• exhausted didClose budget returns the completed result but retires the session;
• a 5,000-digit JSON integer reports an invalid protocol body;
• a body of 200,000 nested JSON arrays reports an invalid protocol body.

Scope

No process, cache, deadline, or public MCP contract is introduced here. #168 owns those contracts. This PR is a +133/−58 consolidation and normalization follow-up.

Validation

At exact head 2ce7ecb4 over #168 head 953ff2f7:

• full suite: 1,870 passed, 6 skipped, 1 expected failure;
• focused LSP/runtime suites: 113 passed;
• repeated queued-failure race: 20/20 passes;
• Ruff and git diff --check: pass;
• make check-example: pass, including strict MkDocs;
• two independent agent audits found no blocker; human GitHub review pending;
• exact-head GitHub CI: all 9 checks pass, including both real-Lean and both Windows/Python workflows.

0f789c28 then adds the RecursionError case. On it, tests/test_lsp_protocol.py passes (31 tests) on Python 3.13, the new test fails with a raw RecursionError without the fix, and Ruff and git diff --check pass. The full-suite and CI results above predate that commit.

[Deicyde]

Exact-head verification is complete at b85255f0. Both Python 3.10/3.13 jobs, both real-Lean jobs, Windows hardening, and CLA are green. Local full suite: 1,088 passed, 1 skipped; focused lifecycle suite: 68 passed; consumer example and strict MkDocs build pass. Independent security review re-ran the startup-lock, reused-PGID, poisoned-waiter, didClose, stale-replacement, multi-session, lifetime-lock, Windows, descriptor, cancellation, and real-descendant cases and reports SHIP. No known merge blocker remains.

[Deicyde]

Golfed and re-verified at ee352e59 (current main merged in).

What changed and why

• Rebuilt the fix on top of main and kept only what runtime: retain LSP ownership until process-group cleanup is verified #108 needs: process-group launch, group retirement through the existing _kill_subprocesses, poisoning before admission is released, and invalidate-before-abort in the runtime.
• Cleanup now retries until the group is verified gone instead of raising. That makes the ProjectResourceCache, factory, and LeanRuntimeServices.close changes redundant, so they are reverted to main.
• Removed the async-cancellation bookkeeping (pending-cancellation ordering, LspCleanupError, retry constants). The daemon runs requests on handler threads, and its SIGTERM/SIGINT handlers only request shutdown and stay installed until services.close() returns, so no BaseException can interrupt a session mid-cleanup.
• A didClose failure, or an exhausted budget, now poisons the session and returns the result already read, where the previous head raised. This keeps main's response contract and still never reuses the stream.

Diff vs base: 4 files, +1600/-90 → 4 files, +518/-27.

Checks: exact-head CI green (test 3.10/3.13, real Lean, Windows hardening, CLA): https://github.com/facebookresearch/autoform-bot/actions/runs/37386310084 and https://github.com/facebookresearch/autoform-bot/actions/runs/37386314139. Locally: ruff clean; tests/test_lsp_protocol.py 21 passed; LSP and lifetime-lock tests in tests/test_shared_lean_runtime.py 5 passed. Run against main's source, 11 of the 12 new tests fail. The lifetime-lock test passes there because it pins existing serve() behaviour.

Remaining risks

• is_alive() polls the wrapper. If that poll reaps the wrapper just before group retirement, the PGID could in principle be reused in that gap. The graceful close() path (wait() before killing the group) has the same window. Closing it fully would need pidfds.
• If a process group never dies, cleanup retries forever (logging, with backoff capped at 1s), which blocks the cache slot and runtime shutdown. This is deliberate: it fails closed rather than releasing ownership.
• Merges cleanly with Keep shared runtime status observational #112 in either order (checked with git merge-tree; the combined tree lints and has no duplicate test names).

Posted by PR swarm: Swarm · runtime #111+#112

[Deicyde]

Exact-head lifecycle review is complete at 58ff1a2e. Process-group ownership is retained through verified TERM/KILL/reap; failure invalidates the cache before synchronous abort while the lease stays active; poisoning precedes admission release; replacement waits for cleanup; and the daemon lifetime lock is released only after service close. Focused protocol/runtime tests and all nine GitHub checks pass, current main has no touched-file overlap, and no correctness blocker remains.

[Deicyde]

Independent review of 58ff1a2. An earlier swarm pass at ee352e5 found one regression and two golf items. f793cae, bb50482 and 58ff1a2 respond to them. This pass verified those fixes and then reviewed the new commits for fresh issues.

Verdict: fix first (small). The Latin-1 hover regression is fixed and pinned. Moving the read ahead of admission opened a narrower one: an unreadable hover file now kills the session while another caller's request is in flight (issue 1). A two-line change closes it. Everything else below is low severity, golf, or a design question for a maintainer.

Earlier findings

• A Latin-1 hover file kills the shared session (regression): fixed by f793cae.
  • hover() now reads before admission (server.py:226-228).
  • Both runtime handlers pass (LspBusyError, ValueError) through (lean_runtime.py:746-748, :770-772).
  • test_unreadable_hover_file_leaves_a_warm_lsp_session_alone (tests/test_shared_lean_runtime.py:705-751) fails if either half is reverted.
• No test pinned that LspBusyError leaves a healthy session alone: fixed by bb50482, for lsp.diagnostics only. Issue 4 covers the hover half.
• Golf, reuse _remaining for the didClose budget checks: done in 58ff1a2.
• Golf, close the pipes before signalling and drop _process_group_id: not done. Skipping it is fine. Re-measured, it saves about 5 lines, not 28, because the hover test's pid-less stub (tests/test_shared_lean_runtime.py:713-718) would need patching. The PR body gives the wrong reason for deferring it, though. test_cleanup_retry_never_resignals_a_retired_group passes unchanged under that ordering (simulated with the test's own fakes); only its comment at tests/test_lsp_protocol.py:164-165 would go stale.
• Correction to the earlier pass. It claimed every stream decode error is already wrapped as LspProtocolError, and it isn't (issue 2).

Confirmed issues

1. servers/lsp/server.py:228: an unreadable hover file now kills the session under another caller's in-flight request (low, regression).

• Scenario.
  • Client B is inside get_diagnostics on project P. It holds _operation_lock while a slow file elaborates.
  • Client A calls lean_hover on a file in P that can be stat'd but not opened. Either it is mode 000, or it was deleted after resolve_lean_file ran at lean_runtime.py:761.
  • read_text() raises PermissionError or FileNotFoundError before admission. That is an OSError, not a ValueError, so lean_runtime.py:773-776 invalidates the entry and calls session.abort().
  • abort() takes only _lifecycle_lock (server.py:141-144). It kills the process group and closes the pipes B is reading.
  • B's valid request fails with LspProtocolError("LSP process closed stdout mid-header").
• Before this PR. At ee352e5 and on main, the read ran under _operation_lock, so A queued behind B and B finished normally. Main also aborted on OSError, but only after B was done.
• It falsifies the PR body's invariant, "a caller's bad input or busy queue never retires a healthy shared session". Issue 3 does too.
• Severity: low. It needs an unopenable .lean file plus a concurrent request on the same project. Two narrower outcomes require B to stay off-CPU through the whole kill-and-reap, so treat them as theoretical:
  • B returns truncated diagnostics as success;
  • B busy-spins until its deadline once process is None.
• Fix, smallest. In hover(), use try: content = path.read_text() / except OSError as error: raise ValueError(f"Cannot read file: {error}") from error. UnicodeDecodeError isn't an OSError, so the existing test still passes.
• Fix, better. In both handlers, decide on session state instead of exception type: except Exception: if not session.is_alive(): invalidate; abort, then raise.
  • Delete both (LspBusyError, ValueError) clauses and the LspBusyError import (lean_runtime.py:44).
  • Why it is safe: every failure after admission already poisons the session (server.py:171-175, :244-248), so is_alive() is False exactly when the stream can't be trusted. Errors before admission and LspBusyError leave it True.
  • This also fixes issue 2.
  • The fake at tests/test_shared_lean_runtime.py:787-789 must then set self._poisoned = True before raising, as the real wrapper does.
• Test. Add a second case to the unreadable-hover test where the read raises PermissionError.
  • Monkeypatch Path.read_text for that one path. chmod 000 doesn't stop root.
  • Assert sessions[0].is_alive() and len(sessions) == 1.

2. servers/lsp/server.py:489: one stream decode error escapes as a plain ValueError, which the runtime treats as healthy input (low, contract).

• What happens.
  • _read_message wraps only (UnicodeDecodeError, json.JSONDecodeError).
  • json.loads raises a plain ValueError for an integer literal longer than 4300 digits (checked on Python 3.12).
  • Such a frame poisons the session, which is right. But except (LspBusyError, ValueError): raise then skips invalidate and abort.
  • So stats() keeps reporting the entry as valid, and the Lean process group lingers until the next lease, an LRU eviction or the 30-minute idle sweep.
• The diagnostics clause has no legitimate ValueError case. _get_diagnostics turns read and decode failures into a "Cannot read file" result (server.py:185-188). Any ValueError that reaches lean_runtime.py:746 therefore came from inside the poisoned operation.
• Severity: low. Lean's LSP sends only small integers, so this needs a misbehaving server. The cost is mostly a false contract: the f793cae message and the comments at lean_runtime.py:747 and :771 say stream decode errors can't take this route.
• Fix. Use except ValueError as error: at server.py:489. Both current types are subclasses, and the line count doesn't change. Then narrow the diagnostics clause to LspBusyError, or reword its comment. Issue 1's is_alive() routing covers this too.
• Test. Feed _read_message a frame containing a 5000-digit integer and expect LspProtocolError.

3. servers/lsp/server.py:339-343: an oversized input file still kills a healthy session before any byte is written (low, pre-existing).

• What happens. _write_message raises LspProtocolError("LSP request exceeds 16777216 bytes") before its first os.write, inside the poison wrapper. The runtime then retires a warm session for an input problem.
• This contradicts the new comment at server.py:226 ("a bad input file cannot poison the session"). Main does the same.
• It takes a file of roughly 10-14 MiB, because didOpen's JSON escaping grows Lean text by about 1.1-1.6x.
• Fix (a follow-up is fine). Check the size of the whole didOpen body, envelope and URI included, not just json.dumps(content).
  • In hover(), check before admission and raise ValueError.
  • In _get_diagnostics, return a "file too large" diagnostic next to "Cannot read file".

4. tests/test_shared_lean_runtime.py:663-702: the busy-session test covers only lsp.diagnostics, and nothing runs the post-admission busy raise on a real session (low, test gap).

• Two mutations pass the whole suite.
  • Narrowing lean_runtime.py:770 to except ValueError:. A hover that times out in the queue would then abort the shared session.
  • Moving the inner try: above remaining = deadline - time.monotonic() in get_diagnostics or hover. A call admitted after its budget ran out would then poison a healthy session, and the next lease would replace it.
• Why the tests miss them. bb50482's fake raises LspBusyError itself and never runs LeanLspSession. The only session-level queue test (tests/test_lsp_protocol.py:504-513) raises before admission.
• Fix.
  • Parametrize the busy test over lsp.diagnostics and lsp.hover.
  • Add a session-level case with LspConfig(timeout=0), the lock free and a fake process. acquire(timeout=0) succeeds, and remaining <= 0 always holds.
  • For both methods, assert LspBusyError and session.is_alive().

Golf (about 30 lines)

• servers/lsp/server.py:154-177 and :224-250 (about 19 lines).
  • The admission/poison block is duplicated, and the copies differ in one call.
  • Fold it into _admitted(self, operation: Callable[[float], T]) -> T and pass lambda remaining: self._get_diagnostics(file_path, timeout=remaining) or lambda remaining: self._hover(path, content, line, character, timeout=remaining).
  • On a scratch copy, the fold behaved identically across 11 scenarios: success, poison on failure, refusal when poisoned, busy before and after admission, Latin-1, KeyboardInterrupt, and a queued waiter.
  • This PR added the poison lines to both copies, and issue 4 shows that a one-sided edit would go unnoticed.
• servers/lean_runtime.py:738-753 and :762-777 (about 12 lines).
  • The lease/route/retire block has the same duplication: this PR and f793cae both edited the two copies in lockstep.
  • Add _lsp_operation(self, root, operation), which runs operation(session) under the lease with the routing. Each call site becomes one line.
  • Callable, T and LeanLspSession are already imported.
  • The lease is still released before formatting, and invalidate still runs before abort.

Open design questions (unchanged since ee352e5; for a maintainer)

1. Cleanup retries forever (server.py:113-126).
   • If a process group can't be killed, abort and close never return. Runtime shutdown and the next start, which waits on the lifetime flock (lean_client.py:303), then hang silently.
   • Options: bound cleanup with a background reaper that keeps the slot and the flock, or document the hang in servers/README.md.
2. LRU eviction can stall an unrelated project (lean_runtime.py:514-523, :544-546).
   • Eviction closes synchronously inside B's _acquire, so B inherits A's unbounded cleanup.
   • At minimum, reword lean_runtime.py:69-71: LSP_CLOSE_BUDGET bounds only the graceful attempt.
3. Budget exhaustion is the normal exit for slow files (server.py:207-222, :495-500).
   • A file that keeps Lean busy until lsp_timeout poisons the session on the success path, so the next call re-imports Mathlib.
   • Options: reserve a slice of the budget for didClose, or document the restart.
4. Callers already admitted to a poisoned session fail (server.py:162-163, :235-236). They could instead retry once on a fresh lease when the budget allows.

Low notes

• lean_runtime.py:750-751 and :774-775. invalidate() re-resolves the project root. If the directory vanished mid-call, it raises and abort() never runs, so the poisoned session stays cached as valid until eviction. Fix: try: invalidate(...) / finally: session.abort().
• Reaping race (server.py:116-118, :151). The PR body already flags it: poll() in is_alive() and wait() in close() can reap the leader before the group is signalled. psutil, already a dependency, can detect a zombie without reaping it.
• tests/test_shared_lean_runtime.py:848-914 is listed as LSP coverage, but it isn't. The PR body counts it, yet it stubs Services.close, never builds a LeanLspSession, and pins unchanged serve() behaviour; it passes on main.
• Timing-sensitive checks in the concurrency tests.
  • tests/test_lsp_protocol.py:297-298 and tests/test_shared_lean_runtime.py:824-826 rely on 0.1-0.2s joins.
  • assert release_cleanup.wait(timeout=2) at tests/test_shared_lean_runtime.py:799 runs inside the retried stub. A timeout there is swallowed and retried, not reported.
  • os.killpg at tests/test_lsp_protocol.py:337 runs after the leader was reaped, so it can hit a reused PGID.

Not verified

• Local test runs: the machine's load is about 330. CI at 58ff1a2 is green on all nine checks.
• The merge with Keep shared runtime status observational #112 after the issue 1 change. The current head merges cleanly with Keep shared runtime status observational #112 (git merge-file), including Keep shared runtime status observational #112 deleting its three dead assert ... is not None lines.

Spot-checked at 58ff1a2: issues 1 and 2 (server.py:226-230 and :487-490, lean_runtime.py:746-752 and :770-776, and the exception type of the int-limit error on Python 3.12).

Posted by PR swarm: PR Swarm Lead

[Deicyde]

Implemented the exact-head “fix first (small)” follow-up and merged current main (including #112) into this branch.

Production changes:

• unreadable/deleted hover input now leaves a healthy or concurrently active LSP session alone;
• runtime routing decides retirement from session.is_alive() rather than broad exception classes;
• every JSON decoder ValueError becomes LspProtocolError, including Python's oversized-integer failure;
• diagnostics and hover share one admission/poison helper; their runtime lease/retire routing is also shared.

New regressions cover PermissionError during concurrent diagnostics, hover queue/budget exhaustion, both operations staying healthy on admission failure, a 5,000-digit JSON integer frame, and faithful poisoning in the cleanup-order test.

Validation on the merged head:

• make lint: pass
• complete tests/test_lsp_protocol.py plus shared-runtime tests excluding the six host-load-sensitive daemon boot cases: 61 passed, 6 deselected
• focused changed regressions: 12 passed
• diff check: clean

One separate merge blocker remains. The generic ProjectResourceCache on both main and this branch removes idle/LRU victims from _entries before close_resource finishes. A same-project lease can therefore create generation 2 while generation 1 cleanup is still blocked. Exact controlled reproduction reports overlap=True replacement=2 generations=2. #111 makes that pre-existing window potentially unbounded because LSP group retirement retries until verified.

That prerequisite belongs under #109 as a focused cache-retirement change: keep a per-root retiring reservation through verified cleanup, count it against capacity, and make same-root acquisition wait/fail rather than invoke the factory. Until it lands, #111 should remain draft and should not close #108. The small fixes above are orthogonal and can stay on this branch.

[Deicyde]

Restacked at 2ce7ecb4 on #168 (953ff2f7) without force-pushing. The restack merge is tree-identical to #168; the final PR delta is only +119/-58: JSON ValueError normalization plus server/runtime helper consolidation and focused regressions. Full suite: 1,870 passed, 6 skipped, 1 expected failure. Exact-head CI is running.

[Deicyde]

Final exact-head status at 2ce7ecb4: all 9 checks pass and GitHub reports the stack mergeable. The final delta over #168 is +119/-58; full suite 1,870 passed, 6 skipped, 1 expected failure; two independent reviews plus repeated queued-call races found no blocker. Ready for human review after #168.

[Deicyde]

Review at 2ce7ecb

Verdict: merge-ready once #168 lands. Against its base (#168 at 953ff2f7), this PR does three things: it folds the duplicated admission blocks into LeanLspSession._admitted, folds the duplicated runtime lease/retire blocks into LeanRuntimeServices._lsp_operation, and widens the JSON-body except in _read_message to ValueError. I compared both folds line by line with the base and found no behaviour change: the order is the same (hover input is read before admission, and the deadline is computed after it), so are the exception types and messages, the budget arithmetic, and the lease_resolved/invalidate_resolved/retire sequence. tests/test_lsp_protocol.py passes at the head (30 passed). The 5,000-digit integer test fails when the except is reverted to the base's tuple, and the post-admission budget test fails if the inner try is moved above the remaining check. The only thing left is a nit.

Nits

• servers/lsp/server.py:547: except ValueError still lets one decoder failure through. A deeply nested body raises RecursionError: 200,000 [ followed by 200,000 ] is 400 KB, well under MAX_LSP_MESSAGE_BYTES, and CPython 3.13 raises RecursionError: maximum recursion depth exceeded while decoding a JSON array. The session is still retired correctly, because _admitted (:235-236) marks it on any BaseException and _lsp_operation routes by is_alive(). The client then sees RecursionError rather than LspProtocolError: LSP emitted an invalid JSON body. If the goal is one protocol error for every malformed body, catch (ValueError, RecursionError).

Earlier reviews

Status at this head of the findings from earlier swarm reviews: the posted 10-06 review (58ff1a2) and earlier unposted notes at ee352e5. After the restack, most of that code lives in #168, which is reviewed separately.

• Latin-1 hover kills the shared session (ee352e5 Add Aristotle (Harmonic) inference backend #1): fixed. Hover reads before admission (server.py:297-298), and test_hover_input_decode_failure_keeps_healthy_session pins it.
• An unreadable hover file kills the session under another caller's request (58ff1a2 Add Aristotle (Harmonic) inference backend #1): fixed by Retain Lean project ownership through verified cleanup #168. The runtime now retires only when not session.is_alive() (lean_runtime.py:978-982), and a pre-admission OSError leaves the session alive. test_hover_input_os_error_does_not_retire_healthy_session (tests/test_shared_lean_runtime.py:1751) pins it.
• 5,000-digit JSON integer escapes as a plain ValueError (58ff1a2 Revert #1 — Port aristotle backend #2): fixed here (server.py:547, test at tests/test_lsp_protocol.py:701). The routing half no longer matters, since retirement no longer depends on the exception type.
• An oversized input file retires a healthy session (58ff1a2 autoform-bot v2 (formalization pipeline — plan → prove → verify → review) #3, pre-existing on main): still open. _write_message raises LspProtocolError before writing anything (server.py:398-401) inside _admitted, which sets _retire_pending, and _lsp_operation then retires the session. It takes a file whose didOpen JSON exceeds 16 MiB. Neither this PR nor Retain Lean project ownership through verified cleanup #168 changes it; a follow-up is fine.
• Busy-session test covered only diagnostics (58ff1a2 Codex/refine roadmap review skills #4): partly addressed. test_post_admission_budget_exhaustion_keeps_session_healthy (tests/test_lsp_protocol.py:344) covers both methods on a real LeanLspSession. The runtime-level busy tests from bb50482 were dropped in the restack. Now that both methods share _lsp_operation, the hover input-error test above covers that routing, so nothing is lost.
• Golf: fold _admitted and _lsp_operation: done; that is this PR.
• Golf: use _remaining for the didClose budget checks (done in 58ff1a2): lost in the restack. Both didClose blocks are back to the inline three-line check (server.py:281-284, :343-346). That code is Retain Lean project ownership through verified cleanup #168's, so it's optional and belongs there.
• invalidate() re-resolves a vanished root and skips abort() (58ff1a2 low note): fixed by Retain Lean project ownership through verified cleanup #168's invalidate_resolved, pinned by test_failed_lsp_invalidation_survives_project_deletion.
• Open design questions (unbounded cleanup, LRU eviction stalling another project, budget exhaustion poisoning slow files, queued callers failing): Retain Lean project ownership through verified cleanup #168 moved cleanup onto cache reapers, so request threads no longer run it. Poisoning on an exhausted didClose budget stays as designed, and test_document_close_budget_exhaustion_retires_session pins it.

Landing

• Depends on Retain Lean project ownership through verified cleanup #168 and nothing else. _lsp_operation calls Retain Lean project ownership through verified cleanup #168's lease_resolved, invalidate_resolved, LeanLspSession.retire() and is_alive(), so if Retain Lean project ownership through verified cleanup #168's pending review renames or changes those, this PR must follow. No other line here depends on Retain Lean project ownership through verified cleanup #168's internals.
• Merge order, as the PR body says: merge-commit Retain Lean project ownership through verified cleanup #168, retarget this PR to main, check that the diff is still +119/-58, then squash-merge. Squash matters: the restack merge 8d74b484 carries the superseded pre-restack history (ee352e59, 2fc66f47, ...) as its second parent.
• Exact-head CI: all 9 checks pass. git merge-tree --write-tree 89dff279 2ce7ecb4 is clean. Main moved 65 commits past Retain Lean project ownership through verified cleanup #168's base 7fa6d1d6, none of them in servers/, tests/test_lsp_protocol.py or tests/test_shared_lean_runtime.py.
• Isolate and validate public REPL calls #105 is stacked on this branch. Report a non-UTF-8 Lean runtime reply as a protocol error and simplify request phases #175 (servers/lean_client.py, tests/test_shared_lean_runtime.py) merges cleanly with this head. No other open PR touches these three files.

Posted by PR swarm: Review #111 #105

[Deicyde]

Fixed the review nit in 0f789c28. _read_message now catches (ValueError, RecursionError) around the JSON body decode, so a body nested past the decoder's recursion limit reports LspProtocolError: LSP emitted an invalid JSON body instead of a raw RecursionError. Session retirement already handled that case; only the error the caller sees changes.
test_lsp_json_nesting_limit_is_reported_as_a_protocol_error, next to the 5,000-digit integer test, reads 200,000 nested arrays (400 KB, far under MAX_LSP_MESSAGE_BYTES) from a file, since a pipe cannot buffer the whole frame. With the previous except ValueError it fails with the raw RecursionError. That depth is past the decoder's limit on both CI versions (about 1,000 levels on 3.10, 10,000 on 3.13); a standalone json.loads of the same body raises RecursionError on 3.10 through 3.13 and on 3.15b3.
tests/test_lsp_protocol.py: 31 passed on Python 3.13. ruff check autoform_cli servers tests and git diff --check are clean. The PR body now lists the new case, and the diff against #168 is +133/−58.
Exact-head CI at 0f789c28: all 9 checks pass (real Lean, Python 3.10 and 3.13, Windows).
Posted by PR swarm: Swarm Manager

[Deicyde]

Merge status at fd9197f2

• Contents: merges Retain Lean project ownership through verified cleanup #168's final-review fixes (76f58167) without conflicts. Normalize and consolidate shared LSP calls #111's own diff on top of Retain Lean project ownership through verified cleanup #168 is unchanged in scope: +133/−58 in servers/lean_runtime.py, servers/lsp/server.py and tests/test_lsp_protocol.py.
• CI: all 9 check runs at this commit pass, in both the push and pull-request runs, including real Lean. The earlier real-Lean failure on 869e0afd came from a test that went through get_diagnostics. That test now opens its file directly, and the underlying bug is lsp: a frame straddling the quiet-read window fails get_diagnostics and kills the session #238.
• Against its base: mergeable into fix/retained-project-cleanup; GitHub reports CLEAN.
• Blocked on Retain Lean project ownership through verified cleanup #168: merge Retain Lean project ownership through verified cleanup #168 into main first. Then retarget this PR to main, check that the diff is only Normalize and consolidate shared LSP calls #111's own change, and rerun CI.
• Downstream: Isolate and validate public REPL calls #105 is stacked on this branch. Updating Isolate and validate public REPL calls #105 from here conflicts in one place: tests/test_shared_lean_runtime.py, where Isolate and validate public REPL calls #105 replaces test_partial_repl_startup_transfers_cleanup_without_masking_the_error. Take Isolate and validate public REPL calls #105's side.

[Deicyde]

Status at fd9197f2: blocked on #168, otherwise ready

• Contents: #111's own change on top of #168 is +133/−58: the _admitted and _lsp_operation folds, plus the JSON body decode hardening. It also carries #168's final-review fixes, brought in by the clean merge fd9197f2.
• Review: the swarm reviewed it at 2ce7ecb4 ("merge-ready once #168 lands") and found one nit, fixed in 0f789c28. Since then the only changes are the two merges of #168's fixes (869e0afd, fd9197f2), both without conflicts.
• CI: all 9 check runs at this commit pass, including real Lean. The earlier real-Lean failure on 869e0afd was a flake in a test that no longer calls get_diagnostics; the root cause is #238.
• Mergeable: GitHub reports CLEAN against the base fix/retained-project-cleanup. A simulation of the full order (merge #168 into current main 2825e93b, then this PR) also produces no conflicts.
• To merge: once #168 lands, retarget this PR to main. Check that the diff shows only #111's own +133/−58, rerun CI, then squash-merge. Squash matters because the restack merge 8d74b484 brings superseded pre-restack history in as its second parent.
• Downstream #105: GitHub now marks #105 as conflicting with this branch. The only conflict is in tests/test_shared_lean_runtime.py, where #105 replaces test_partial_repl_startup_transfers_cleanup_without_masking_the_error. Take #105's side when you next update it from this branch.