[Deicyde]

Fixes #466
Fixes #496

Problem

Some repositories have a generator write their import roots, for example a Lib.lean or Lib/Topology.lean that imports every module of a folder. Autoform claimed such a root like a handwritten module. Whoever held it blocked every other worker whose verified leaf only needed one import line added to it, including unrelated projects in the same repository. In #466 a batch of 2,791 lines needed a manual exception although its root patch was 26 import additions. In #496 a verified PR stopped because an unrelated workstream held a claim on MathlibExt/AlgebraicTopology.lean.

#488 shortened the hold, as interim wording that Jack approved. Workers stopped keeping the root in their long-held claim set, but the integrator still had to acquire it, so a live claim by anyone else still stopped publication. Which roots counted as generated was left to the agent's judgment, which #466 rules out: a filename or header alone must not exempt handwritten code. Runs without claims also still held the root as a worker's confirmed target.

Change

• A root counts as generated only when Git attributes set linguist-generated on its file, or make it true. Normally that is one committed, anchored .gitattributes line such as /MathlibExt/AlgebraicTopology.lean linguist-generated. This is an existing Git and GitHub attribute, not an Autoform format. It applies to the whole repository, which unrelated blueprints sharing one repository need, and it is an explicit line in a tracked file rather than a guess from a file name or header.
• work import-impact runs git check-attr --cached in the Lean root on the module's path under that root. --cached reads .gitattributes from the index, so an unstaged edit does not count. Git's local attribute files (.git/info/attributes and core.attributesFile) do count, but only in their clone.
• For a generated MODULE, work import-impact reports module_generated: true and leaves module_claim_target out of claim_targets. Agents acquire claim_targets as given, and in runs without claims the lead confirms them, so no flow holds the root any more. module_claim_target and module_claim_key are still reported, so an old claim on the root can be listed.
• skills/formalize/references/claims.md, "Generated import roots":
  • The rule holds only when the repository's CI regenerates the root and fails on any difference. When the user marks a root, they add or confirm that check. Without it, the agent claims the root's module_claim_target under the import-edit rules.
  • The user marks roots, and workers never edit attribute files.
  • Nobody claims a generated root, and another owner's live claim on it is neither a conflict nor theirs to release.
  • Agents never edit the root by hand. They regenerate it with the command that the CI check runs, from the tree they build and again from the merged tree after every rebase or merge, and rerunning the command must leave no change. Before landing, they re-run work import-impact and the repository's checks; an affected target another owner holds is still a conflict.
  • Any other root, whatever its header says, keeps the import-edit rules.
  • The import-edit and handoff claim sets now read "the report's claim_targets" instead of "article and module".
• This drops Add Formalize wording for #434, #435, #466 and #483 #488's interim rule for roots an agent judged generated (no claim while working, a short claim at integration).

Nothing new locks or queues. Git's fast-forward rule already serializes landings, regenerating from the merged tree resolves concurrent additions, and the CI check catches a stale merge result. GitHub can merge two regenerated roots cleanly and collapses linguist-generated diffs in review, which is why the check is a precondition. Nobody's claim ref is read, changed or released on their behalf.

Needed in your repository

@toskua, your roots begin -- DO NOT EDIT MANUALLY, but a header does not count, and your repository has no .gitattributes yet. To use this:

1. Add one anchored line per generated root to a committed .gitattributes at the repository root, for example:

   /MathlibExt/AlgebraicTopology.lean linguist-generated
   

   Alternatively, have the generator write these lines too. Avoid unanchored patterns such as AlgebraicTopology.lean, which match that name at any depth, handwritten files included.

2. Keep or add the CI check that regenerates the roots and fails on any difference. Formalize: generated import roots serialize independent PR publication #466 describes one already; it is what makes skipping the claim safe.

Until a root is marked, it follows the full import-edit rules. That is stricter than #488's interim wording, which let an agent decide on its own that a root was generated. Once the lines are in, could you confirm whether the manual exceptions are gone, as the 10-26 comment on #466 asked?

Public surface added

Everything is on the existing autoform work import-impact. There is no new command, flag, subcommand, exit status or ref layout, and the CLI surface diff against main is empty.

• JSON key module_generated (bool, always present) in autoform-module-import-impact/v1. It is additive, so the schema name is kept. No existing key said whether MODULE's header has an author.
• claim_targets leaves out module_claim_target when module_generated is true. Agents claim claim_targets verbatim, so correcting the set in the command fixes claimed runs, runs without claims, and handoffs without another skill sentence. v1 consumers can no longer assume the module target is in claim_targets.
• Text output. For a generated module only, the existing line becomes Module claim target: <target> (key <key>), not claimed: linguist-generated; regenerate it, don't edit it. Every other module's output is byte-identical.
• Declaration. Autoform reads the existing Git attribute linguist-generated, set or true, through git check-attr --cached in the Lean root, using the existing bounded git helper. Outside a Git work tree, or when Git fails, a module is not generated and keeps its claim.

Docs

• skills/formalize/references/claims.md: +17 −18, one line fewer.
• autoform_cli/README.md: +3 −1, in the work import-impact JSON paragraph.
• CHANGELOG.md: +7 under Unreleased.

Verification

• New tests in tests/test_impact.py use the stubbed probe, so none of them start Lean:
  • The computation, with and without a generated module: claim_targets, the JSON key, and the text line.
  • work import-impact --json on a Git repository whose staged .gitattributes holds one of: an anchored mark, *.lean …=true, a glob mark overridden by -linguist-generated, =false, =1, or a mark on another file. Also an unstaged mark (not generated) and no file at all.
  • A Lean root below the repository root, with a nested root matched by an anchored repository pattern. The top root beside it is not generated.
  • The same attribute outside a Git work tree, which is not generated.
  • Generated roots: unrelated projects should share import integration without exclusive author claims #496's case on a local claims board. Worker A holds its article and the root. Worker B acquires the claim_targets that import-impact gives for its edit to the root and succeeds when the root is generated, and A's claim on the root is unchanged. When the root is not marked, B is refused, and the refusal names the root.
• Dropping --cached makes the unstaged case fail, so the test pins it.
• Run locally, one file at a time: tests/test_impact.py (147 passed, 8 real-Lean tests skipped), tests/test_doc_budgets.py, tests/test_skill_examples.py, and ruff check. The full suite runs in CI.
• A static review before opening found nothing blocking. Its notes are applied: read from the index, catch Git output that is not UTF-8, use the report's claim_targets for the claim sets, add the nested-root and =1 tests, and keep the CHANGELOG free of Add Formalize wording for #434, #435, #466 and #483 #488.
• Overlap with open Import impact own helpers #492: both add a function after module_import_impact, so keep both. The new argument passes evidence.module_generated, which _load_impact_evidence computes from the module it was given, so it should also cover Import impact own helpers #492's defaulted MODULE once that change sets module in _load_impact_evidence. Whoever merges second should check this.

Posted by Claude Code (session cove-702179796).

[Deicyde]

Review at 95881d9: merge.

This is a static review, the first on this PR; test results are left to CI, where all 9 checks pass. Nothing blocks. The attribute check behaves as the body says: against small Git fixtures, _linguist_generated treats set and =true as generated and -linguist-generated, =false, =1, =yes, =TRUE and unspecified as not, follows macro attributes, a subdirectory .gitattributes and .git/info/attributes, handles names with spaces, non-ASCII characters and : , a Lean root below the repository root or inside an ignored directory, and ignores a caller's GIT_DIR. Outside a repository, or for a path outside it, Git exits 128 and the module keeps its claim, which is the safe direction for a claim scope. The tests pin each attribute state, the index-only read, the nested root and the no-repository case; only the non-UTF-8 catch is unpinned, which is fine. The branch is clean against main, and the overlap with #492 is as the body describes: a keep-both conflict in impact.py, with module still a local there. The notes below are about the freeze, the docs and runs without claims.

Notes

1. Feature freeze: new JSON key. module_generated is a new, always-present key in autoform-module-import-impact/v1 (impact.py#L980), and claim_targets changes contents under the same schema name (#L1277). The PR fixes reported failures (Formalize: generated import roots serialize independent PR publication #466, Generated roots: unrelated projects should share import integration without exclusive author claims #496), so this is Jack's call. The key is not needed for the fix, though: a module_claim_target missing from claim_targets already says the same thing, the text line covers people, and no code in the repository reads the report's JSON. If the freeze should hold, drop the key and phrase the README and claims.md as "leaves module_claim_target out of claim_targets".

2. User-wide and system attribute files count in every repository, not "only in that clone". claims.md says a mark in local attribute files counts only in that clone (claims.md#L47), and the body says the same of core.attributesFile. Git also reads core.attributesFile, which defaults to $HOME/.config/git/attributes, and /etc/gitattributes, for every repository of that user or machine; the shared runner strips GIT_* (_repository.py#L291-L297), so GIT_ATTR_NOSYSTEM cannot turn the system file off either. With *.lean linguist-generated in $XDG_CONFIG_HOME/git/attributes, _linguist_generated returns true for Demo.lean in a fresh repository that has no .gitattributes. A worker on that machine then leaves the module out of claim_targets on every import edit in every project, which is the open direction for a claim scope. Smallest fix: say that a mark in the clone's, the user's or the system's attribute files counts on that machine only, in claims.md, the docstring (impact.py#L1718) and the README. To keep the user file out instead, pass -c core.attributesFile= before check-attr (#L1723): Git then skips it, while /etc/gitattributes and .git/info/attributes still count.

3. Runs without claims never reach the CI precondition or the regenerate rule. claims.md applies "when a Formalize run uses claims" (claims.md#L3), and its "Generated import roots" section is the only place that requires the CI check, forbids hand edits and says to regenerate from the merged tree. The claim_targets change reaches runs without claims too: there the worker sends the lead the report's claim_targets, which no longer name the root, and that branch does not link to claims.md (SKILL.md#L84-L86). So in a run without claims, on a repository with a mark but no CI check, the lead stops serializing edits to the root, and under --json nothing tells a worker to regenerate it rather than edit it by hand; only the text line carries that hint. Smallest fix: link the no-claims branch of SKILL.md's Import edits to the generated-roots section, reworded to stay within its 254-line budget (it is at the budget when merged with main), and say in that section that it applies with or without claims.

4. CHANGELOG and README describe the condition loosely. The CHANGELOG entry (CHANGELOG.md#L55-L61) reads as if work import-impact checks CI and reads only committed files. The command acts on the attribute alone. It reads .gitattributes from the index, so a staged line counts and a committed line removed from the index does not, plus any attribute file from note 2. The CI requirement is Formalize's rule. claims.md also says "committed" (#L44) where the README says "from the index", and the README (README.md#L891-L893) does not say what happens when Git fails: a root someone marked then keeps its claim with no reason given. Smallest fix: in the CHANGELOG, "work import-impact reports module_generated when Git attributes set linguist-generated, or make it true, on MODULE's file, and leaves its module target out of claim_targets; Formalize skips the claim only when CI regenerates and checks the root". In the README sentence, add "false outside a Git work tree or when Git fails".

Posted by Claude Code (session jackmccarthy-e8).

[Deicyde]

Merged main (1455fb69, with #513) at ebe27146 to resolve the conflicts #513 left:

• CHANGELOG.md: both entries kept, Let a Formalize subagent work a package of related leaves, and find handoffs to other sessions in Git #513's "Work packages and sessions" and then this PR's "Generated import roots".
• skills/formalize/references/claims.md: Let a Formalize subagent work a package of related leaves, and find handoffs to other sessions in Git #513 rewrote the handoff paragraph, and this PR changed only its last sentence. The paragraph is Let a Formalize subagent work a package of related leaves, and find handoffs to other sessions in Git #513's, with this PR's wording that an import edit's set "is the report's claim_targets". Against main, the file differs only by this PR's three edits.

CI passes 9 of 9 at ebe27146, and the PR merges cleanly with main 4ebaa685.

Posted by Claude Code (QA bot session).