Merge union-merge paths with git's own union merge

CHANGELOG.md

@@ -16,6 +16,17 @@ project intends to follow [Semantic Versioning](https://semver.org/) once it rea
   row carries `tree_source`; the receipt and the round summary carry the totals. Unset,
   nothing changes. See `docs/TREE_PROVIDER.md`.
 
+### Fixed
+
+- `[repair] union_merge` paths are now merged by git's own union merge, byte for byte what
+  `git merge` gives with `merge=union` declared for them in `.gitattributes`: inside each
+  conflicting hunk the pull request's lines and then the base branch's, in place, with
+  repeated lines kept, a line one side deleted left deleted, and line endings and bytes
+  untouched. Previously the whole base-side file came first, the pull request's new lines
+  were appended at the end, repeated lines were collapsed and CRLF line endings were lost,
+  so a union-merged step did not match a tree provider or a `git merge` computing git's
+  union.
+
 ## [0.2.0] - 2026-09-25
 
 ### Changed

README.md

@@ -241,7 +241,7 @@ Unknown keys are refused.
 | `train.interval_seconds` | `300` | sleep between rounds in `watch` |
 | `labels.hold` | `"train:hold"` | label that keeps a pull request out |
 | `repair.enabled` | `true` | push mechanical fixes (union merges, stale base) to pull-request branches |
-| `repair.union_merge` | `[]` | globs of files merged by line union instead of conflicting |
+| `repair.union_merge` | `[]` | globs of files merged by git's union merge (`merge=union`) instead of conflicting |
 | `history.order` | `"off"` | `"tests-first"` refuses code committed before its tests |
 | `history.reland` | `true` | re-land refused histories in order instead of holding them |
 | `history.tests`, `history.docs` | common globs | how paths are classified for the history check |

proofs/BraidedTrain/Union.lean

@@ -3,11 +3,13 @@ import BraidedTrain.Braid
 /-!
 # BraidedTrain.Union — the line-level union merge as a model step
 
-`svrf.rules.union_lines(theirs, ours)` keeps the base side's lines in order and appends each
-line of the pull request's side that is not already there, once. `unionLines` is that
-function on lists of lines. `git.RealGit.union_step` applies it only on configured union
-paths, and only when every path git's merge reports as conflicted is a union path; any
-other conflicted path keeps the two heads apart. Finite lists, no Mathlib.
+`unionLines theirs ours` keeps the base side's lines in order and appends each line of the
+pull request's side that is not already there, once: the union of two line lists, as a
+model. `git.RealGit.union_step` applies a union only on configured union paths, and only
+when every path git's merge reports as conflicted is a union path; any other conflicted
+path keeps the two heads apart. The code's union is git's own (`merge=union`), declared
+for those paths through `svrf.rules.union_attributes`; see the modelling boundary below.
+Finite lists, no Mathlib.
 
 1. `count_unionLines`: the count of a line after a union is its count on the base side,
    plus one exactly when the base side lacks it and the pull request's side has it. Every
@@ -30,6 +32,12 @@ other conflicted path keeps the two heads apart. Finite lists, no Mathlib.
 Modelling boundary: git merges a non-union file edited on both sides hunk by hunk; this
 model treats such a path as a conflict (the coarser, path-level reading used by
 `apply_comm_of_disjoint`), and it treats every edit of a union path as a union of lines.
+git's union merge is also hunk by hunk: inside each conflicting hunk it keeps the pull
+request's lines and then the base side's, outside them it is git's ordinary merge, and it
+neither drops repeated lines nor restores lines one side deleted. `unionLines` is the
+line-set reading of that merge, not its exact byte order; the train never relies on that
+order, because it fixes the fold order once, replays it at landing, and compares the
+landed tree with the gated tree byte for byte.
 -/
 
 set_option linter.unusedSimpArgs false
@@ -43,7 +51,7 @@ variable {Line : Type} [DecidableEq Line]
 def addLine (acc : List Line) (l : Line) : List Line :=
   if l ∈ acc then acc else acc ++ [l]
 
-/-- `union_lines(theirs, ours)`: the base side's lines, then each new line of ours, once. -/
+/-- The line-set union: the base side's lines, then each new line of ours, once. -/
 def unionLines (theirs ours : List Line) : List Line :=
   ours.foldl addLine theirs
 

proofs/README.md

@@ -64,7 +64,7 @@ states it and the function or method that enforces it in the running train.
 | `interleaved-owners` | `interleaved_landing` | `choose_families` |
 | `repair-mechanical` | `retry_iff` | `repair_class` |
 | `ordered-reland` | `reland_tree` | `reland_class` |
-| `union-merge` | `change_comm` | `union_lines` |
+| `union-merge` | `change_comm` | `union_attributes` |
 | `speculative-stacking` | `stack_lands_gated` | `Train.round` |
 | `speculation-void` | `stackStatus_void_iff` | `Train.round` |
 | `bisect-holds-exactly-red` | `settle_outcome` | `Train.settle_red` |
@@ -88,7 +88,7 @@ or rename a rule, update the table above and the code together; the test fails o
 | `BraidedTrain/Braid.lean` | The ungated-window invariant (`AllGated`, `mains`); retry as a function of a read key; commutation of disjoint writes (`strands_comm`). |
 | `BraidedTrain/Interleaving.lean` | Two owners landing path-disjoint families interleaved still land one tree (`interleaved_landing`); when a gate's own read paths miss the other owner's writes, no joint gate is needed (`two_owners_end_gated`). |
 | `BraidedTrain/Reland.lean` | Re-landing a history as tests-then-code-then-docs commits lands the identical tree (`reland_tree`), so any tree-reading gate's verdict is unchanged (`reland_gate`). |
-| `BraidedTrain/Union.lean` | The line-level union merge (`unionLines`, the model of `union_lines`): exact associativity (`unionLines_assoc`), commutation up to line order (`unionLines_comm`, sharp by `union_order_visible`), and at the path level `change_comm` / `family_perm` under `UnionOnlyOverlap`, the union repair's hypothesis. |
+| `BraidedTrain/Union.lean` | The line-level union merge (`unionLines`, the line-set model of git's `merge=union`, which `union_attributes` declares for the union paths): exact associativity (`unionLines_assoc`), commutation up to line order (`unionLines_comm`, sharp by `union_order_visible`), and at the path level `change_comm` / `family_perm` under `UnionOnlyOverlap`, the union repair's hypothesis. |
 | `BraidedTrain/Stacking.lean` | Speculative stacking: families gated on the fold of every family before them land gated trees at every family boundary (`stack_lands_gated`); a stacked verdict does not carry past a red family (`stack_fold_through`, `stacked_verdict_does_not_carry`); the round's bookkeeping voids exactly the families above the first red one (`stackStatus_void_iff`, `stackStatus_landed_iff`, `stackStatus_bisected_iff`). |
 | `BraidedTrain/Bisection.lean` | Bisection of a red family (`settle`, the model of `Train.settle_red`) terminates (well-founded on family length), holds exactly the bad pull requests and lands the rest under a monotone gate (`settle_outcome`), and costs at most `2·r·⌈log₂ n⌉ + 1` gates including the family's own (`settle_gates_le`, `bisection_gates_le`). |
 | `BraidedTrain/Families.lean` | The Bron–Kerbosch recursion of `families`, with arbitrary pivot and iteration order: every family it reports is a maximal compatible set (`bk_maximal`), so the family `choose_families` keeps holds no conflicting pair and every pull request left out conflicts with a kept one (`chosen_family_maximal`). With a pivot drawn from the candidates or excluded nodes (the code's rule, `codePivot_mem`) and an order visiting every node, it reports every maximal compatible set (`bk_complete`), so the first family of the size-sorted list is a maximum compatible set (`chosen_family_maximum`). |

src/svrf/git.py

@@ -18,7 +18,7 @@
 
 from .errors import ReadFailed
 from .redact import redact
-from .rules import union_lines
+from .rules import union_attributes
 
 
 @dataclass
@@ -63,6 +63,10 @@ def _run(self, *args, input: str | None = None, env: dict | None = None) -> subp
         return subprocess.run(["git", "-C", str(self.root), *args], capture_output=True, text=True, input=input,
                               env=env or self.env)
 
+    def _raw(self, *args, input: bytes | None = None) -> subprocess.CompletedProcess:
+        """`_run` with bytes in and out: file contents and paths exactly as git holds them."""
+        return subprocess.run(["git", "-C", str(self.root), *args], capture_output=True, input=input, env=self.env)
+
     def _out(self, *args, input: str | None = None, env: dict | None = None) -> str:
         done = self._run(*args, input=input, env=env)
         if done.returncode != 0:
@@ -152,9 +156,11 @@ def pairs(self, rows: list[dict], base: str) -> dict:
 
     def union_step(self, acc: str, head: str, message: str, union: Callable[[str], bool] | None = None) -> Step:
         """Merge `acc` (the base branch, or the fold so far) into the pull request `head`:
-        git's merge with the pull request as ours and the base as theirs, configured
-        union-merge paths resolved by `union_lines`, committed with parents (head, acc)
-        exactly as `git merge <base>` on the branch would."""
+        git's merge with the pull request as ours and the base as theirs, committed with
+        parents (head, acc) exactly as `git merge <base>` on the branch would. When every
+        path that merge leaves conflicted is a configured union-merge path, the merge is
+        made again by git with `merge=union` declared for those paths, so each is git's own
+        union merge, byte for byte what `.gitattributes` declaring it would give."""
         union = union or self.union
         try:
             if self.is_ancestor(acc, head):
@@ -163,34 +169,61 @@ def union_step(self, acc: str, head: str, message: str, union: Callable[[str], b
                 return Step("CLEAN", commit=acc, tree=self.tree(acc))
             # Same attribute-source fix as `merge_preview`: read .gitattributes from `acc`
             # (the base/theirs side), never from this clone's checkout.
-            done = self._run("-c", f"attr.tree={acc}", "merge-tree", "--write-tree", head, acc)
-            if done.returncode not in (0, 1):
-                return Step("FAILED", reason=f"MERGE_TREE_FAILED:{done.returncode}")
-            lines = done.stdout.split("\n")
-            tree = lines[0].strip()
-            if done.returncode == 1:
-                stages: dict[str, dict[int, tuple[str, str]]] = {}
-                for line in lines[1:]:
-                    if not line.strip():
-                        break
-                    meta, _, path = line.partition("\t")
-                    mode, sha, stage = meta.split()
-                    stages.setdefault(path, {})[int(stage)] = (mode, sha)
+            code, tree, stages = self._merge_tree(acc, head, acc)
+            if code == 1:
                 other = sorted(p for p in stages if not union(p))
                 if other:
                     return Step("CONFLICT", conflicts=other)
-                for path, by_stage in stages.items():
+                for path, by_stage in sorted(stages.items()):
                     if 2 not in by_stage or 3 not in by_stage:
                         return Step("CONFLICT", conflicts=[path])
-                    ours = self._out("cat-file", "blob", by_stage[2][1])
-                    theirs = self._out("cat-file", "blob", by_stage[3][1])
-                    blob = self._out("hash-object", "-w", "--stdin", input=union_lines(theirs=theirs, ours=ours))
-                    tree = self._overlay_tree(tree, {path: (by_stage[2][0], blob)})
+                code, tree, stages = self._merge_tree(self._union_attribute_tree(acc, sorted(stages)), head, acc)
+                if code == 1:
+                    return Step("CONFLICT", conflicts=sorted(stages))
             commit = self._out("commit-tree", tree, "-p", head, "-p", acc, "-m", message)
             return Step("CLEAN", commit=commit, tree=tree)
         except ReadFailed as failure:
             return Step("FAILED", reason=failure.reason)
 
+    def _merge_tree(self, attributes: str, ours: str, theirs: str) -> tuple[int, str, dict[str, dict[int, str]]]:
+        """git's merge of `ours` and `theirs` with .gitattributes read from `attributes`:
+        (0 clean or 1 conflicted, the tree, each conflicted path's stages)."""
+        done = self._raw("-c", f"attr.tree={attributes}", "merge-tree", "--write-tree", "-z", "--no-messages",
+                         ours, theirs)
+        if done.returncode not in (0, 1):
+            raise ReadFailed(f"MERGE_TREE_FAILED:{done.returncode}")
+        fields = done.stdout.split(b"\0")
+        tree = fields[0].decode().strip()
+        stages: dict[str, dict[int, str]] = {}
+        if done.returncode == 1:
+            for field in fields[1:]:
+                if not field:
+                    break
+                meta, _, path = field.partition(b"\t")
+                _mode, sha, stage = meta.decode().split()
+                stages.setdefault(path.decode("utf-8", "surrogateescape"), {})[int(stage)] = sha
+        return done.returncode, tree, stages
+
+    def _union_attribute_tree(self, commit: str, paths: list[str]) -> str:
+        """`commit`'s tree with `merge=union` declared for `paths`, each in the
+        `.gitattributes` of its own directory after whatever that file already declares:
+        an attribute source for git's merge, never committed."""
+        by_dir: dict[str, list[str]] = {}
+        for path in paths:
+            folder, _, name = path.rpartition("/")
+            by_dir.setdefault(folder, []).append(name)
+        sets: dict[str, tuple[str, str] | None] = {}
+        for folder, names in by_dir.items():
+            attributes = f"{folder}/.gitattributes" if folder else ".gitattributes"
+            read = self._raw("cat-file", "blob", f"{commit}:{attributes}")
+            text = read.stdout.decode("utf-8", "surrogateescape") if read.returncode == 0 else ""
+            body = union_attributes(text, names).encode("utf-8", "surrogateescape")
+            written = self._raw("hash-object", "-w", "--stdin", input=body)
+            if written.returncode != 0:
+                raise ReadFailed(f"GIT_FAILED:hash-object:{written.returncode}")
+            sets[attributes] = ("100644", written.stdout.decode().strip())
+        return self._overlay_tree(self.tree(commit), sets)
+
     repair_step = union_step
 
     def _overlay_tree(self, base_tree: str, sets: dict[str, tuple[str, str] | None]) -> str:

src/svrf/rules.py

@@ -34,7 +34,7 @@
     "interleaved-owners": {"lean": "interleaved_landing", "check": "choose_families"},
     "repair-mechanical": {"lean": "retry_iff", "check": "repair_class"},
     "ordered-reland": {"lean": "reland_tree", "check": "reland_class"},
-    "union-merge": {"lean": "change_comm", "check": "union_lines"},
+    "union-merge": {"lean": "change_comm", "check": "union_attributes"},
     "speculative-stacking": {"lean": "stack_lands_gated", "check": "Train.round"},
     "speculation-void": {"lean": "stackStatus_void_iff", "check": "Train.round"},
     "bisect-holds-exactly-red": {"lean": "settle_outcome", "check": "Train.settle_red"},
@@ -49,17 +49,21 @@
 # --------------------------------------------------------------------------- merging
 
 
-def union_lines(*, theirs: str, ours: str) -> str:
-    """A union-merged file: the base branch's lines in order, then the lines the pull
-    request adds, each once. Suited to files whose lines are independent entries: import
-    indexes, requirement lists, changelog bullets."""
-    out = theirs.splitlines()
-    seen = set(out)
-    for line in ours.splitlines():
-        if line not in seen:
-            out.append(line)
-            seen.add(line)
-    return "\n".join(out) + "\n"
+def union_attributes(text: str, names) -> str:
+    """A directory's `.gitattributes` body (`text`, possibly empty) with git's union merge
+    (`merge=union`) declared for each file name in `names`, after everything `text` already
+    declares, so for those files it is the line git reads last. Each name is anchored to the
+    directory and its pattern characters escaped; a name with whitespace, a quote or a
+    control character is written as a quoted pattern."""
+    out = text if not text or text.endswith("\n") else text + "\n"
+    for name in sorted(set(names)):
+        pattern = "/" + re.sub(r"([\\*?\[])", r"\\\1", name)
+        if any(c.isspace() or c == '"' or ord(c) < 32 or ord(c) == 127 for c in pattern):
+            quoted = pattern.replace("\\", "\\\\").replace('"', '\\"')
+            quoted = re.sub(r"[\x00-\x1f\x7f]", lambda m: "\\%03o" % ord(m.group()), quoted)
+            pattern = f'"{quoted}"'
+        out += f"{pattern} merge=union\n"
+    return out
 
 
 def chunk(items: list, size: int) -> list[list]:

tests/test_history.py

@@ -175,7 +175,7 @@ def test_the_repair_pushes_a_union_merge_while_the_branch_is_checked_out_elsewhe
         self.assertEqual(pushed, step.commit)
         self.assertEqual(g.parents(step.commit), [head, main])
         text = git(self.work, "cat-file", "-p", f"{step.commit}:requirements.txt")
-        self.assertEqual(text.splitlines(), ["a", "main", "lane"])
+        self.assertEqual(text.splitlines(), ["a", "lane", "main"])
         rows = history.dispositions(g, main, step.commit, KIND)
         self.assertEqual([r["disposition"] for r in rows], ["TESTS", "CODE", "MERGE"])
 

tests/test_train.py

@@ -30,11 +30,6 @@ def train(repo, gh, gate, tmp, clock=None, **kw):
 
 
 class PureReads(unittest.TestCase):
-    def test_union_lines_keep_base_order_then_the_additions_once(self):
-        base = "a\nb\nm\n"
-        head = "a\nb\nl\n"
-        self.assertEqual(rules.union_lines(theirs=base, ours=head), "a\nb\nm\nl\n")
-
     def test_a_rate_limit_is_a_read_failure_never_a_conflict(self):
         with self.assertRaises(RateLimited) as caught:
             classify_gh_failure(1, "GraphQL: API rate limit already exceeded for user ID 7.")