diff options
| author | Pierre-Marie Pédrot | 2019-11-28 18:06:10 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-12-02 09:14:22 +0100 |
| commit | 7fcfef1d6efabfb0c736621499c342d060856499 (patch) | |
| tree | eebaa15a3cbf919c482c98f5fb9df21370ad37bd | |
| parent | 31e109671896ef42653b1fcf239d8ebe1424c3da (diff) | |
Add a script to pin CI developments.
It is useful for the release process, and there is no reason for somebody
to lose time reimplementing it again.
| -rw-r--r-- | dev/doc/release-process.md | 3 | ||||
| -rwxr-xr-x | dev/tools/pin-ci.sh | 46 |
2 files changed, 48 insertions, 1 deletions
diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md index 1c486b024d..ba68501e04 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -75,7 +75,8 @@ in time. - [ ] Pin the versions of libraries and plugins in `dev/ci/ci-basic-overlays.sh` to use commit hashes or tag (or, if it exists, a branch dedicated to compatibility with the corresponding - Coq branch). + Coq branch). You can use the `dev/tools/pin-ci.sh` script to do this + semi-automatically. - [ ] Remove all remaining unmerged feature PRs from the beta milestone. - [ ] Start a new project to track PR backporting. The project should have a "Request X.X+beta1 inclusion" column for the PRs that were diff --git a/dev/tools/pin-ci.sh b/dev/tools/pin-ci.sh new file mode 100755 index 0000000000..dbf54d7f0a --- /dev/null +++ b/dev/tools/pin-ci.sh @@ -0,0 +1,46 @@ +#!/usr/bin/env bash + +# Use this script to pin the commit used by the developments tracked by the CI + +OVERLAYS="./dev/ci/ci-basic-overlay.sh" + +process_development() { + local DEV=$1 + local REPO_VAR="${DEV}_CI_GITURL" + local REPO=${!REPO_VAR} + local BRANCH_VAR="${DEV}_CI_REF" + local BRANCH=${!BRANCH_VAR} + if [[ -z "$BRANCH" ]] + then + echo "$DEV has no branch set, skipping" + return 0 + fi + if [[ $BRANCH =~ ^[a-f0-9]{40}$ ]] + then + echo "$DEV is already set to hash $BRANCH, skipping" + return 0 + fi + echo "Resolving $DEV as $BRANCH from $REPO" + local HASH=$(git ls-remote --heads $REPO $BRANCH | cut -f 1) + if [[ -z "$HASH" ]] + then + echo "Could not resolve reference $BRANCH for $DEV (something went wrong), skipping" + return 0 + fi + read -p "Expand $DEV from $BRANCH to $HASH? [y/N] " -n 1 -r + echo + if [[ $REPLY =~ ^[Yy]$ ]]; then + # use -i.bak to be compatible with MacOS; see, e.g., https://stackoverflow.com/a/7573438/377022 + sed -i.bak -e "s/$BRANCH_VAR:=$BRANCH/$BRANCH_VAR:=$HASH/" $OVERLAYS + fi +} + +# Execute the script to set the overlay variables +. $OVERLAYS + +# Find all variables declared in the base overlay of the form *_CI_GITURL +for REPO_VAR in $(compgen -A variable | grep _CI_GITURL) +do + DEV=${REPO_VAR%_CI_GITURL} + process_development $DEV +done |