diff options
Diffstat (limited to 'dev/tools')
| -rwxr-xr-x | dev/tools/change-header | 1 | ||||
| -rwxr-xr-x | dev/tools/merge-pr.sh | 31 | ||||
| -rwxr-xr-x | dev/tools/pin-ci.sh | 46 | ||||
| -rwxr-xr-x | dev/tools/pre-commit | 98 | ||||
| -rwxr-xr-x | dev/tools/update-compat.py | 2 |
5 files changed, 115 insertions, 63 deletions
diff --git a/dev/tools/change-header b/dev/tools/change-header index 59c6f43958..3b0a9d1ef9 100755 --- a/dev/tools/change-header +++ b/dev/tools/change-header @@ -43,6 +43,7 @@ for i in $(git grep --name-only --fixed-strings "$(head -1 $oldheader)"); do mv $i.tmp$$ $i modified=$(expr $modified + 1) else + echo "$i: header unchanged" kept=$(expr $kept + 1) fi rm $i.head.tmp$$ diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index c0a3eeb11c..ce64aebdc7 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -22,7 +22,6 @@ fi RED="\033[31m" RESET="\033[0m" GREEN="\033[32m" -BLUE="\033[34m" YELLOW="\033[33m" info() { echo -e "${GREEN}info:${RESET} $1 ${RESET}" @@ -74,17 +73,17 @@ fi PRDATA=$(curl -s "$API/pulls/$PR") TITLE=$(echo "$PRDATA" | jq -r '.title') -info "title for PR $PR is ${BLUE}$TITLE" +info "title for PR $PR is $TITLE" BASE_BRANCH=$(echo "$PRDATA" | jq -r '.base.label') -info "PR $PR targets branch ${BLUE}$BASE_BRANCH" +info "PR $PR targets branch $BASE_BRANCH" CURRENT_LOCAL_BRANCH=$(git rev-parse --abbrev-ref HEAD) -info "you are merging in ${BLUE}$CURRENT_LOCAL_BRANCH" +info "you are merging in $CURRENT_LOCAL_BRANCH" REMOTE=$(git config --get "branch.$CURRENT_LOCAL_BRANCH.remote") if [ -z "$REMOTE" ]; then - error "branch ${BLUE}$CURRENT_LOCAL_BRANCH${RESET} has not associated remote" + error "branch $CURRENT_LOCAL_BRANCH has not associated remote" error "don't know where to fetch the PR from" error "please run: git branch --set-upstream-to=THE_REMOTE/$CURRENT_LOCAL_BRANCH" exit 1 @@ -96,12 +95,12 @@ if [ "$REMOTE_URL" != "${OFFICIAL_REMOTE_GIT_URL}" ] && \ [ "$REMOTE_URL" != "https://${OFFICIAL_REMOTE_HTTPS_URL}.git" ] && \ [[ "$REMOTE_URL" != "https://"*"@${OFFICIAL_REMOTE_HTTPS_URL}" ]] && \ [[ "$REMOTE_URL" != "https://"*"@${OFFICIAL_REMOTE_HTTPS_URL}.git" ]] ; then - error "remote ${BLUE}$REMOTE${RESET} does not point to the official Coq repo" - error "that is ${BLUE}$OFFICIAL_REMOTE_GIT_URL" - error "it points to ${BLUE}$REMOTE_URL${RESET} instead" + error "remote $REMOTE does not point to the official Coq repo" + error "that is $OFFICIAL_REMOTE_GIT_URL" + error "it points to $REMOTE_URL instead" ask_confirmation fi -info "remote for $CURRENT_LOCAL_BRANCH is ${BLUE}$REMOTE" +info "remote for $CURRENT_LOCAL_BRANCH is $REMOTE" info "fetching from $REMOTE the PR" git remote update "$REMOTE" @@ -112,12 +111,12 @@ if ! git ls-remote "$REMOTE" | grep pull >/dev/null; then fi git fetch "$REMOTE" "refs/pull/$PR/head" COMMIT=$(git rev-parse FETCH_HEAD) -info "commit for PR $PR is ${BLUE}$COMMIT" +info "commit for PR $PR is $COMMIT" # Sanity check: merge to a different branch if [ "$BASE_BRANCH" != "coq:$CURRENT_LOCAL_BRANCH" ]; then - error "PR requests merge in ${BLUE}$BASE_BRANCH${RESET} but you are merging in ${BLUE}$CURRENT_LOCAL_BRANCH" + error "PR requests merge in $BASE_BRANCH but you are merging in $CURRENT_LOCAL_BRANCH" ask_confirmation fi; @@ -132,12 +131,14 @@ if [ "$LOCAL_BRANCH_COMMIT" != "$UPSTREAM_COMMIT" ]; then if git merge-base --is-ancestor -- "$UPSTREAM_COMMIT" "$LOCAL_BRANCH_COMMIT"; then warning "Your branch is ahead of ${REMOTE}." - warning "You should see this warning only if you've just merged another PR and did not push yet." + warning "On master, GitHub's branch protection rule prevents merging several PRs at once." + warning "You should run [git push ${REMOTE}] between each call to the merge script." ask_confirmation else error "Local branch is not up-to-date with ${REMOTE}." error "Pull before merging." - ask_confirmation + # This check should never be bypassed. + exit 1 fi fi @@ -164,7 +165,7 @@ fi STATUS=$(curl -s "$API/commits/$COMMIT/status") if [ "$(echo "$STATUS" | jq -r '.state')" != "success" ]; then - error "CI unsuccessful on ${BLUE}$(echo "$STATUS" | + error "CI unsuccessful on $(echo "$STATUS" | jq -r -c '.statuses|map(select(.state != "success"))|map(.context)')" ask_confirmation fi; @@ -173,7 +174,7 @@ fi; NEEDS_LABELS=$(echo "$PRDATA" | jq -rc '.labels | map(select(.name | match("needs:"))) | map(.name)') if [ "$NEEDS_LABELS" != "[]" ]; then - error "needs:something labels still present: ${BLUE}$NEEDS_LABELS" + error "needs:something labels still present: $NEEDS_LABELS" ask_confirmation fi 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 diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit index ad2f2f93e7..633913aac6 100755 --- a/dev/tools/pre-commit +++ b/dev/tools/pre-commit @@ -7,69 +7,75 @@ set -e dev/tools/check-overlays.sh -if ! git diff --cached --name-only -z | xargs -0 dev/tools/check-eof-newline.sh || - ! git diff-index --check --cached HEAD >/dev/null 2>&1 ; +# Can we check and fix formatting? +# NB: we will ignore errors from ocamlformat as it fails when +# encountering OCaml syntax errors +ocamlformat=$(command -v ocamlformat || echo true) +if [ "$ocamlformat" = true ] then - 1>&2 echo "Auto fixing whitespace issues..." + 1>&2 echo "Warning: ocamlformat is not in path. Cannot check formatting." +fi - # We fix whitespace in the index and in the working tree - # separately to preserve non-added changes. - index=$(mktemp "git-fix-ws-index.XXXXXX") - fixed_index=$(mktemp "git-fix-ws-index-fixed.XXXXXX") - tree=$(mktemp "git-fix-ws-tree.XXXXXX") - 1>&2 echo "Patches are saved in '$index', '$fixed_index' and '$tree'." - 1>&2 echo "If an error destroys your changes you can recover using them." - 1>&2 echo "(The files are cleaned up on success.)" - 1>&2 echo #newline +1>&2 echo "Auto fixing whitespace and formatting issues..." - git diff-index -p --cached HEAD > "$index" - git diff-index -p HEAD > "$tree" +# We fix whitespace in the index and in the working tree +# separately to preserve non-added changes. +index=$(mktemp "git-fix-ws-index.XXXXXX") +fixed_index=$(mktemp "git-fix-ws-index-fixed.XXXXXX") +tree=$(mktemp "git-fix-ws-tree.XXXXXX") +1>&2 echo "Patches are saved in '$index', '$fixed_index' and '$tree'." +1>&2 echo "If an error destroys your changes you can recover using them." +1>&2 echo "(The files are cleaned up on success.)" +1>&2 echo #newline - # reset work tree and index - # NB: untracked files which were not added are untouched - git apply --whitespace=nowarn --cached -R "$index" - git apply --whitespace=nowarn -R "$tree" +git diff-index -p --cached HEAD > "$index" +git diff-index -p HEAD > "$tree" - # Fix index - # For end of file newlines we must go through the worktree +# reset work tree and index +# NB: untracked files which were not added are untouched +if [ -s "$index" ]; then git apply --whitespace=nowarn --cached -R "$index"; fi +if [ -s "$tree" ]; then git apply --whitespace=nowarn -R "$tree"; fi + +# Fix index +# For end of file newlines we must go through the worktree +if [ -s "$index" ]; then 1>&2 echo "Fixing staged changes..." git apply --cached --whitespace=fix "$index" git apply --whitespace=fix "$index" 2>/dev/null # no need to repeat yourself git diff --cached --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix + git diff --cached --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true git add -u 1>&2 echo #newline +fi - # reset work tree - git diff-index -p --cached HEAD > "$fixed_index" - # If all changes were bad whitespace changes the patch is empty - # making git fail. Don't fail now: we fix the worktree first. - if [ -s "$fixed_index" ] - then - git apply --whitespace=nowarn -R "$fixed_index" - fi +# reset work tree +git diff-index -p --cached HEAD > "$fixed_index" +# If all changes were bad whitespace changes the patch is empty +# making git fail. Don't fail now: we fix the worktree first. +if [ -s "$fixed_index" ]; then git apply --whitespace=nowarn -R "$fixed_index"; fi - # Fix worktree +# Fix worktree +if [ -s "$tree" ]; then 1>&2 echo "Fixing unstaged changes..." git apply --whitespace=fix "$tree" git diff --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix + git diff --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true 1>&2 echo #newline +fi - if ! [ -s "$fixed_index" ] - then - 1>&2 echo "No changes after fixing whitespace issues!" - exit 1 - fi - - # Check that we did fix whitespace - if ! git diff-index --check --cached HEAD; - then - 1>&2 echo "Auto-fixing whitespace failed: errors remain." - 1>&2 echo "This may fix itself if you try again." - 1>&2 echo "(Consider whether the number of errors decreases after each run.)" - exit 1 - fi - 1>&2 echo "Whitespace issues fixed!" +if [ -s "$index" ] && ! [ -s "$fixed_index" ]; then + 1>&2 echo "Fixing whitespace and formatting issues cancelled all changes." + exit 1 +fi - # clean up temporary files - rm "$index" "$tree" "$fixed_index" +# Check that we did fix whitespace +if ! git diff-index --check --cached HEAD; then + 1>&2 echo "Auto-fixing whitespace failed: errors remain." + 1>&2 echo "This may fix itself if you try again." + 1>&2 echo "(Consider whether the number of errors decreases after each run.)" + exit 1 fi +1>&2 echo "Whitespace and formatting pass complete." + +# clean up temporary files +rm "$index" "$tree" "$fixed_index" diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py index ddb0362186..666fb6cc91 100755 --- a/dev/tools/update-compat.py +++ b/dev/tools/update-compat.py @@ -1,6 +1,4 @@ #!/usr/bin/env python3 -from __future__ import with_statement -from __future__ import print_function import os, re, sys, subprocess from io import open |