[Deicyde]

Follow-up to #251 and #322.

Problem

#322 records the process groups of lean --server's descendants before EOF and before the shutdown request, then terminates the recorded groups that still hold a recorded process. Recording needs a live server. When lean --server dies before close starts, its file workers are reparented and nothing ties them to the session, so the workers, their lake setup-file and its lean ... -o keep running after close() returns. #251 saw that case leak every time, and #322 left it uncovered. #322's review recommended tagging the session's processes with an environment token instead, and the maintainer chose that mechanism.

Change

servers/lsp/server.py:

• start() puts a random token (secrets.token_hex(16)) in the server's environment as _AUTOFORM_LSP_SESSION_TOKEN. The runtime's own environment is untouched, so its REPL and diagnostics children never carry it. Lean v4.32.2 starts each file worker and lake setup-file with the default inheritEnv := true (SpawnArgs in src/Init/System/IO.lean; nothing in Lean or Lake sets it to false), and lake serve starts lean --server with env := extraEnv, which sets only a fixed list of Elan, Lake and Lean variables and search paths. So every process the server starts carries the token, in any process group, orphaned or not.
• Where _stop_worker_groups ran, after the server's own group is retired and before its leader is reaped, _stop_processes_with_token sends SIGTERM to every live process whose environment carries the token, then SIGKILL to those a new scan still finds, with the same waits as the group termination (0.5 s, then 1 s), and raises while a final scan finds any. close() and abort() retry it before the leader is reaped, as they retried a failed worker group, and the retry does not signal the retired group again.
• Identity: the scan creates each psutil handle before it reads that process's environment, and every signal goes through the handle, which checks the PID's creation time first. A process that took over a PID after the scan is spared, and the SIGKILL round signals only what its own scan found. A process that takes over a PID is reported only if it carries the token itself.
• When an environment cannot be read (psutil AccessDenied), that process is never signalled, since nothing shows that it belongs to the session, and it does not hold up the close either. Setuid programs a user runs, such as login on macOS, are unreadable to that user for as long as they run, so waiting for unreadable processes would make every close retry forever; Lean and Lake run as the user, so their environments can be read. If the process table cannot be read, or reading an environment fails in any other way, the attempt fails and close or abort retries. Exited processes and zombies count as gone. A process started without the variable is not found (unsetting it in a running process does not hide that process), and the README says so.
• The scan refuses a missing token, since every process without the variable would match it.
• Removed with the recording: _descendant_process_groups, _still_in_process_group, _record_worker_groups, _stop_worker_groups, _worker_groups, and the recording call before the shutdown request.

Helper: a minimal scan beside the LSP code, rather than autoform_cli/skeleton.py's _remember_tagged_processes or a shared module. Nothing in servers/ imports autoform_cli. The wheel ships both packages, so the import would resolve, but the runtime's code fingerprint (_RUNTIME_SOURCES in servers/lean_client.py) covers only servers/ files, so a cleanup helper in autoform_cli could change without replacing a live runtime. The skeleton helper also passes over processes it cannot read, raises SkeletonError, and would load the skeleton module and its imports into the runtime. A shared module would mean reworking the skeleton's cleanup, which this change does not need. The variable is distinct from the skeleton's _AUTOFORM_PROCESS_TOKEN.

servers/README.md gets a paragraph, after the one on stop, on what closing a project's Lean server stops, including any daemon a tagged process started, and on what the sweep cannot see.

Tests

tests/test_lsp_protocol.py:

• New test_close_stops_workers_orphaned_before_close: a fake server under a wrapper that has already exited starts a worker in its own session, and the worker starts a build that ignores SIGTERM, so only the SIGKILL round can stop it. The test kills the server, checks that both are still running, and closes the session. Against main's servers/lsp/server.py it fails with the worker still running.
• New test_real_lean_close_stops_workers_orphaned_before_close: real Lean opens a file whose import blocks in #eval IO.sleep; the test kills lean --server, checks that the Slow.lean build is still running, then retires and closes the session. Nothing it recorded may outlive the close. CI's real-Lean job selects it with -k real_lean.
• test_close_stops_a_build_the_watchdog_left_running (abort and graceful) and test_close_stops_a_build_left_running_after_the_wrapper_crashed are Stop worker groups that Lean's watchdog leaves running at LSP close #322's skipping-watchdog tests, now with the session's token in the fake processes' environment.
• test_abort_lets_the_watchdog_stop_workers_outside_the_group and test_abort_after_the_wrapper_crashed_still_reaches_the_watchdog run with no token, so only the watchdog can stop the worker, as when Stop worker groups that Lean's watchdog leaves running at LSP close #322 turned the recording off in them.
• test_abort_retries_the_token_sweep_before_reaping_the_leader replaces the worker-group retry test. It records every group termination, scan, signal and reap in order: the scan after SIGKILL still finds a process and fails the attempt, the retry does not signal the retired group, and the leader is reaped only after a sweep finds nothing.
• Replacing the PID-reuse test: test_token_sweep_signals_only_what_its_latest_scan_found; test_token_scan_finds_only_the_processes_carrying_the_token, on real processes carrying this token, another session's token, and none; test_token_scan_leaves_out_processes_it_cannot_read (unreadable, zombie, exited, and the runtime's own process); test_token_scan_fails_when_the_process_table_cannot_be_read; and test_token_scan_fails_on_any_other_environment_error (an OSError and a SystemError).
• New test_start_gives_each_server_its_own_token and test_token_scan_refuses_a_missing_token (None and the empty string).

What ran: uvx ruff@0.15.17 check autoform_cli servers tests passes. Load on the machine was too high for pytest, so a script called 25 cases from tests/test_lsp_protocol.py directly (every new and changed unit test, each parametrized case, and the lifecycle tests around them) and test_partial_lsp_startup_transfers_cleanup_without_masking_the_error from tests/test_shared_lean_runtime.py; all pass. The same script checked that a child which unsets the variable after it starts is still found and that one started without it is not. Mutants of servers/lsp/server.py fail the tests written for them: without the final scan, the retry test fails; with every environment error passed over, both cases of the error test fail; without the missing-token check, both of its cases fail. Against main's servers/lsp/server.py, the orphan test fails and the two skipping-watchdog tests it was compared with (the crashed-wrapper one and the abort case of the other) pass. The full suite and the real-Lean tests run only in CI.

Landing

• Settle the LSP follow-ups from #256 except dependencyBuildMode #354, the follow-ups to lsp: small follow-ups to #256 #271, changes _read_message's first branch, adds a test after test_json_rpc_error_response_raises_protocol_error, and rewrites the LEAN_LSP_TIMEOUT paragraph of servers/README.md. This PR touches none of those lines, and git merge-tree merges the two cleanly.
• Point run_lean_code at lean_diagnostic_messages for project code #356 edits the import-allowlist paragraph of servers/README.md; it also merges cleanly with this one.
• Main has moved since this branch's base (Bump mcp from 1.29.0 to 1.30.0 #353 and Check that a manifest's schema is a string before looking it up #357). Neither touches these files, and the branch merges cleanly with current main.
• No other open PR gets a new conflict: git merge-tree of each against this branch merged into main matches the same against main alone.

[Deicyde]

Review at 3a5c1d9

Verdict: Ready to merge. The token sweep replaces #322's recording at the same point in retirement, keeps the leader-last order and the retry, and stops workers orphaned before close, which main leaks. The review findings are applied: the retry test now fails without the final scan, the scan refuses a missing token, and the README says that a process started without the token is not found and that daemons a tagged process started are stopped.

Checked

• The token reaches every Lean descendant: Lean v4.32.2's SpawnArgs.inheritEnv defaults to true and nothing overrides it, and lake serve passes env := extraEnv, which sets only a fixed list of Elan, Lake and Lean variables and search paths.
• Order and retry: the sweep runs after the server's group is retired and before the leader is reaped. A failed sweep keeps ownership and never signals the retired group again, and close and abort serialize on the lifecycle lock.
• Identity: each psutil handle is created before that process's environment is read, and psutil checks the creation time before every signal, so a reused PID without the token is never signalled.
• Unreadable environments are never signalled and do not hold up the close, because same-user setuid programs are always unreadable. An unreadable process table or any other read error fails the attempt.
• The removed recording helpers have no references left. servers/ still imports nothing from autoform_cli, whose files the runtime fingerprint does not cover.
• Test teeth: the retry test records every scan, and mutants without the final scan, with every environment error skipped, or without the missing-token check each fail a test. The orphan test's build ignores SIGTERM, so only the SIGKILL round can stop it.
• Not changed here: a token carrier that cannot be killed makes close retry forever, as a stuck process group already does.

Landing

• Settle the LSP follow-ups from #256 except dependencyBuildMode #354, the follow-ups to lsp: small follow-ups to #256 #271, changes _read_message's first branch, one test and the LEAN_LSP_TIMEOUT paragraph. This PR touches none of those lines, and git merge-tree merges the two cleanly, so either can land first.
• Point run_lean_code at lean_diagnostic_messages for project code #356 edits the import-allowlist paragraph of servers/README.md and also merges cleanly.
• The branch merges cleanly with current main (Bump mcp from 1.29.0 to 1.30.0 #353 and Check that a manifest's schema is a string before looking it up #357 landed after its base; neither touches these files), and no other open PR gets a new conflict.

This PR came from the same PR swarm that reviewed it, so this is the author's review, not an independent one. Ruff passes. Load on the review machine was too high for pytest, so a script called 25 cases from tests/test_lsp_protocol.py and one from tests/test_shared_lean_runtime.py directly, and all pass; the orphan test fails against main. The full suite and the real-Lean test run only in CI. CI at this head: all 7 checks pass. The real-Lean LSP step passed all 8 of its tests, test_real_lean_close_stops_workers_orphaned_before_close among them.

Posted by PR swarm: PR Swarm Lead