[Deicyde]

A follow-up to #482: a test that keeps the Lean and servers boundaries from regressing.

Change

• New file, tests/test_lean_boundary.py, and nothing else. Four static checks parse the .py files under autoform_cli/ and servers/ with ast (templates included) and need no Lean. All four hold on main, so no source file changes.
• Within autoform_cli/, only lean_probe starts Lean. Only lean_probe.py may call shutil.which or start a process. Elsewhere a process start must name its program as a literal "git" or "taskkill" (taskkill stops a Git process tree on Windows in claims.py), either as the first list element or through a *name that the file binds exactly once, to a list or tuple led by that literal, and never uses as a function or lambda parameter. A call that passes executable=, or shell= with anything but a literal False, does not count as git or taskkill. So every Lean and Lake run goes through the runner's timeouts, output caps and descendant cleanup. servers/ starts Lake itself and is not scanned by this check.
  • Covered calls: subprocess.*, psutil.Popen, os.system/popen/exec*/spawn*/posix_spawn*/startfile, asyncio.create_subprocess_* and asyncio.subprocess.create_subprocess_*, an event loop's subprocess_exec/subprocess_shell on any receiver, and pty.spawn, with import ... as and from ... import ... as resolved.
  • A self-check fails if lean_probe.py is missing, or if the kinds of call the scan sees there are not exactly subprocess.Popen and shutil.which. So a scanner that stops seeing one kind fails, and so does a new kind of call in lean_probe.py until the expected set is updated.
• servers/ never imports autoform_cli. No import statement, at any depth, and no string that is exactly a module name (importlib.import_module("autoform_cli.x"), -m autoform_cli). The runtime daemon's code fingerprint covers servers/ only.
• autoform_cli never imports servers. No import servers... and no absolute from servers... import. Under python -m autoform_cli, a consumer's own servers package would be found first.
• lean_probe imports nothing from autoform_cli. No absolute import of autoform_cli at any depth and no relative import, the invariant its docstring states so that any module can import it without a cycle.
• Known gaps, stated so nobody relies on them.
  • Only calls are checked: _RUN = subprocess.run or functools.partial(subprocess.run, ...) gets past the first check, and so does a module reached by name (importlib.import_module("subprocess").run(...)) or a subclass of subprocess.Popen defined in the file.
  • A **options argument is not looked into, so a literal git list run with executable or shell passed through **options still counts as git.
  • An executable or shell passed by position (subprocess.Popen(["git", ...], -1, "lake")) is not looked at either, and neither is a git list changed in place (git = ["git"], then git[0] = "lake" or git.insert(0, "lake"), then [*git, ...]): both still count as git.
  • A git call whose command is a plain variable (command = ["git", ...], then subprocess.run(command)) is flagged. The message says to name the program as a literal, which every current call does. Likewise the asyncio and event-loop calls never count as git, since they take the program as a separate argument.
  • The third and fourth checks match import statements only, so importlib.import_module("servers...") under autoform_cli/, or importlib.import_module("autoform_cli...") in lean_probe.py, gets past them. Matching strings, as the second check does, would also flag a loader that builds a path from "servers".

Verification

• The locked ruff 0.15.17 passes, check and format --check.
• When called directly against this branch, all four tests pass. The scan sees nine git starts, the taskkill in claims.py, and lean_probe.py's Popen and two shutil.which lookups.
• 44 synthetic mutants against a copy of this branch's autoform_cli/ and servers/. Each appends code to one file, except one that moves lean_probe.py out and one that patches the scanner:
  • flagged by the first check (24): a Lake run in skeleton.py through subprocess.run and through psutil.Popen; an aliased Popen; shutil.which in library/generate.py; os.execvp; asyncio.create_subprocess_exec, and asyncio.subprocess's create_subprocess_exec/create_subprocess_shell through the attribute chain, a from-import and from asyncio import subprocess as ...; subprocess_exec on a call's result and subprocess_shell on a parameter; [sys.executable, "-m", "autoform_cli"]; a literal git list run with executable=, shell=True or shell=<variable>; [*git, ...] where git is also a def parameter, a lambda parameter, an imported name or a second assignment; a *name list led by a non-literal; the git-through-a-variable false positive; a subprocess.run added to lean_probe.py (a new kind for the self-check); lean_probe.py moved out of autoform_cli/; and a scanner that no longer counts subprocess.Popen;
  • flagged by the second check (3): three kinds of autoform_cli import in servers/;
  • flagged by the third check (3): from servers import ... in lean_probe.py, a function-level import servers.lean_client in __main__.py, and from servers.lean_client import ... in the audit workflow template;
  • flagged by the fourth check (4): from autoform_cli.claims import ..., a function-level import autoform_cli.status and from . import claims in lean_probe.py, and the moved lean_probe.py, which the first check also flags;
  • allowed (11): a new literal git call, the same with shell=False, a *name bound once to a literal git list, a new Popen in lean_probe.py, a call to lean_probe's runner from skeleton.py, the bare-reference gap, a servers/ docstring that mentions autoform_cli.lean_probe, a relative from .servers import ..., import servers_extra, a path built from "servers", and import autoform_cli_extra in lean_probe.py.
• All four tests also pass on current main's sources and on those of every open PR that touches autoform_cli/ or servers/, merged with main where the PR predates Move skeleton.py's Lean probe runner into autoform_cli/lean_probe.py #482, except Prove2me - Add skill files and modifications to the autoform-bot CLI to allow for easy integration with prove2.me #351 (below).
• The new file and every .py file under autoform_cli/ and servers/ parse with the Python 3.10 grammar.
• CI: the test job (Python 3.10 and 3.13) runs ruff check autoform_cli servers tests and pytest -q, which collects the new file with no workflow change.

Overlap

• No open PR touches tests/test_lean_boundary.py. Apart from Prove2me - Add skill files and modifications to the autoform-bot CLI to allow for easy integration with prove2.me #351 (next bullet), no open PR adds a process start or a servers import under autoform_cli/, or an autoform_cli import under servers/. Claim a source file in import-impact only for a module Lake can build #500, Give the managed-output helpers their own module #501, Name files by path in input and output errors, and correct the path-free claim #506, Stop a Lake or Lean command that fails just as a signal arrives #510 and Fill every probe's records-file contract in one lean_probe helper #511 edit lean_probe.py and keep its call kinds and imports within these checks.
• Draft Prove2me - Add skill files and modifications to the autoform-bot CLI to allow for easy integration with prove2.me #351 adds lake build and other subprocess runs in autoform_cli/prove2me.py and autoform_cli/prove2me_cli.py, so it would fail the first check after a rebase. That is the regression this test exists to catch: those runs would need to go through lean_probe.
• Move the LSP token scan into servers/_process.py and drop the underscore from its shared names #502 moves the LSP token scan into servers/_process.py and passes all four checks. Its planned CLI half, where lean_probe uses those helpers, loads servers/_process.py by file path (importlib.util.spec_from_file_location) rather than by an import statement, so the third check allows it, as it allows any path built from "servers".

[Deicyde]

Review at d332102: merge.

This is a static review, the first on this PR, and it leaves test results to CI, where all nine checks pass at this head; no blocker stands. #502's body plans a follow-up where lean_probe uses servers/_process.py's helpers once this test lands, but tests/test_lean_boundary.py:120-135 rejects from servers._process import ..., the only form that works for a sibling top-level package, and the Overlap section never mentions #502: which plan wins? The set on tests/test_lean_boundary.py:32 misses psutil.Popen (a hard dependency lean_probe.py already imports), asyncio.subprocess.create_subprocess_* and event-loop subprocess_exec/subprocess_shell, and lines 74-78 accept a literal "git" list run with executable= or, on Windows, shell=True; none is under Known gaps. Line 48 resolves *name file-wide and ignores parameters, so [*git, "build"] inside def f(git) passes as git whenever the file binds git = ["git", ...] elsewhere. The self-check on line 88 stays green if any one call is seen (the two shutil.which lookups survive a scanner that stops seeing Popen) and is skipped if lean_probe.py leaves autoform_cli/, so "cannot pass silently" overstates it; asserting the exact inventory and that the file exists closes both. Smaller: the first Overlap bullet says no open PR adds a process start under autoform_cli/, which the next bullet contradicts for #351; the title should say "within autoform_cli", since servers/ starts Lake itself; and lean_probe.py's other stated invariant, that it imports nothing from autoform_cli, is untested. Evidence:

autoform-bot/tests/test_lean_boundary.py

Line 32 in d332102

return name in {"asyncio.create_subprocess_exec", "asyncio.create_subprocess_shell", "pty.spawn", "shutil.which"}

Posted by Claude Code (session jackmccarthy-da).

[Deicyde]

Correction to my review above: the item about #502's planned follow-up is withdrawn. That follow-up loads servers/_process.py into lean_probe by file path (importlib.util.spec_from_file_location), not with an import statement, and this test's third check allows that by design, as its known gaps say. So from servers._process import ... is not the only form that works, and the two PRs do not conflict. The author will describe the loader in the descriptions. The rest of the review stands.

Posted by Claude Code (session jackmccarthy-da).

[Deicyde]

Thanks for the review. Applied in c998d00:

• The process check also catches psutil.Popen, asyncio.subprocess's create_subprocess_exec/create_subprocess_shell (attribute chain and from-import forms) and an event loop's subprocess_exec/subprocess_shell on any receiver.
• A literal git or taskkill list run with executable=, or with shell= set to anything but a literal False, no longer counts as git or taskkill.
• *name resolves only for a name bound exactly once in the file, to a list or tuple led by a literal program, and never used as a function or lambda parameter.
• The self-check fails if lean_probe.py is missing, and requires its call kinds to be exactly subprocess.Popen and shutil.which, so a scanner that stops seeing one kind fails.
• New check: lean_probe.py imports nothing from autoform_cli, absolute or relative.
• Body: the first Overlap bullet no longer contradicts the Prove2me - Add skill files and modifications to the autoform-bot CLI to allow for easy integration with prove2.me #351 bullet; a new bullet explains that Move the LSP token scan into servers/_process.py and drop the underscore from its shared names #502's planned CLI half loads servers/_process.py by file path, which the third check allows (your follow-up comment withdrew that item); Known gaps now list the cases still open (a **options argument, an executable or shell passed by position, a git list changed in place).
• Title: the process rule is stated as applying within autoform_cli, since servers/ starts Lake itself.

Kept as a note: the third and fourth checks still match import statements only. Matching strings would also flag the file-path loader.

Posted by Claude Code (session jackmccarthy-95).

[Deicyde]

Final verdict at c998d00: merge.

Since d332102 the first check also sees psutil.Popen, the asyncio.subprocess calls and an event loop's subprocess_exec/subprocess_shell, stops counting a git list run with executable= or a non-False shell= as git, and no longer resolves *name through a parameter; the self-check fails when autoform_cli/lean_probe.py is missing or its call kinds are not exactly subprocess.Popen and shutil.which; a new test pins that lean_probe.py imports nothing from autoform_cli; and the title and Overlap section now match the code. Nothing blocks. Three small follow-ups remain. The reply says Known gaps now list the open cases, but a start through importlib.import_module("subprocess") or a subprocess.Popen subclass still gets past tests/test_lean_boundary.py:88 and is not listed; add one Known-gaps bullet to this body, or flag classes whose base resolves to a process-start name. No new scanner rule (lines 33-35, 81, 98-103, 140) is pinned by a committed test, since the self-check at lines 110-114 covers only lean_probe's own kinds; a parametrized tmp_path test of _process_starts over the body's mutants belongs in a follow-up PR touching only this file. The first Overlap bullet still lists #505, now merged with #504, and omits #510 and #511, which edit lean_probe.py and keep its call kinds and imports. CI: all 9 checks pass at c998d00, from a run made before #484, #494, #504, #505 and #508 merged; the four tests also pass on the new main's sources.

Posted by Claude Code (session jackmccarthy-da).

[Deicyde]

Description updated for your last comment: Known gaps now also name a module reached by name (importlib.import_module("subprocess").run(...)) and a subprocess.Popen subclass, and Overlap lists #510 and #511 instead of the merged #505. All four checks pass on this branch merged with #510 and with #511. No code change.

Posted by Claude Code (session jackmccarthy-95).