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

[nybarius]

[repair] union_merge paths are now merged by git's own union merge. Before, a union-merged path was rebuilt line by line: the whole base-side file, then the pull request's new lines appended at the end, with repeated lines collapsed and CRLF line endings lost. git's merge=union works hunk by hunk instead: inside each conflicting hunk it keeps the pull request's lines and then the base branch's, in place, and it keeps everything else exactly as git's ordinary merge would. Because the two results differed, a union-merged step could never equal the tree from a tree provider (or from a git merge) that computes git's union.

How: union_step still runs git's merge first. When every conflicted path is a configured union path (and both sides still have the file), git runs the merge again with merge=union declared for exactly those paths. The declaration is added to the .gitattributes of each path's directory, after whatever that file already declares, in an attribute tree built from the base side's tree. That tree is passed as attr.tree and never committed. So the result is byte for byte what git merge gives when .gitattributes declares merge=union for the path, using the same diff algorithm, the same virtual merge bases and the same handling of trailing newlines. Conflict handling is unchanged: a conflict on any other path, or a union path deleted on one side, still conflicts. merge-tree output is now read with -z, and file contents stay bytes.

rules.union_lines is replaced by rules.union_attributes, the pure function that writes those attribute lines: names are anchored and their pattern characters escaped, and a name with whitespace or quotes becomes a quoted pattern. The union-merge rule now maps to it. The Lean model unionLines and its theorems are unchanged. Union.lean's module text and proofs/README.md now say that unionLines models the set of lines a union keeps, not git's exact byte order. The train doesn't depend on that order, because it compares the landed tree with the gated tree byte for byte.

Tests come first (test: ...). tests/test_union_merge.py compares the union step's file with two references: git merge-file --union on the three versions, and a git merge with merge=union declared in a separate repository. The cases cover insertions at the same spot, interleaved hunks, clean hunks next to a union hunk, deletions, repeated lines, an emptied file, four trailing-newline variants, CRLF and mixed line endings, bytes that aren't valid UTF-8, a file added on both sides, a path with pattern characters and spaces, a directory .gitattributes that declares another merge, and 40 seeded random cases against git's own merge. Two existing expectations changed to git's order: test_history's repair now expects a, lane, main, and the old union_lines unit test is replaced by union_attributes tests. Running make test gives 364 tests passing; lake build for the proofs passes.

[chatgpt-codex-connector]

You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard.