Stop worker groups that Lean's watchdog leaves running at LSP close

[Deicyde]

Closes #251.

Problem

Lean's watchdog (Watchdog.lean, Lean v4.32.2) starts each file worker
with setsid. On stdin EOF or a shutdown request it sends every worker
an exit notification and then calls killProcAndWait on each in URI
order, which terminates a worker's process group only if the watchdog
has not yet seen that worker exit. A worker that exits on its exit
notification while an earlier one is being killed is skipped; its group
is then terminated only by the fallback in forwardMessages, which
races with the watchdog's own exit. When the fallback loses, the
worker's lake setup-file and its lean ... -o child keep running
after close() returns. Workers are also left running when the EOF
grace (LSP_EOF_GRACE_SECONDS) ends while the watchdog is still
stopping them: the group signal then kills the watchdog before it
reaches them.

On main the server never holds two documents open: _hover is the only
caller of _open_document, and a session that may still hold its
document admits no further operation. So this is hardening: close()
stops the worker groups the watchdog leaves behind, however many
documents are open.

Change

LeanLspSession records the process groups of its descendants outside
its own group while the watchdog still parents them: in _retire_once
before it closes Lean's pipes, and in close() before the shutdown
request. It scans every member of the server's group, so it still finds
lean --server after lake serve has died. After the server group is
retired, and before its leader is reaped, _stop_worker_groups
terminates each recorded group that still holds a recorded process
(os.getpgid, then psutil's PID and creation-time check), so a group
whose ID was reused is not signalled. A failed termination keeps the
groups recorded for _abort_process's retry.

Not covered: processes already orphaned when close starts. If
lean --server dies first, its workers are reparented and there is
nothing left to record.

Tests

• test_close_stops_a_worker_group_the_watchdog_left_running (abort
  and graceful) and
  test_close_stops_a_worker_group_left_running_after_the_wrapper_crashed:
  a fake watchdog, run directly or under a wrapper that has already
  exited, leaves a worker's build running and exits; close must stop the
  build. Each fails without the recording on its path.
• test_abort_never_signals_a_worker_group_whose_recorded_members_are_gone
  (exited and left-the-group): a live group under a recorded group ID is
  not signalled once its recorded process has exited or moved to another
  group.
• test_abort_retries_a_failed_worker_group_before_reaping_the_leader:
  a failed worker-group termination is retried before the leader is
  reaped.
• The two older fake-watchdog tests turn the recording off, so they
  still fail if the group is signalled before EOF or if stdout stays
  open.
• test_real_lean_abort_stops_the_workers_of_every_open_file: real
  Lean with two open files, the second building a slow import, then an
  abort; nothing may outlive it. Whether Lean skips the second worker is
  a race, so this test can pass without the change. CI's real-Lean job
  selects it with -k real_lean.

ruff check autoform_cli servers tests passes, and the tests above
other than the real-Lean one pass locally.

[Deicyde]

Review at 532458a

Verdict: Request changes. This makes LeanLspSession record the process groups of the Lean server's descendants before EOF and before the shutdown request, then terminate any recorded group that still holds a recorded process, so a worker's build that Lean's watchdog skips at shutdown no longer outlives close(). On main the server never holds two documents open, so this is hardening, as the description says; the code does what it claims, and the identity check never signals a group that only reuses a recorded PID. One gap blocks merge: the worker-group retry and leader-last ordering the description promises have no test. Which mechanism to keep, and with it whether this closes #251, is your call (below).

Fixes before merge

1. Pin the worker-group retry and leader-last ordering (servers/lsp/server.py:215, servers/lsp/server.py:242-244). The description says a failed termination keeps the group recorded and the leader stays unreaped until every recorded group is retired, but no test reaches that path: the new unit test (tests/test_lsp_protocol.py:439) records no running member, and the fake-watchdog tests only cover success. By trace, two edits pass every test: deleting the record before terminating (as the natural golf members = self._worker_groups.pop(process_group_id) would), which drops the group after a failure, and moving self._stop_worker_groups() below self.process = None, which ends _abort_process's retries with the group still running. Fix: add a unit test beside tests/test_lsp_protocol.py:220-276 that stubs _descendant_process_groups to return one start_new_session sleeper, fails _terminate_process_group once for its group, records the terminations seen when _reap_process runs, and asserts [server, worker, worker]. That test passes at this head and fails on both edits. Keep the retry itself; it matches the cleanup policy in servers/README.md:108-110.

Optional

• tests/test_lsp_protocol.py:827: say why the file names matter. The watchdog kills workers in URI order (fileWorkersRef is a Std.TreeMap) and skips a worker that has already exited by its turn, so the test relies on Second.lean sorting after Main.lean; a module that sorts first, such as Aux, would likely pass without the fix.
• tests/test_lsp_protocol.py:714-730 repeats the setup at tests/test_lsp_protocol.py:615-631; a _start_crashed_wrapper(watchdog) helper used by both tests is about 10 lines shorter and lint clean.
• Trim the description: the reachability argument fits in two sentences, and the Landing list of merge results against other open PRs goes stale with each merge.

Landing

• Merges cleanly into main at 09cb009; since the base only Delete the unused project routers and resident-era REPL pool code #316 changed servers/, without conflict. No other open PR in this batch, Let work and search omit what they can't represent, and have check warn #325 included, touches servers/lsp/ or tests/test_lsp_protocol.py, and Let work and search omit what they can't represent, and have check warn #325's principle (tools inform and must not break a codebase) does not bear on this: no CLI or JSON contract changes.

Decision for the maintainer

• Which mechanism should handle LSP close can leave Lean worker processes running when several files are open #251? The group recording covers workers still running at close, but not workers orphaned before close starts: when lean --server dies first, nothing is left to record, as the description says, and LSP close can leave Lean worker processes running when several files are open #251 reports that this case leaks every time. The repository already tracks descendants that escape both the parent and the process group another way: autoform_cli/skeleton.py:1137-1139 puts a random token in the child's environment and autoform_cli/skeleton.py:894-927 finds every process that carries it. Lean v4.32.2 never overrides inheritEnv := true (src/Init/System/IO.lean:1450), so such a token reaches lean --server, every --worker, lake setup-file and lean -o, orphaned or not, and psutil rechecks process identity right before each kill.
• Options: (a) keep the group recording, change "Closes LSP close can leave Lean worker processes running when several files are open #251" to "Part of LSP close can leave Lean worker processes running when several files are open #251", and open an issue for workers orphaned before close. (b) Tag the session instead: set the token in start(), and where _stop_worker_groups() runs now, kill every live process carrying it and fail the attempt while any remain. (b) replaces the two recording points with one sweep, drops _still_in_process_group and its PID-reuse test, and makes "Closes LSP close can leave Lean worker processes running when several files are open #251" accurate.
• Recommendation: (b), with fix 1's test pinning the same retry and leader-last ordering for the sweep.

This PR came from the same PR swarm that reviewed it, so this is the author's review, not an independent one. The test suite was not run locally; fix 1's proposed test was run directly against this branch's code. CI at this head: all 11 checks pass, including the real-Lean jobs.

Posted by PR swarm: PR Swarm Lead

[Deicyde]

Review changes addressed at b0cf364

• Rebased onto main at feec945, which includes Let work and search omit what they can't represent, and have check warn #325. Let work and search omit what they can't represent, and have check warn #325 touches no file this branch changes, and the branch merges cleanly.
• Added test_abort_retries_a_failed_worker_group_before_reaping_the_leader. It makes the first termination of a recorded worker group fail, then checks that the retry terminates that group again before the leader is reaped.
• That test fails if a group's record is dropped before its termination succeeds, or if the worker groups are stopped only after the session has given up the process. No production code changed.
• The commit message and the description's Tests and Landing sections are updated to match.

Still open for you: keep the process-group recording ("Part of #251"), or tag the session's processes with an environment token and sweep them, which also covers workers orphaned before close and would close #251.

CI is running on this head.

Posted by PR swarm: PR Swarm Lead

[Deicyde]

Follow-up review at 7cf7735

Verdict: Ready to merge. This pass checked each applied fix and the one rejected suggestion against the diff, re-read the Lean v4.32.2 watchdog code the description cites, and went over the whole change again. It merges cleanly into current main (d1ad2fb), and no commit on main since the first review touches servers/lsp/, its tests, or the process helpers it calls. The production change is small, each guard has a test that fails without it, and nothing blocks merging this mechanism; whether to keep it is your call (below).

Changed in this pass

• Description trimmed: the stale base pins and the open-PR merge list are gone, reachability is two sentences, and it now names the second leak, where the EOF grace ends while the watchdog is still stopping workers.
• servers/lsp/server.py:236-243: _stop_worker_groups iterates the record directly and clears it once at the end; a failed termination still keeps every group for the retry.
• tests/test_lsp_protocol.py:468-492: the reuse test also covers a recorded process that is alive but has left the group, which pins the os.getpgid half of servers/lsp/server.py:94-103.
• tests/test_lsp_protocol.py:279-306: the retry test stubs the identity check instead of spawning a process; it still fails if a record is dropped before its termination succeeds or if the groups are stopped after the leader is reaped.
• tests/test_lsp_protocol.py:616-635: _start_crashing_wrapper replaces two copies of the crashed-wrapper setup.
• tests/test_lsp_protocol.py:848-853: the two-file real-Lean test says why Second.lean must sort after Main.lean, and that it can pass without the fix because the skip is a race.
• Commit message rewritten to match. A worker process is still recorded once per server-group ancestor; any() makes the repeats harmless, so that stays.

Decision for the maintainer

• Which mechanism handles LSP close can leave Lean worker processes running when several files are open #251: this recording misses workers orphaned before close starts (when lean --server dies first), the case LSP close can leave Lean worker processes running when several files are open #251 reports as leaking every time, while an environment-token sweep like autoform_cli/skeleton.py:90 and autoform_cli/skeleton.py:918 would cover it. Recommendation, as before: the sweep. If you keep this mechanism, merge it with "Part of LSP close can leave Lean worker processes running when several files are open #251" in place of "Closes LSP close can leave Lean worker processes running when several files are open #251" and track the orphaned case in its own issue.

This PR came from the same PR swarm that reviewed it, so this is the author's review, not an independent one. pytest was not run at this head because the machine was overloaded; the changed tests and the lifecycle tests around them were called directly and pass, and the reuse and crashed-wrapper tests fail when the identity check, the running check, or the whole-group scan is removed. The real-Lean test runs only in CI. CI at this head: all 7 checks pass, including the real-Lean jobs.

Posted by PR swarm: PR Swarm Lead