[sync] Synced only the children whose source directory a push changed.

.github/workflows/sync.yml

@@ -2,6 +2,7 @@ name: Sync
 
 on:
   push:
+    branches: [ main ]
   workflow_dispatch:
   workflow_call:
 
@@ -31,6 +32,7 @@ jobs:
         id: parse
         env:
           DEFAULT_BRANCH: ${{ github.event.repository.default_branch }}
+          SOURCE_BEFORE: ${{ github.event.before }}
         run: bash .github-graph/scripts/parse-config.sh
 
   # Synchronise each target repository.

README.md

@@ -39,6 +39,7 @@ name: Sync
 
 on:
   push:
+    branches: [ main ]
   workflow_dispatch:
 
 jobs:
@@ -47,9 +48,9 @@ jobs:
     secrets: inherit
 ```
 
-As written, this will trigger the synchronisation procedure when (any branch of) the source repository is pushed to.
-It doesn't matter now if you only want to sync from one branch (e.g. `main`), this is configured later.
-Nevertheless, feel free to modify the trigger to suit your needs.
+As written, this will trigger the synchronisation procedure when `main` is pushed to.
+Which branches are synced from is configured later (see [`source`](#source)),
+but list each of them here too: a push to any other branch would find nothing to sync, yet still start a job to find that out.
 
 ### 2. Add a configuration file
 
@@ -81,6 +82,8 @@ This is true both in the [git](https://git-scm.com/docs/git-push) sense and in t
 Changes _pushed_ to the source are _eagerly_ propagated (i.e. _pushed_) downstream.
 A [GitHub Actions](https://github.com/features/actions) workflow in the source repository listens for pushes to a designated branch and directory,
 in response to which pull requests are automatically opened.
+A push syncs only into the targets whose source directory it changed,
+or into every target if it changed the configuration file, as does running the workflow by hand.
 
 ### Which files are synced
 
@@ -92,7 +95,8 @@ A file deleted from the source is deleted from the target once, by the first syn
 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 sync which is skipped or fails is made up for by the next**, as it covers everything since
+  (run the workflow by hand to sync every target without waiting for a push to its source directory);
 - **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.
 

scripts/parse-config.sh

@@ -10,6 +10,8 @@ set -euo pipefail
 #   - GITHUB_REPOSITORY: The source repository in the form owner/name.
 #   - GITHUB_REF_NAME:   The name of the branch that was pushed to.
 #   - GITHUB_SHA:        The commit SHA that triggered the workflow.
+#   - GITHUB_EVENT_NAME: The event that triggered the workflow.
+#   - SOURCE_BEFORE:     The commit before the push which triggered this sync, if any.
 #
 # Output:
 #   - children: A JSON list of downstream repositories to be updated, sent to GITHUB_OUTPUT.
@@ -20,10 +22,22 @@ CONFIG_PATH="${CONFIG_PATH:-.github/graph.json}"
 
 SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)"
 
+# The files which the push changed, or null to sync every child. A sync which a push skips is made
+# up for by the next, so a child need only sync when the push changed its source directory. Any
+# other run syncs every child: one started by hand, or a push which created its branch, or whose
+# earlier commit can't be fetched to compare with.
+CHANGED=null
+BEFORE="${SOURCE_BEFORE:-}"
+if [[ "${GITHUB_EVENT_NAME:-}" == "push" && ! "$BEFORE" =~ ^0*$ ]] \
+  && git fetch --quiet --no-tags --depth=1 origin "$BEFORE"; then
+  CHANGED=$(git diff --name-only --no-renames "$BEFORE" "$GITHUB_SHA" | jq -R . | jq -s -c .)
+fi
+
 CHILDREN=$(jq \
   -c \
   --rawfile default_pr_body "$SCRIPT_DIR/../templates/pull-request-body.md" \
   --arg config_path "$CONFIG_PATH" \
+  --argjson changed "$CHANGED" \
   '
     (. | del(.children)) as $global |
     (.children // []) |
@@ -74,7 +88,16 @@ CHILDREN=$(jq \
     ) |
 
     # Filter to only children that are triggered by the current branch.
-    map(select(.source.branch == $ENV.GITHUB_REF_NAME))
+    map(select(.source.branch == $ENV.GITHUB_REF_NAME)) |
+
+    # And to those whose source directory the push changed, unless it changed this file,
+    # which may change what any child syncs.
+    if $changed == null or any($changed[]; . == $config_path) then . else
+      map(select(
+        (.source.root | ltrimstr("./") | rtrimstr("/")) as $root |
+        $root == "" or $root == "." or any($changed[]; startswith($root + "/"))
+      ))
+    end
   ' \
   "$CONFIG_PATH" \
 )