about summary refs log tree commit diff
diff options
context:
space:
mode:
authorVincent Ambo <mail@tazj.in>2022-05-25T16·17+0200
committertazjin <tazjin@tvl.su>2022-05-26T08·41+0000
commit74c422d0a0ff9040ae68629c9657f77330ae8727 (patch)
tree8ef4197aca89dc956b66d35c9961548e8cf1b11d
parent6a17cf232d5a13b3ec96b0dd0320d8c6858c35a5 (diff)
feat(tools/releases): Add release helper for mirroring to Github r/4120
This adds an extra step definition which can push the result of
running a josh filter on the repository to Github.

Change-Id: I1f93ae78e1bf452fbd1b21ce943a60acc85c944f
Reviewed-on: https://cl.tvl.fyi/c/depot/+/5666
Tested-by: BuildkiteCI
Reviewed-by: sterni <sternenseemann@systemli.org>
Reviewed-by: grfn <grfn@gws.fyi>
-rw-r--r--tools/releases/default.nix37
1 files changed, 37 insertions, 0 deletions
diff --git a/tools/releases/default.nix b/tools/releases/default.nix
new file mode 100644
index 0000000000..2d00a2b01f
--- /dev/null
+++ b/tools/releases/default.nix
@@ -0,0 +1,37 @@
+# Definitions for simple release mechanisms from depot.
+{ depot, lib, pkgs, ... }:
+
+let
+  inherit (lib.strings) makeBinPath sanitizeDerivationName;
+in
+{
+  # Use a josh filter to push a certain subset of canon to another git
+  # repository.
+  #
+  # This expects, of course, that the remote repository has granted
+  # push access to the CI SSH key.
+  filteredGitPush = { filter, remote, ref ? "refs/heads/canon" }: {
+    label = ":git: push '${filter}' to external git repository";
+    branches = [ "refs/heads/canon" ];
+    postBuild = true;
+
+    command = pkgs.writeShellScript "${sanitizeDerivationName filter}-push" ''
+      set -e
+      export PATH="${makeBinPath [ pkgs.git depot.third_party.josh ]}:$PATH"
+
+      echo 'Filtering depot through ${filter}'
+      josh-filter '${filter}'
+
+      echo 'Fetching remote to check if a push is needed'
+      git fetch '${remote}' '${ref}'
+
+      if git merge-base --is-ancestor FILTERED_HEAD FETCH_HEAD; then
+        echo 'Commit already present, nothing to push.'
+        exit 0
+      fi
+
+      echo 'Pushing filtered repository to ${remote}:${ref}'
+      git push '${remote}' 'FILTERED_HEAD:${ref}'
+    '';
+  };
+}