Keep shared runtime status observational

[Deicyde]

Part of #109.

Problem

repl.status read the pool through the normal lease(create=False) path. That path fingerprints the project and calls is_valid, can retire an idle stale or invalid pool, and refreshes last_used on release. A status probe could therefore close a quarantined pool or keep an idle project resident past its TTL. When no pool was found, a second state() lookup could also disagree with the first.

Fix

ProjectResourceCache.observe() takes one (resource, state) snapshot under the cache condition. For a resident entry it pins it (active += 1) while status fields are read, then unpins without touching last_used. It never fingerprints, validates, creates, retires, replaces, or waits for a warming entry, and it raises on a closed cache as lease does. repl.status uses it. That leaves state() and lease(create=False) without callers, so both are removed: lease() now always yields a resource. Execution leases and the REPL/LSP protocols are otherwise unchanged.

Invariant

Status observation has no lifecycle side effects. It reports the state that exists, including invalid, stale, or shut-down pools. Its pin still keeps idle eviction, stale replacement, and cache close from closing a pool mid-read.

Tests

In tests/test_shared_lean_runtime.py, cache level: no fingerprinting or validation and no repair of an invalid or stale entry (through a symlinked alias); no TTL refresh, with the pin blocking idle eviction; close waiting on a pin; invalid-pool replacement waiting on a pin; closed and warming states without creating or waiting; a startup that misses its budget leaves the project observably cold. Service level: cold repl.status creates no pool; repl.status reports a stale shut-down pool without replacing it; an exception while reading a pool field releases the pin without refreshing the TTL.

[Deicyde]

Exact-head verification is complete at 5977979f. Both Python 3.10/3.13 jobs, both real-Lean jobs, Windows hardening, and CLA are green. Local full suite: 1,069 passed, 1 skipped; focused shared-runtime suite: 39 passed; consumer example and strict MkDocs build pass. Independent review verified atomic status/state snapshots, no validity/factory/cleanup/TTL side effects, active ownership under cancellation, stale/shutdown visibility, and concurrent eviction/close/replacement behavior, and reports SHIP. No known merge blocker remains.

[Deicyde]

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

What changed and why

• Dropped the "no longer registered" check when an observation unpins. A pinned entry is never evicted, replaced, or closed (eviction and LRU only take inactive entries, stale replacement and close() wait for active ones), so the check could not fire. If it ever did, raising inside finally would mask the caller's own error.
• Dropped two cancellation tests that only repeated other coverage. test_cache_close_waits_for_an_active_observation pins close waiting on a pin, and the repl.status field-cancellation test pins release on an exception.
• No behaviour change. Status output (the JSON contract) is unchanged.

Diff vs base: 2 files, +425/-3 → 2 files, +356/-3.

Checks: exact-head CI green (test 3.10/3.13, real Lean, Windows hardening, CLA): https://github.com/facebookresearch/autoform-bot/actions/runs/37388275135 and https://github.com/facebookresearch/autoform-bot/actions/runs/37388279995. Locally: ruff clean, and every observation and status test in tests/test_shared_lean_runtime.py passes. The only local failures were the 6 daemon-boot tests, which hit their 15s readiness timeout at load average ~330; they don't touch this change and are green on CI.

Remaining risks

• While status reads pool fields the pool is pinned, so a hung get_memory_usage() would hold up cache close. main's lease-based status pinned the same way.
• ProjectResourceCache.state() no longer has a production caller (one existing test still uses it). I left it in place to keep the diff to this PR's hunks.
• Merges cleanly with Normalize and consolidate shared LSP calls #111 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 d9f85eae. observe() snapshots state under the cache condition, pins a resident resource before exposure, releases in finally without refreshing TTL, and composes with every eviction/replacement/close path that uses the same active counter. No production caller remains on lease(create=False) or state(). All nine GitHub checks pass, current main merges cleanly without touching the two PR files, and no correctness blocker remains.

[Deicyde]

Independent review of d9f85ea. An earlier swarm pass at a5a4ca0 found that this PR orphaned ProjectResourceCache.state(), and it suggested two golf items. 666cf7a, 781ea9b and d9f85ea respond to them. This pass verified those commits and then reviewed the full effective diff again.

Verdict: mergeable. Every earlier item is fixed, and nothing new blocks:

• one pre-existing race, low and fine as a follow-up;
• one pre-existing test gap;
• about 10 lines of golf that d9f85ea left behind.

The PR merges cleanly with #111 in either order.

Earlier findings

• state() had no production caller: fixed by 666cf7a.
  • observe() (lean_runtime.py:364-371) is now the only copy of the cold/warming/warm logic.
  • The startup-expiry test checks through observe() (tests/test_shared_lean_runtime.py:575-576), so it still verifies that the abandoned startup cleared _creating.
• Golf, drop the cold half of the observation test: done in 781ea9b.
• Golf, remove lease(create=False): done in d9f85ea.
  • lease() is now -> Iterator[T], and nothing in servers/, autoform_cli/ or tests/ calls lease(create=...) or .state(.
  • Two leftovers are listed under Golf.
• The claims in the a5a4ca0 golf comment still hold:
  • the dropped "still registered" check is safe;
  • the dropped cancellation tests are covered;
  • status stays observational;
  • state() is gone.

Confirmed issues

1. servers/lean_runtime.py:508: _acquire can pop a stale resource and then raise before closing it (low, pre-existing).

• How it leaks.
  • The stale-idle branch moves the entry into the local resources_to_close (:490).
  • The second _require_creation_budget (:508-512) then reads the clock again. If the remaining budget has just dropped below creation_budget, it raises ProjectResourceBusyError.
  • The only closes are at :543-545 and :547-548, and the exception skips both.
  • The popped LeanReplPool or LeanLspSession is no longer in _entries, so neither close() nor evict_idle() can reach it.
• Cost. Its processes run until the daemon exits, and the freed slot lets the next call start a second pool for the same project, past the RAM-based worker budget.
• Severity: low. The window is the gap between two clock reads. It takes a waiter that wakes right at the threshold, typically after chained waits.
• Not a regression. The _acquire bodies at a5a4ca0 and main hash the same, and the race dates to 00a3cbd.
• Reproduction. On a scratch copy, with a clock that advances 1.0 per read, lease → invalidate → lease(acquisition_timeout=6.0, creation_budget=5.0) raises "not enough response budget" with closed == [] and nothing resident. Main gives the same result.
• Fix. Check the budget once per iteration, before anything is mutated.
  • Put if entry_is_stale or (entry is None and root not in self._creating): self._require_creation_budget(...) above the stale branch, and delete both current call sites (:482-486, :508-512). That saves about 4 lines.
  • In the scratch harness this changed only the two leak scenarios, which now close the stale resource and create its replacement. The other 14 scenarios were identical.
  • The alternative is try/finally around the loop, always closing resources_to_close.

2. servers/lean_runtime.py:482-486: no test exercises the stale-entry budget check (low, pre-existing test gap).

• Why it matters. After d9f85ea the two _require_creation_budget calls are byte-identical, 22 lines apart, which invites deleting the first as a duplicate.
• What deleting it does.
  • Every stale-idle call with a short budget would pop the entry and raise at :508, leaking one pool or session per call.
  • A stale-but-active caller would wait out its deadline instead of failing on the budget.
  • The suite would still pass.
• Can it happen in practice? Yes, with valid settings: with AUTOFORM_REPL_WORKERS_PER_PROJECT=3, a timeout=240 call has 26 s of slack. The only deadline tests (tests/test_shared_lean_runtime.py:536-539, :567-570) have no stale entry.
• Fix. Add a cache-level test next to :521.
  • Lease once, call invalidate, then expect lease(acquisition_timeout=0.05, creation_budget=1.0) to raise ProjectResourceBusyError(match="not enough response budget").
  • Assert the invalid entry is still in stats()["resident"].
  • Add a variant that holds the first lease open (stale and active) and expects the same message, not "timed out waiting".
  • This pins issue 1's fix too.

Golf (about 10 lines)

• servers/lean_runtime.py:460, :499-502, :526-531, :550-552 (7 lines). The reserved flag and the resource = None sentinel are leftovers from the create=False exits d9f85ea removed.
  • Replace resource = entry.resource / break with return entry.resource. The with block releases the lock, and resources_to_close is always empty on that path.
  • Then delete reserved, resource = None and if not reserved: return resource.
  • This also removes a None store in a -> T function.
  • A scratch harness found 0 behaviour differences across 27 scenarios, and the lock was never left held.
• servers/lean_runtime.py:713, :741, :764 (3 lines). The assert pool is not None and assert session is not None lines narrow a type lease() can no longer return.
  • The PR keeps the LSP pair to stay clear of Normalize and consolidate shared LSP calls #111's hunks, but two unchanged lines separate them from Normalize and consolidate shared LSP calls #111's edits.
  • Deleting all three merges cleanly with Normalize and consolidate shared LSP calls #111 at 58ff1a2 and with Isolate and validate public REPL calls #105's REPL stack (checked with git merge-file).
  • Keep assert entry is not None at :481, which still narrows self._entries.get(root).

Low notes

• lean_runtime.py:379: nothing pins the notify_all() in observe()'s release.
  • Deleting it passes the suite, because close() and _acquire both re-poll every 0.5 s (:432, :533). The worst case is 0.5 s of extra latency, not a hang.
  • To pin it: in the tests at :221 and :256, swap cache._condition for a subclass whose wait(timeout=None) ignores the timeout.
• The pin-blocks-close and pin-blocks-replacement tests (tests/test_shared_lean_runtime.py:247, :300) are probabilistic.
  • They tell correct code from a mutant only through a 0.1 s negative wait.
  • A close() that ignores active (:431), or a stale replacement that ignores entry.active (:487), survives if the worker thread is starved.
  • A fully no-op pin is caught deterministically elsewhere (:179, :209-211, :425).
  • Barrier fix for the close test: retry observe() until it raises "cache is closed", then assert the entry is still resident and closed == [].

Not verified

• Local test runs: the machine's load is about 330. CI at d9f85ea is green on all nine checks.

Spot-checked at d9f85ea: issue 1 and both golf items (lean_runtime.py:456-552, and the asserts at :713, :741, :764).

Posted by PR swarm: PR Swarm Lead