[zibo-yang]

Problem

A Lean project has no autoform on PATH. Roadmap, Formalize, agent-review and human-review tell agents to run bare autoform … commands. The prefix they actually need, uv run --project "<AUTOFORM_PLUGIN_ROOT>", appears in one sentence of autoform_cli/README.md#commands, and Roadmap points agents at that README "only when exact syntax or CLI usage is needed".

So agents guessed. Across 21 headless trial sessions (Setup → Roadmap → Formalize on paper §1.2, with ATLAS):

Skill	Sessions without the launcher in context	Started by guessing	Never reached the CLI
Setup (states the launcher)	4	0	0
Roadmap	8	8	2
Formalize	5	5	1

• The guesses were which autoform, then python3 -m autoform_cli, a bare uv run autoform, or reading the Makefile.
• The worst Roadmap session made 15 guesses, gave up on the CLI, used find in place of autoform search, and skipped library reuse altogether.
• Fresh Formalize sessions found the launcher only after reading the 1,800-line README in chunks.
• Every session already knew the plugin root: they had all run ls on it. What none of them had was the form of the command.

A test enforced the gap: test_skills_delegate_the_command_line_to_the_reference forbade uv run --project in every skill except Setup.

Change

• Skills: Roadmap, Formalize, agent-review and human-review each state the launcher once, near the top. The paragraph says:

  • there is no autoform on PATH;
  • run every command as uv run --project "<AUTOFORM_PLUGIN_ROOT>" autoform followed by its arguments, from the project;
  • the plugin root is the directory that holds the skill's skills/ folder, along with pyproject.toml and autoform_cli/;
  • give subagents that root and the prefix, since Formalize's worktree subagents don't load the skill.

  The root is described by its contents rather than as "N levels above the skill's base directory", because Codex and Muse present a skill by path, not with Claude Code's "Base directory" line.

• Formalize: the vague "resolve the plugin root and run commands through the invocation contract" sentence is replaced by that paragraph.

• Tests:

  • The delegation test still forbids restating a subcommand or flags, and now allows exactly the bare launcher.
  • A new test finds every skill whose text names an autoform command and requires the paragraph, including the exact subagent sentence. Setup and Develop Plugin are exempt, with the reasons stated.

Verification

• Suite: uv run pytest → 3246 passed, 56 skipped, 1 xfailed; make lint clean.

• Test checked: the new test fails without the paragraph, and fails when the subagent sentence is removed.

• Fresh chain: I reran the same Setup → Roadmap → Formalize prompts and allowlist from scratch on this branch, with no launcher hint in any prompt:

  Session	Guesses before the first CLI call	First CLI call
  Setup	0	call 6
  Roadmap	0 (before: 8 of 8 guessed)	call 9, autoform library list .
  Formalize	0 (before: 5 of 5 guessed)	call 13, autoform work list …

  That Roadmap ran 8 ATLAS searches and reused 3 ATLAS results, and check and audit were clean.

• Not yet confirmed: the Formalize run is still in progress, so its worktree subagents haven't been checked yet. No Codex or Muse run has been done.

🤖 Generated with Claude Code

[zibo-yang]

Final check before merge

Branch state. The branch is rebased on 54127e97 (current main, including #307). Rebasing caused no conflicts. The full suite passes on the rebased head (3246 passed, 56 skipped, 1 xfailed), and make lint is clean.

Fresh end-to-end trial on this branch. I ran Setup → Roadmap → Formalize from scratch, with the same prompts and permission allowlist as the earlier baseline. None of the prompts hinted at the launcher.

Session	which autoform and other guesses	First CLI call	Outcome
Setup	0	call 6	ATLAS project created, library list: atlas usable, all builds green
Roadmap	0 (baseline: 8 of 8 guessed)	call 9, uv run --project … autoform library list .	8 ATLAS searches, 3 results reused from ATLAS, check and audit clean
Formalize	0 in 166 tool calls (baseline: 5 of 5 guessed)	call 13, uv run --project … autoform work list …	2 results committed with no sorry: the Legendre/Gauss corollary from ATLAS lemmas, and the Hurwitz class number definition, which it checked against 23 table values. Fully proved results went from 3 to 5; check, audit and unused-hypotheses are clean; all claims are released

Neither Roadmap nor Formalize ever ran which autoform or opened autoform_cli/README.md to find the launcher. The only permission denials in either session came from piping JSON into python3, which the trial allowlist doesn't cover. They are unrelated to this change.

Not yet verified:

• The subagent hand-off sentence. Formalize dispatched 2 subagents, both read-only reviewers that never ran the CLI, so no run has exercised the hand-off yet.
• The two main Theorem 1.4 cases. Formalize stopped before them because the paper only cites Gauss's Disquisitiones for them. That limit is mathematical, not a tooling problem.
• Codex and Muse. No session has run on either host. The plugin-root wording describes the directory by its contents (it holds skills/, pyproject.toml and autoform_cli/) so that it doesn't depend on Claude Code's "Base directory" line. That reasoning hasn't been checked with a live agent.

Possible follow-ups (none blocks this PR):

• The command examples in the reference files under agent-review and Formalize could point back to the skill's launcher paragraph.
• The #commands section of the README could describe the plugin root as concretely as the skills now do.

Ready to merge from my side.

🤖 Generated with Claude Code