Fix registered replay descendant cleanup on command exit

docs/research/research-package-guide.md

@@ -81,7 +81,15 @@ already trigger replay. Use canonical repository-relative POSIX paths, such as
 slashes or dot components. The planner rejects aliases because Git reports the
 canonical path when a dependency changes. The generic hook does not infer transitive imports.
 Each command has a maximum 600-second timeout and the package total is at most
-1200 seconds. A timeout fails and terminates the local process group. These
+1200 seconds. On POSIX, the launcher terminates the command's local process
+group on every exit, including success, failure, timeout and interruption, so
+background solver processes in that group cannot continue into another replay.
+Verification commands must wait for all proof-relevant children and propagate
+their failures before returning; cleanup is not evidence that unfinished checks
+passed. Descendants that deliberately detach into another group/session are
+outside this cleanup contract. On Windows, tree cleanup uses `taskkill` while
+the leader is still running; cleanup after leader exit needs a separate native
+lifetime mechanism and is not provided here. A timeout still fails. These
 bounds limit a verification job, not the mathematical search budget.
 
 The [registered-package workflow](../../.github/workflows/research-packages.yml)

scripts/research_package.py

@@ -215,18 +215,26 @@ def run_command(argv, cwd, timeout):
     # Keep explicit manifest options (including deliberate -O controls) intact.
     env = os.environ.copy()
     env.pop("PYTHONOPTIMIZE", None)
-    # A timeout ends the whole local process group, including child solvers.
+    # Own a group for POSIX cleanup of this command and its descendants.
     process = subprocess.Popen(argv, cwd=cwd, env=env, start_new_session=True)
     try:
-        code = process.wait(timeout=timeout)
-    except subprocess.TimeoutExpired:
+        try:
+            code = process.wait(timeout=timeout)
+        except subprocess.TimeoutExpired:
+            raise ValueError("verification timed out") from None
+        require(code == 0, f"verification command exited {code}")
+    finally:
         if hasattr(os, "killpg"):
-            os.killpg(process.pid, signal.SIGKILL)
-        else:  # Windows has no process groups to signal; end the whole child tree instead.
+            # The leader may have exited while descendants still hold the group.
+            # Signal it on success, failure and interruption, not only timeout.
+            try:
+                os.killpg(process.pid, signal.SIGKILL)
+            except ProcessLookupError:
+                pass  # A completely finished group needs no cleanup.
+        elif process.poll() is None:
+            # Windows taskkill can address the tree only while its leader exists.
             subprocess.run(["taskkill", "/F", "/T", "/PID", str(process.pid)], capture_output=True)
         process.wait()
-        raise ValueError("verification timed out")
-    require(code == 0, f"verification command exited {code}")
 
 
 def run_package(root, package, install=False):

tests/test_research_process_tree.py

@@ -1,6 +1,7 @@
 """Linux process-tree failure controls for bounded research-package replay.
 
 Paul Romeo, with substantial OpenAI Codex assistance. Apache-2.0.
+Leader-exit and interruption controls by yssite, with OpenAI Codex assistance.
 """
 import os
 from pathlib import Path
@@ -31,6 +32,10 @@
          if depth else None)
 if depth == 0:
     (root / "ready").touch()
+if len(sys.argv) == 4:
+    while not (root / "ready").exists():
+        time.sleep(0.01)
+    sys.exit(int(sys.argv[3]))
 deadline = time.monotonic() + 60
 while not (root / "release").exists() and time.monotonic() < deadline:
     time.sleep(0.01)
@@ -59,7 +64,7 @@ def alive(pid):
 
 @unittest.skipUnless(sys.platform == "linux", "requires Linux /proc process states")
 class ProcessTreeTests(unittest.TestCase):
-    def exercise_tree(self, complete=False):
+    def exercise_tree(self, complete=False, leader_exit=None, interrupt=False):
         process, owned_group, pids = None, False, []
         real_popen = subprocess.Popen
         with tempfile.TemporaryDirectory() as tmp:
@@ -76,18 +81,39 @@ def started(*args, **kwargs):
                 pids = [int((root / f"{depth}.pid").read_text()) for depth in range(3)]
                 self.assertEqual(pids[2], process.pid)
                 for pid in pids:
-                    self.assertTrue(alive(pid))
+                    if pid != process.pid or leader_exit is None:
+                        self.assertTrue(alive(pid))
                     self.assertEqual(os.getpgid(pid), process.pid)
                     self.assertEqual(os.getsid(pid), process.pid)
                 if complete:
                     (root / "release").touch()
+                if interrupt:
+                    real_wait = process.wait
+
+                    def interrupted_wait(*args, **kwargs):
+                        # One interruption after readiness; cleanup must still
+                        # reap the real leader using its ordinary wait method.
+                        process.wait = real_wait
+                        raise KeyboardInterrupt
+
+                    process.wait = interrupted_wait
                 return process
 
             try:
                 # Start the timeout clock only after both descendants exist.
                 with patch.object(package.subprocess, "Popen", side_effect=started):
                     argv = [sys.executable, str(script), str(root), "2"]
-                    if complete:
+                    if leader_exit is not None:
+                        argv.append(str(leader_exit))
+                        if leader_exit:
+                            with self.assertRaisesRegex(ValueError, f"exited {leader_exit}"):
+                                package.run_command(argv, root, 5)
+                        else:
+                            package.run_command(argv, root, 5)
+                    elif interrupt:
+                        with self.assertRaises(KeyboardInterrupt):
+                            package.run_command(argv, root, 5)
+                    elif complete:
                         package.run_command(argv, root, 5)
                     else:
                         with self.assertRaisesRegex(ValueError, "verification timed out"):
@@ -114,6 +140,21 @@ def test_successful_tree_completion(self):
     def test_timeout_terminates_descendants(self):
         self.exercise_tree()
 
+    def test_successful_leader_exit_terminates_descendants(self):
+        self.exercise_tree(leader_exit=0)
+
+    def test_failed_leader_exit_terminates_descendants(self):
+        self.exercise_tree(leader_exit=7)
+
+    def test_interruption_terminates_descendants(self):
+        self.exercise_tree(interrupt=True)
+
+    def test_leader_only_cleanup_is_detected_after_exit(self):
+        for code in (0, 7):
+            with self.subTest(code=code), patch.object(package.os, "killpg", os.kill):
+                with self.assertRaisesRegex(AssertionError, "live descendants after replay"):
+                    self.exercise_tree(leader_exit=code)
+
     def test_parent_only_cleanup_is_detected(self):
         with patch.object(package.os, "killpg", os.kill):
             with self.assertRaisesRegex(AssertionError, "live descendants after replay"):