[sync] Always overwrote synced files, and deleted each file once, since the last merged sync.

.github/workflows/sync.yml

@@ -54,7 +54,7 @@ jobs:
           repository: SgtSwagrid/github-graph
           path: .github-graph
 
-      # Full history of both repositories is needed to tell the source's changes from the target's.
+      # Full history of the source is needed to find what it has deleted since the last sync.
       - name: Checkout source
         uses: actions/checkout@v4
         with:
@@ -74,6 +74,12 @@ jobs:
       - name: Load config
         run: bash .github-graph/scripts/load-config.sh '${{ toJson(matrix.child) }}'
 
+      - name: Find last sync
+        env:
+          GH_TOKEN: ${{ secrets[matrix.child.token] }}
+          SOURCE_BEFORE: ${{ github.event.before }}
+        run: bash .github-graph/scripts/last-sync.sh
+
       - name: Merge files
         run: bash .github-graph/scripts/merge-files.sh
 

README.md

@@ -84,25 +84,19 @@ in response to which pull requests are automatically opened.
 
 ### Which files are synced
 
-Every file which the source has ever had (outside the [`ignore`](#ignore) list) is given the state it now has in the source:
-its latest version, or none if the source has deleted it.
-But a target may change a synced file itself, or have a file of its own with the same name,
-so the source's state is only given to a file whose last change in the target came from the source.
-That is, the history of both repositories shows that:
-- **its state in the target is one which the source had before the target last changed it**,
-  where a file's absence counts as one of the source's states once the source has deleted it, and
-- **the source has changed it since**.
-
-A file which the target never had is simply added.
-So a file which the target has modified, deleted, or re-added after its deletion was synced is left alone from then on,
-as is one which the target had of its own before the source added it.
-Each is reported in the workflow logs as `Kept`.
-To have a file follow the source again, give it the source's latest version (or delete it, if the source has deleted it),
-and the source's next change to it is synced as usual.
-
-Only a file's last change counts, not how it first arrived:
-a file which the source overwrote, or which another source first added before this one took it over (as when a repository is moved beneath a new parent),
-is the source's as long as its version is one which the source had.
+Every file in the source directory (outside the [`ignore`](#ignore) list) is copied into the target on every sync,
+replacing whatever the target has.
+So a target which wants to keep a file of its own, or a change of its own to a synced file, needs that file ignored.
+
+A file deleted from the source is deleted from the target once, by the first sync after the deletion which the target merges.
+Each sync deletes the files which the source has deleted since the source commit of the last sync from it that the target merged,
+which each sync's commit records in a trailer, and which is read back from the latest merged pull request.
+So:
+- **a sync which is skipped or fails is made up for by the next**, as it covers everything since;
+- **a file which the target re-adds after a deletion was merged is left alone**, as later syncs start after it;
+- **a pull request closed without merging leaves its deletions to be proposed again**, so a deletion is only declined for good by ignoring the file.
+
+Until the target has merged a sync from the source, as at its first, only the deletions made by the push which triggered the sync are synced.
 A renamed file is treated as a deletion of the old name, plus an addition of the new one.
 
 ### One pull request per target
@@ -116,7 +110,7 @@ The sync branch holds one commit for each source directory with changes, on top
 Each sync rebuilds it on the latest target branch,
 reapplying the commits from every other source directory, and replacing its own with its latest changes
 (or dropping it, if there are none).
-As in [which files are synced](#which-files-are-synced), a change isn't reapplied to a file which the target branch has changed itself since the change was made.
+As its own commit holds every change since the last merged sync, the pull request never loses one, however often it's rebuilt.
 Anything else pushed to the sync branch is discarded.
 If several syncs update the branch at once, only one can push at a time,
 and the others rebuild the branch with its changes and try again.
@@ -306,12 +300,11 @@ That being said, if you wanted to tackle these yourself, I'd be a grateful PR re
 
 ### Merge semantics
 
-Files are never "merged": each is either the source's, and follows the source, or the target's, and is left alone
+Updated files are never "merged", but simply overwrite whatever exists downstream,
+so any change made to a synced file downstream is lost at the next sync, unless the file is ignored
 (see [which files are synced](#which-files-are-synced)).
-A file changed downstream stops following the source altogether, however small the change.
 _GitHub Graph_ is only intended for use when the responsibility for each file can be unambiguously associated with a single source repository.
-If several sources nonetheless sync the same file into one target, the first to sync it keeps it,
-unless another has had the very same version.
+If several sources nonetheless sync the same file into one target, whichever synced most recently wins.
 
 ### Platform support
 

scripts/last-sync.sh

@@ -0,0 +1,60 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+# =================================================================================================
+# Finds the source commit from which the target last merged a sync of this source directory,
+# so that `merge-files.sh` deletes the files which the source has deleted since.
+#
+# That commit is named by the SOURCE_TRAILER of this source directory's commit in the most recently
+# merged pull request from the sync branch, which GitHub keeps after a merge however it was done.
+# Until the target has merged one, as at the first sync, it falls back to the commit before the push
+# which triggered this sync, if there is one, so that the deletions made by that push are synced.
+#
+# Environment variables:
+#   - GH_TOKEN:           A token which can read the target repository's pull requests.
+#   - TARGET_REPOSITORY:  The name of the target GitHub repository as 'Username/Repository'.
+#   - TARGET_BRANCH:      The branch into which the sync branch is merged.
+#   - TARGET_SYNC_BRANCH: The name of the branch used to stage the pull request.
+#   - SYNC_TRAILER:       The trailer naming the source directory of a commit on the sync branch.
+#   - SYNC_KEY:           The value of SYNC_TRAILER for this source directory.
+#   - SOURCE_TRAILER:     The trailer naming the source commit which a commit was taken from.
+#   - SOURCE_BEFORE:      The commit before the push which triggered this sync, if any.
+#
+# Output:
+#   - SOURCE_SYNCED: The commit, or nothing if there is none, sent to GITHUB_ENV.
+# =================================================================================================
+
+
+# The message of this source directory's commit in each merged pull request, most recent first,
+# and in it, the source commit it was taken from.
+synced=$(
+  gh pr list \
+    --repo "$TARGET_REPOSITORY" \
+    --head "$TARGET_SYNC_BRANCH" \
+    --base "$TARGET_BRANCH" \
+    --state merged \
+    --limit 20 \
+    --json mergedAt,isCrossRepository,commits \
+    --jq "
+      map(select(.isCrossRepository | not)) | sort_by(.mergedAt) | reverse |
+      [.[].commits[].messageBody | select(contains(\"$SYNC_TRAILER: $SYNC_KEY\"))] |
+      .[0] // \"\"
+    " |
+  sed -n "s/^$SOURCE_TRAILER: \([0-9a-f]*\)$/\1/p" | head -n 1
+)
+
+# The commit before a push which created its branch is all zeros.
+before="${SOURCE_BEFORE:-}"
+if [[ "$before" =~ ^0*$ ]]; then before=""; fi
+
+if [[ -n "$synced" ]]; then
+  echo "Syncing deletions since $synced, the source commit of the last sync which $TARGET_REPOSITORY merged."
+elif [[ -n "$before" ]]; then
+  synced="$before"
+  echo "Syncing deletions since $synced, the commit before this push," \
+    "as no sync which $TARGET_REPOSITORY merged names its source commit."
+else
+  echo "Syncing no deletions, as no sync which $TARGET_REPOSITORY merged names its source commit," \
+    "and there is no commit before this push to compare with."
+fi
+echo "SOURCE_SYNCED=$synced" >> "$GITHUB_ENV"

scripts/load-config.sh

@@ -47,3 +47,19 @@ echo "TARGET_SYNC_BRANCH=${TARGET_SYNC_BRANCH:-sync/github-graph/$TARGET_BRANCH}
 PR_BODY=$(jq -r '.pullRequest.body' <<< "$CHILD")
 delimiter="$(openssl rand -hex 8)"
 { echo "PR_BODY<<$delimiter"; echo "$PR_BODY"; echo "$delimiter"; } >> "$GITHUB_ENV"
+
+# Each commit on the sync branch names the source directory it came from in a trailer, SYNC_TRAILER.
+# This is a key rather than a name, as the source may be private while the target is public.
+# The key is "<source>/<directory>", where the first half is shared by every directory synced from
+# the same branch of the same source repository.
+# A second trailer, SOURCE_TRAILER, names the source commit which the changes were taken from.
+SOURCE_ID="${GITHUB_REPOSITORY_ID:-$(jq -r '.source.repository' <<< "$CHILD")}"
+SOURCE_BRANCH=$(jq -r '.source.branch' <<< "$CHILD")
+SOURCE_ROOT=$(jq -r '.source.root' <<< "$CHILD")
+TARGET_ROOT=$(jq -r '.target.root' <<< "$CHILD")
+digest() { printf '%s\n' "$@" | sha256sum | cut -c1-12; }
+{
+  echo "SYNC_TRAILER=GitHub-Graph-Sync"
+  echo "SYNC_KEY=$(digest "$SOURCE_ID" "$SOURCE_BRANCH")/$(digest "$SOURCE_ID" "$SOURCE_BRANCH" "$SOURCE_ROOT" "$TARGET_ROOT")"
+  echo "SOURCE_TRAILER=GitHub-Graph-Source"
+} >> "$GITHUB_ENV"

scripts/merge-files.sh

@@ -2,27 +2,17 @@
 set -euo pipefail
 
 # =================================================================================================
-# Locally applies the changes from the source repository to the target repository.
-#
-# Every file which the source has ever had in SOURCE_ROOT is given the state it now has in the
-# source: its current version, or none if it was deleted. But the target may change a file itself,
-# or have a file of its own with the same name, so the source's state is only given to a file
-# whose last change in the target came from the source:
-#   a) Its state in the target is one which the source had before the target last changed it.
-#      A file's absence counts as a state which the source had once the source deleted it.
-#   b) The source has changed it since the target last changed it.
-# A file which the target never had is given the source's state.
-# So a file which the target has modified, deleted or re-added is left alone from then on,
-# as is one which the target had of its own before the source added it.
+# Locally applies updates from the source repository into the target repository.
 #
 # Environment variables:
 #   - IGNORE: A JSON-formatted list of file paths to exclude from syncing.
 #   - SOURCE_ROOT: The root directory within the source repository to copy files from.
 #   - TARGET_ROOT: The root directory within the target repository to copy files into.
+#   - SOURCE_SYNCED: The source commit from which the target last merged a sync, or nothing.
 #
 # Requirements:
 #   - source/ should already contain the source repository at the correct branch, with full history.
-#   - target/ should already contain the target repository at the correct branch, with full history.
+#   - target/ should already contain the target repository at the correct branch.
 # =================================================================================================
 
 
@@ -54,95 +44,44 @@ target_path() {
   echo "target/$TARGET_ROOT/${1#"$prefix"}"
 }
 
-# Convert a file name that is relative to SOURCE_ROOT to a normalised path relative to the target repository.
-target_relative_path() {
-  realpath -ms --relative-to=target "$(target_path "$1")"
-}
-
-# Output the first-parent history of a branch, as NUL-separated records of the form:
-#   <commit time> <blob> <status> <file>
-# There is one record for each file changed by each commit, with renames treated as a deletion plus an addition.
-# The blob of a deleted file is ABSENT.
-# Following only the first parent means that each change is dated by when it actually landed on the branch.
-#   - $1: The repository directory.
-#   - $@: Any further arguments are passed to `git log`.
-file_history() {
-  local repo="$1" token timestamp="" blob status file
-  shift
-  while IFS= read -r -d '' token; do
-    if [[ "$token" =~ ^[[:space:]]*:(.*)$ ]]; then
-      read -r _ _ _ blob status <<< "${BASH_REMATCH[1]}"
-      IFS= read -r -d '' file
-      printf '%s\0' "$timestamp" "$blob" "$status" "$file"
-    elif [[ "$token" =~ ^[[:space:]]*([0-9]+)[[:space:]]*$ ]]; then
-      timestamp="${BASH_REMATCH[1]}"
-    fi
-  done < <(
-    git -C "$repo" log --first-parent --diff-merges=first-parent --no-renames --raw --no-abbrev -z --format='%ct' "$@"
-  )
-}
-
-# The state of a file which doesn't exist: the blob which git gives a deleted file, all zeros.
-ABSENT=$(git -C source hash-object --stdin < /dev/null | tr '0-9a-f' '0')
-
-# Whose change was whose can't be told without the full history of both repositories.
-if [[ "$(git -C source rev-parse --is-shallow-repository)" == "true" ||
-      "$(git -C target rev-parse --is-shallow-repository)" == "true" ]]; then
-  echo "::error::Syncing requires the full history of both repositories."
-  exit 1
-fi
-
 # =================================================================================================
-# 1. Read the history of every file which the source has ever had in SOURCE_ROOT:
-#      - STATE: Its state now, i.e. its current blob, or ABSENT if it has been deleted.
-#      - CHANGED: When the source last changed it.
-#      - SINCE: When the source first had each of its states, keyed by "<state>:<file>".
+# 1. Copy all files in the SOURCE_ROOT directory of the source repository
+#    to the TARGET_ROOT directory of the target repository.
+#    Files in the ignore list or outside of SOURCE_ROOT are skipped.
+#    Files which already exist in the target repository are replaced.
 # =================================================================================================
 
-declare -A STATE CHANGED SINCE
-while IFS= read -r -d '' timestamp && IFS= read -r -d '' blob && IFS= read -r -d '' status && IFS= read -r -d '' file; do
-  STATE["$file"]="$blob"
-  CHANGED["$file"]="$timestamp"
-  if [[ -z "${SINCE["$blob:$file"]+_}" ]]; then SINCE["$blob:$file"]="$timestamp"; fi
-done < <(file_history source --reverse -- "$SOURCE_ROOT")
-
-# =================================================================================================
-# 2. Give each file in the target the state it has in the source, if the file is the source's.
-#    Files in the ignore list are skipped.
-# =================================================================================================
-
-for file in "${!STATE[@]}"; do
+while IFS= read -r -d '' file; do
   if is_ignored "${file#"$SOURCE_ROOT/"}"; then
     echo "Skipped: $file"
-    continue
+  else
+    dest=$(target_path "$file")
+    mkdir -p "$(dirname "$dest")"
+    cp "source/$file" "$dest"
+    echo "Copied: $file"
   fi
+done < <(git -C source ls-files -z -- "$SOURCE_ROOT")
 
-  wanted="${STATE[$file]}"
-  dest=$(target_relative_path "$file")
-  current=$(git -C target rev-parse -q --verify "HEAD:$dest") || current="$ABSENT"
-  if [[ "$current" == "$wanted" ]]; then continue; fi
+# =================================================================================================
+# 2. Delete from the target repository the files which the source has deleted since SOURCE_SYNCED,
+#    the commit from which the target last merged a sync, so that each deletion is synced once.
+#    A sync which is skipped or fails is made up for by the next, as it covers everything since.
+#    Files in the ignore list or outside of SOURCE_ROOT are skipped.
+# =================================================================================================
 
-  # When the target last changed the file, dated by when the change landed on its branch,
-  # or nothing if it never had the file.
-  changed_at=$(git -C target log -1 --first-parent --format=%ct -- ":(literal)$dest")
-  if [[ -n "$changed_at" ]]; then
-    since="${SINCE["$current:$file"]:-}"
-    source_changed_at="${CHANGED[$file]}"
-    if [[ -z "$since" ]] || (( since > changed_at )); then
-      echo "Kept: $file (changed in the target)"
-      continue
-    elif (( source_changed_at <= changed_at )); then
-      echo "Kept: $file (changed in the target since the source last changed it)"
-      continue
-    fi
-  fi
+if [[ -z "${SOURCE_SYNCED:-}" ]]; then
+  exit 0
+fi
+if ! git -C source cat-file -e "$SOURCE_SYNCED^{commit}" 2> /dev/null; then
+  echo "::warning::Skipped deletions, as $SOURCE_SYNCED isn't in the history of the source."
+  exit 0
+fi
 
-  if [[ "$wanted" == "$ABSENT" ]]; then
-    rm "target/$dest"
+while IFS= read -r -d '' file; do
+  if is_ignored "${file#"$SOURCE_ROOT/"}"; then continue; fi
+  dest=$(target_path "$file")
+  if [[ -e "$dest" || -L "$dest" ]]; then
+    rm "$dest"
     echo "Deleted: $file"
-  else
-    mkdir -p "$(dirname "target/$dest")"
-    cp "source/$file" "target/$dest"
-    if [[ "$current" == "$ABSENT" ]]; then echo "Added: $file"; else echo "Updated: $file"; fi
   fi
-done
+done < <(git -C source diff -z --name-only --no-renames --diff-filter=D "$SOURCE_SYNCED" HEAD -- "$SOURCE_ROOT")