Count only the repository's Git attributes for generated roots, and apply #514's review notes

CHANGELOG.md

@@ -66,11 +66,13 @@ date when the release is tagged.
   pushing, goes to an `origin` branch ending with the leaf's `article_id`, which
   `git ls-remote` finds after the lease is gone. No message grants ownership or
   completes a leaf (#434).
-- **Generated import roots.** A root that a committed `.gitattributes` line
-  such as `/Lib.lean linguist-generated` marks, and that CI regenerates and
-  checks, is no one's to claim: `work import-impact` reports `module_generated`
-  and leaves its module target out of `claim_targets`, and Formalize regenerates
-  the root from the merged tree, so independent leaves, other projects'
+- **Generated import roots.** `work import-impact` reports `module_generated`
+  when the repository's Git attributes set `linguist-generated` on MODULE's
+  file, or make it `true`, normally through a committed `.gitattributes` line
+  such as `/Lib.lean linguist-generated`, and leaves its module target out of
+  `claim_targets`. The user's and the system's attribute files do not count.
+  Formalize skips the claim only when CI regenerates and checks the root, and
+  regenerates it from the merged tree, so independent leaves, other projects'
   included, publish without waiting on a claim on it. Any other root keeps the
   import-edit claims (#466, #496).
 - **Render.** An article's page lists its `mathlib_declaration` names in a

autoform_cli/README.md

@@ -901,10 +901,12 @@ JSON uses `autoform-module-import-impact/v1`, with `module_graph_revision` and
 the selected article (`id`, `article_id`, `claim_target`). `claim_targets` holds
 only it and `module_claim_target`, `lean-module/<lowercase-slug>-<sha256[:16]>`,
 whose key is `module_claim_key`, or only it when `module_generated`: Git
-attributes, from the index or local attribute files, set `linguist-generated` on
-MODULE's file, or make it `true`. `affected_claim_targets` are downstream
-warnings, not ownership requirements; `claim_keys` and `affected_claim_keys`
-match the JSON of `autoform claim list --worker-id WORKER` given those targets.
+attributes from the index or the clone's `.git/info/attributes`, not the user's
+or the system's attribute files, set `linguist-generated` on MODULE's file, or
+make it `true`. It is `false` outside a Git work tree or when Git fails.
+`affected_claim_targets` are downstream warnings, not ownership requirements;
+`claim_keys` and `affected_claim_keys` match the JSON of
+`autoform claim list --worker-id WORKER` given those targets.
 `affected_articles` lists each article that names, or owns through the parent
 chain, a declaration in an affected module, with those `modules`, and
 `selected_affected` says whether the selected article is one.

autoform_cli/_repository.py

@@ -19,7 +19,7 @@
 import os
 import subprocess
 import unicodedata
-from collections.abc import Iterable
+from collections.abc import Iterable, Mapping
 from pathlib import Path
 from urllib.parse import urlsplit, urlunsplit
 
@@ -271,13 +271,15 @@ def _normalize_remote(remote: str) -> str | None:
     return urlunsplit((parsed.scheme, netloc, path, "", ""))
 
 
-def git(root: str | Path, *arguments: str) -> str | None:
+def git(root: str | Path, *arguments: str, environment: Mapping[str, str] | None = None) -> str | None:
+    """Run Git in ``root``; ``environment`` adds variables to the stripped environment."""
+
     try:
         result = subprocess.run(
             ["git", *arguments],
             cwd=str(root),
             capture_output=True,
-            env=_git_environment(),
+            env={**_git_environment(), **(environment or {})},
             text=True,
             timeout=10,
             check=False,

autoform_cli/impact.py

@@ -1701,14 +1701,27 @@ def module_import_impact(
 def _linguist_generated(root: Path, relative: str) -> bool:
     """Whether Git attributes set ``linguist-generated``, or make it ``true``, on ``relative`` under ``root``.
 
-    That is how a repository declares a generated import root. ``--cached``
-    reads ``.gitattributes`` from the index, so an unstaged edit does not
-    count; Git's local attribute files still do. A file outside a Git work
-    tree, or one Git cannot be asked about, is not generated.
+    That is how a repository declares a generated import root. Only the
+    repository's attributes count: ``--cached`` reads ``.gitattributes`` from
+    the index, so an unstaged edit does not count, and the clone's
+    ``.git/info/attributes`` counts in that clone. The user's and the system's
+    attribute files are skipped, since a mark there would cover every
+    repository on the machine. A file outside a Git work tree, or one Git
+    cannot be asked about, is not generated.
     """
 
     try:
-        output = git(root, "check-attr", "--cached", "linguist-generated", "--", relative)
+        output = git(
+            root,
+            "-c",
+            "core.attributesFile=",
+            "check-attr",
+            "--cached",
+            "linguist-generated",
+            "--",
+            relative,
+            environment={"GIT_ATTR_NOSYSTEM": "1"},
+        )
     except ValueError:  # Git printed a name that is not UTF-8
         return False
     return output is not None and output.rsplit(": ", 1)[-1] in ("set", "true")

skills/formalize/SKILL.md

@@ -78,24 +78,25 @@ rules](references/claims.md) at each step.
 
 ### Import edits
 
-Lean imports are allowed; do not pre-block a proof because it needs one. Before
-an effective module header or import change, run `autoform work import-impact`,
+Lean imports are allowed; never pre-block a proof for needing one. Before an
+effective module header or import change, run `autoform work import-impact`,
 rerunning it with `--module-scope import-closure` when the default scope cannot
 build or load every root library. When the run uses claims, follow the [import
 claims](references/claims.md#import-edits) from then on; otherwise send the lead
 the report's `claim_targets` and `affected_claim_targets` and wait for its
 answer. Unless the user has paused skeleton evidence, capture baseline skeleton
 evidence for the report's currently built, named affected articles and, when the
 edit removes an import, for the articles of modules only that import kept in the
-build. The affected articles are not a lock: do not acquire or edit them merely
-because they are listed, and treat reported unresolved declarations as unknown
-validation scope, not proof they are unaffected. After rebuilding, repeat any
-baseline skeleton evidence and use Agent Review to judge semantic changes; repair
-each article that actually needs changes under the review gates of the [revision
+build. The affected articles are not a lock: do not acquire or edit them because
+they are listed, and treat unresolved declarations as unknown validation scope,
+not proof they are unaffected. After rebuilding, repeat any baseline skeleton
+evidence and use Agent Review to judge semantic changes; repair each article
+that needs changes under the review gates of the [revision
 contract](../../autoform_cli/reference/claims-and-revisions.md#revision-contract).
 Stop for an active conflict (an affected target another worker holds, or another
 owner's live claim on one) or failed validation, not for a blanket import rule;
-disclosure alone is neither.
+disclosure alone is neither. With or without claims, a `module_generated` root
+follows [its rules](references/claims.md#generated-import-roots).
 
 Bring the worktree up to date with the shared branch (after [acquiring the
 claim](references/claims.md#acquire-and-renew), when the run uses claims) and
@@ -235,9 +236,8 @@ commit for handoff. When the run uses claims, the [claim
 rules](references/claims.md#integration-and-handoff) say how to renew, keep,
 hand off, and release the claim set.
 
-When `AUTOFORM_SUBAGENT_DEBRIEF=1`, the agent that worked an attempt then
-follows the [subagent debrief steps](references/debrief-subagent.md) before
-reporting.
+When `AUTOFORM_SUBAGENT_DEBRIEF=1`, the agent that worked an attempt follows
+the [subagent debrief steps](references/debrief-subagent.md) before reporting.
 
 Once a worker has reported, debrief included, and its result is integrated or
 handed off, the lead removes its worktree with `git worktree remove` (never

skills/formalize/references/claims.md

@@ -43,14 +43,15 @@ hand off, and release the full import claim set together.
 
 ## Generated import roots
 
-A root is generated only when a committed `.gitattributes` line such as
-`/Lib/Topology.lean linguist-generated` marks it and the repository's CI
-regenerates it and fails on any difference. The user marks roots and adds or
-confirms that check; workers never edit attribute files, and a mark in a
-clone's local attribute files counts only in that clone. `work import-impact`
-reports a marked root as `module_generated` and leaves it out of
-`claim_targets`; without that check, claim its `module_claim_target` under the
-import-edit rules above. No one claims a generated root; another owner's live
+This applies with or without claims. A root is generated only when a committed
+`.gitattributes` line such as `/Lib/Topology.lean linguist-generated` marks it
+and the repository's CI regenerates it and fails on any difference. The user
+marks roots and adds or confirms that check; workers never edit attribute files.
+`work import-impact` reads the mark from the index or the clone's
+`.git/info/attributes`, never the user's or the system's attribute files,
+reports it as `module_generated`, and leaves `module_claim_target` out of
+`claim_targets`; without that check, add it back, claimed or sent to the lead,
+as for any import edit. No one claims a generated root; another owner's live
 claim on it is neither a conflict nor yours to release. Never edit it by hand:
 regenerate it with the command that check runs, from the tree you build and
 again from the merged tree after every rebase or merge; rerunning it must leave

tests/test_impact.py

@@ -10,9 +10,11 @@
 
 import pytest
 
+import autoform_cli.impact as impact_module
 import autoform_cli.lean as lean_module
 from autoform_cli import __main__ as cli, claims, lean_probe, runtime
 from autoform_cli import _tree_snapshot as tree_snapshot_module
+from autoform_cli._repository import git
 from autoform_cli._tree_snapshot import TreeChangedError
 from autoform_cli.impact import (
     IMPACT_MARKER,
@@ -2595,6 +2597,41 @@ def test_cli_import_impact_outside_git_reports_no_generated_module(tmp_path: Pat
     assert report["claim_targets"] == [_BASE_ID, report["module_claim_target"]]
 
 
+def test_cli_import_impact_ignores_the_user_s_attribute_file(tmp_path: Path, monkeypatch, capsys) -> None:
+    # A mark there covers every repository of that user, so its workers would
+    # leave the module out of every import edit's claims in every project.
+    home = tmp_path / "home"
+    (home / ".config" / "git").mkdir(parents=True)
+    (home / ".config" / "git" / "attributes").write_text("*.lean linguist-generated\n", encoding="utf-8")
+    monkeypatch.setenv("HOME", str(home))
+    monkeypatch.delenv("XDG_CONFIG_HOME", raising=False)
+    project = _blueprint_project(tmp_path, "Demo")
+    lean_root = _stub_lean_root(tmp_path)
+    _git_repository(lean_root, None)
+    _stub_probe(monkeypatch, modules=(ModuleEvidence("Demo", str((lean_root / "Demo.lean").resolve())),))
+
+    code = cli.main(["work", "import-impact", _BASE_ID, "Demo", str(project), "--lean-root", str(lean_root), "--json"])
+
+    output = capsys.readouterr()
+    assert code == 0, output.err
+    report = json.loads(output.out)
+    assert report["module_generated"] is False
+    assert report["claim_targets"] == [_BASE_ID, report["module_claim_target"]]
+
+
+def test_the_generated_check_skips_the_system_attribute_file(tmp_path: Path, monkeypatch) -> None:
+    # Git reads $(prefix)/etc/gitattributes unless GIT_ATTR_NOSYSTEM is set, and
+    # the runner strips inherited GIT_ variables, so the check passes it itself.
+    _git_repository(tmp_path, None)
+    added = {"GIT_CONFIG_COUNT": "1", "GIT_CONFIG_KEY_0": "example.key", "GIT_CONFIG_VALUE_0": "seen"}
+    assert git(tmp_path, "config", "--get", "example.key", environment=added) == "seen"
+    calls = []
+    monkeypatch.setattr(impact_module, "git", lambda _root, *arguments, environment=None: calls.append(environment))
+
+    assert impact_module._linguist_generated(tmp_path, "Demo.lean") is False
+    assert calls == [{"GIT_ATTR_NOSYSTEM": "1"}]
+
+
 @pytest.mark.parametrize("generated", [True, False])
 def test_an_unrelated_workers_claim_on_a_generated_root_does_not_block_an_import_edit(
     tmp_path: Path, monkeypatch, capsys, generated: bool