diff options
author | Vincent Ambo <mail@tazj.in> | 2022-05-25T16·17+0200 |
---|---|---|
committer | tazjin <tazjin@tvl.su> | 2022-05-26T08·41+0000 |
commit | 74c422d0a0ff9040ae68629c9657f77330ae8727 (patch) | |
tree | 8ef4197aca89dc956b66d35c9961548e8cf1b11d /tools/releases/default.nix | |
parent | 6a17cf232d5a13b3ec96b0dd0320d8c6858c35a5 (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>
Diffstat (limited to 'tools/releases/default.nix')
-rw-r--r-- | tools/releases/default.nix | 37 |
1 files changed, 37 insertions, 0 deletions
diff --git a/tools/releases/default.nix b/tools/releases/default.nix new file mode 100644 index 000000000000..2d00a2b01fb0 --- /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}' + ''; + }; +} |