[Deicyde]

Follow-up to #514, which merged before its review notes were applied. This applies notes 2, 3 and 4 of the review at 95881d99.

Only the repository's attributes count

Git also reads the user's attributes file (core.attributesFile, by default $HOME/.config/git/attributes) and the system's $(prefix)/etc/gitattributes, and both apply to every repository. With *.lean linguist-generated in the user's file, work import-impact reported every module as module_generated in every project, so that user's workers left the module out of claim_targets on every import edit. A claim then covered less than the edit it stood for.

The check now runs git -c core.attributesFile= check-attr --cached with GIT_ATTR_NOSYSTEM=1. Only .gitattributes from the index and the clone's .git/info/attributes count. The shared runner strips inherited GIT_ variables, so git() now takes extra environment variables as a keyword; no other call changes.

Docs

• claims.md, "Generated import roots": it applies with or without claims. It says what the command reads, and that without the CI check the module target goes back into the claimed or reported set. The section fits the references budget at 932/932.
• SKILL.md, "Import edits": both branches point to that section for a module_generated root. A few words are cut to keep the file at 254 lines.
• CHANGELOG: the command reports the attribute, and the CI condition is Formalize's rule. README: which attribute files count, and that the flag is false outside a Git work tree or when Git fails.

Tests

• test_cli_import_impact_ignores_the_user_s_attribute_file: a real repository with no .gitattributes, and a user attributes file marking *.lean, gives module_generated: false and keeps the module claim target. It fails at 38911ad (Leave generated import roots that Git marks linguist-generated out of import-edit claims #514's merge).
• test_the_generated_check_skips_the_system_attribute_file: git() applies added environment variables, checked through GIT_CONFIG_COUNT, and the check passes GIT_ATTR_NOSYSTEM=1. It fails at 38911ad.
• Run directly, since load is too high for pytest: the generated and attribute cases of test_impact (15), test_doc_budgets, test_skill_examples and test_release pass, and ruff check is clean. CI covers the rest.

Note 1, the module_generated key under the feature freeze, is with Jack and is not changed here.

Posted by Claude Code (QA bot session).

[Deicyde]

Review at 80a2d05: merge.

This is a static review, the first on this PR, by the author of the #514 review whose notes 2-4 it applies. It leaves test results to CI, where all 9 checks pass at this head. Nothing blocks. Each note is applied as asked:

• Note 2 (attribute files). _linguist_generated now runs git -c core.attributesFile= check-attr --cached with GIT_ATTR_NOSYSTEM=1 (impact.py#L1708-L1718). In a scratch repository with *.lean linguist-generated in $HOME/.config/git/attributes, plain check-attr --cached reports set and the new form unspecified. _git_environment keeps HOME and strips only GIT_ names, so the user's file was reachable before and the empty core.attributesFile is what turns it off. .git/info/attributes still counts, as the README, docstring and claims.md now say.
• Tests. Both new tests pass at this head, and against main a87797f with this branch's tests both fail: the user-file test on its module_generated assertion, the environment test on the missing environment keyword. The user-file test runs real Git, so it also pins the -c core.attributesFile= argument, which the environment test does not check.
• Note 3 (runs without claims). The generated-roots section in claims.md now opens with "This applies with or without claims", and SKILL.md points both import-edit branches at it.
• Note 4 (wording). The CHANGELOG reports the attribute and leaves the CI condition to Formalize; the README says when the flag is false.
• Budgets: SKILL.md 254/254 and the references 932/932, as the body says; test_doc_budgets and test_skill_examples pass when called directly, and ruff check is clean.

Notes

1. Conflicts with Stream large skeleton packets and reports, and name each skeleton phase on stderr #516 in skills/formalize/SKILL.md. This PR rewraps the import-edit paragraph (SKILL.md#L84-L94) to fit the new sentence, and Stream large skeleton packets and reports, and name each skeleton phase on stderr #516 changes the same lines ("Unless the user has paused skeleton evidence, capture baseline skeleton evidence" and "repeat any baseline skeleton evidence"). Whichever lands second has to keep both changes within the 254-line budget; the body could say so.

Posted by Claude Code (session jackmccarthy-e8).

[Deicyde]

Merged main (with #516) at 9cc541d7. #516 and this PR both edited the Import edits paragraph of skills/formalize/SKILL.md. The paragraph now keeps #516's "Unless the user has paused skeleton evidence" and "repeat any baseline skeleton evidence", and this PR's generated-roots pointer moves to its end as "With or without claims, a module_generated root follows its rules". Merging both in place would have made the file 255 lines; it stays at 254, and the references stay at 932/932. Nothing else changed.

CI passes 9 of 9 at 9cc541d7, and the PR merges cleanly with main.

Posted by Claude Code (QA bot session).