Leave generated import roots that Git marks linguist-generated out of import-edit claims

CHANGELOG.md

@@ -61,6 +61,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'
+  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
   Mathlib row, as text without a link, so a `mathlib: true` article names the
   declaration it restates (#388).

autoform_cli/README.md

@@ -890,7 +890,9 @@ JSON uses `autoform-module-import-impact/v1`, with `module_graph_revision` and
 `module_scope` (`loaded-root-library-graph` or `import-closure`). `article` is
 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`. `affected_claim_targets` are downstream
+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.
 `affected_articles` lists each article that names, or owns through the parent

autoform_cli/_repository.py

@@ -10,7 +10,7 @@
 outside it or the variable is empty; ``repository_top_level`` places the root
 in its working tree. Every Git command here runs without the caller's ``GIT_*``
 variables, so the given directory alone selects the repository; the debrief
-store and ``autoform --version`` run ``git`` too.
+store, ``work import-impact`` and ``autoform --version`` run ``git`` too.
 """
 
 from __future__ import annotations

autoform_cli/impact.py

@@ -22,6 +22,9 @@
 and refuses any content or source-identity change. ``work import-impact`` takes
 the loaded module graph from Lean and binds every node to its captured root
 source and configured root-package artifact, so a dependency cannot shadow it.
+A module whose file Git attributes mark ``linguist-generated`` is a generated
+import root: its header belongs to the repository's generator, so the import
+edit does not claim it.
 Under ``--module-scope import-closure`` a file is a candidate when its text
 contains every component of a candidate's name, repeated until no new file
 matches (:func:`import_closure`), and Lean loads what the candidates import.
@@ -39,6 +42,7 @@
 from pathlib import Path
 
 from . import lean_probe
+from ._repository import git
 from ._tree_snapshot import TreeSnapshotError
 from .claims import author_claim_key
 from .lean import IndexedSourceSnapshot, LeanSourceError, bind_project_source_snapshot, resolve_lean_root
@@ -903,6 +907,7 @@ class ModuleImportImpactReport:
     affected_claim_targets: tuple[str, ...]
     claim_targets: tuple[str, ...]
     module_scope: str = MODULE_IMPORT_SCOPE
+    module_generated: bool = False
 
     @property
     def selected_affected(self) -> bool:
@@ -954,6 +959,7 @@ def as_dict(self) -> dict[str, object]:
             "module": self.module,
             "module_claim_target": self.module_claim_target,
             "module_claim_key": self.module_claim_key,
+            "module_generated": self.module_generated,
             "selected_affected": self.selected_affected,
             "article_local": self.article_local,
             "affected_modules": list(self.affected_modules),
@@ -1145,6 +1151,7 @@ def compute_module_import_impact(
     lean_source_revision: str = "",
     module_scope: str = MODULE_IMPORT_SCOPE,
     declaration_modules: Mapping[str, str] | None = None,
+    module_generated: bool = False,
 ) -> ModuleImportImpactReport:
     """Return the reverse-import scope of changing ``module`` imports.
 
@@ -1155,7 +1162,8 @@ def compute_module_import_impact(
     roots; this scope does not list them. It never refuses the edit merely
     because the scope is larger than one article. ``declaration_modules`` maps
     a name to the module whose source declares it; an unresolved name it places
-    in an unaffected module is not reported.
+    in an unaffected module is not reported. A ``module_generated`` header
+    belongs to the repository's generator, so it is not a claim target.
     """
 
     if module not in modules:
@@ -1244,10 +1252,11 @@ def owners(record: ConstantRecord) -> tuple[str, ...]:
             }
         )
     )
-    # The import edit itself owns only its selected article and module header.
-    # Other article claims are reported separately: they block only when live,
-    # or become required when validation shows that their content must change.
-    claim_targets = (selected.claim_target, module_claim_target)
+    # The import edit itself owns only its selected article and module header,
+    # unless a generator writes the header. Other article claims are reported
+    # separately: they block only when live, or become required when
+    # validation shows that their content must change.
+    claim_targets = (selected.claim_target,) if module_generated else (selected.claim_target, module_claim_target)
     return ModuleImportImpactReport(
         source_revision=source_revision,
         lean_source_revision=lean_source_revision,
@@ -1263,6 +1272,7 @@ def owners(record: ConstantRecord) -> tuple[str, ...]:
         affected_claim_targets=affected_claim_targets,
         claim_targets=claim_targets,
         module_scope=module_scope,
+        module_generated=module_generated,
     )
 
 
@@ -1456,6 +1466,7 @@ class _ImpactEvidence:
     modules: Mapping[str, ModuleEvidence]
     locate: Locator
     declaration_modules: Mapping[str, str] | None = None
+    module_generated: bool = False
 
 
 def _load_impact_evidence(
@@ -1589,6 +1600,11 @@ def _load_impact_evidence(
             snapshot=source_snapshot,
             required_modules=required_modules,
         )
+    module_generated = False
+    if require_modules and module is not None:
+        paths = _module_source_paths(libraries, source_snapshot, strict=True)
+        relative = {_name_key(name): path for name, path in paths.items()}.get(_name_key(module))
+        module_generated = relative is not None and _linguist_generated(root, relative)
 
     return _ImpactEvidence(
         source_revision=source_revision,
@@ -1599,6 +1615,7 @@ def _load_impact_evidence(
         modules=module_evidence,
         locate=_locator(libraries, source_snapshot),
         declaration_modules=declaration_modules,
+        module_generated=module_generated,
     )
 
 
@@ -1671,9 +1688,26 @@ def module_import_impact(
         lean_source_revision=evidence.lean_source_revision,
         module_scope=module_scope,
         declaration_modules=evidence.declaration_modules,
+        module_generated=evidence.module_generated,
     )
 
 
+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.
+    """
+
+    try:
+        output = git(root, "check-attr", "--cached", "linguist-generated", "--", relative)
+    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")
+
+
 def _locator(
     libraries: tuple[LeanLibrary, ...],
     snapshot: IndexedSourceSnapshot,
@@ -1768,7 +1802,8 @@ def format_module_import_impact(report: ModuleImportImpactReport) -> list[str]:
         f"Lean build revision: {report.build_revision}",
         f"Module graph revision: {report.module_graph_revision}",
         f"Module scope: {report.module_scope}",
-        f"Module claim target: {report.module_claim_target} (key {report.module_claim_key})",
+        f"Module claim target: {report.module_claim_target} (key {report.module_claim_key})"
+        + (", not claimed: linguist-generated; regenerate it, don't edit it" if report.module_generated else ""),
         "Affected project modules: " + ", ".join(report.affected_modules),
         "Removing an import can also drop modules that only imports bring into the build; "
         "this reverse-import scope does not list them.",

skills/formalize/references/claims.md

@@ -31,7 +31,7 @@ Compare the import-impact report's claim keys with `autoform claim list`, as the
 [CLI reference](../../../autoform_cli/README.md#work-import-impact) describes: another
 owner's live affected claim is a conflict, malformed evidence is unverifiable,
 and an expired valid claim is not active. Before the edit, atomically acquire
-the required article and module `claim_targets`; an already-held same-worker
+the report's `claim_targets`; an already-held same-worker
 article claim is upgraded, not released first. Recheck affected keys after
 acquisition and before integration; these checks are best-effort coordination,
 not a lock on downstream articles. Before repairing any article that actually
@@ -43,21 +43,20 @@ hand off, and release the full import claim set together.
 
 ## Generated import roots
 
-Unlike other import edits, a root that the repository's deterministic generator
-writes from the tracked modules, such as a `Lib.lean` that imports every module
-of a folder, is not part of a worker's long-held claim set; a root written or
-edited by hand, or one with no such generator, keeps the import-edit rules
-above. A worker may regenerate it in its worktree to build and check its result,
-without claiming it, and may commit it; on a conflict in it during a rebase or
-merge, regenerate it from the merged tree. Before landing a commit that changes
-the root, the integrator acquires the root's module `claim_target` together
-with the complete set it holds, in one command under that set's worker ID, then
-regenerates it from the integrated tree. If another owner holds the root, follow
-the refusal rule under Import edits:
-release the complete held set before waiting, or keep it and hand off the
-verified candidate. Then re-run `autoform work import-impact` and the checks on
-the result, and release the root's claim with the rest of the set once the
-result is visible, as the next section requires.
+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
+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
+no change. Before landing, re-run `work import-impact` and the repository's
+checks on the result; an affected target another owner holds is still a
+conflict. Any other root, whatever its header says, keeps the import-edit rules.
 
 ## Integration and handoff
 
@@ -78,4 +77,4 @@ continue it, acquires the complete set under its own ID and, before integrating,
 repeats Formalize's pre-edit reload of `work context`. Release the complete set
 once the result is visible that way, or when abandoning the leaf without a
 candidate. For ordinary work that set is just the article; for an import edit it
-also includes the module and any validated expansion.
+is the report's `claim_targets` and any validated expansion.