Merge PR #6568: Cleanup scripts

6 files changed, 101 insertions, 98 deletions

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 232b8a56e..628e89291 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -4,141 +4,143 @@
 
 # Maybe we should just use Ruby to have real objects...
 
+# : "${foo:=bar}" sets foo to "bar" if it is unset or null
+
 ########################################################################
 # MathComp
 ########################################################################
-: ${mathcomp_CI_BRANCH:=master}
-: ${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp.git}
+: "${mathcomp_CI_BRANCH:=master}"
+: "${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp.git}"
 
 ########################################################################
 # UniMath
 ########################################################################
-: ${UniMath_CI_BRANCH:=master}
-: ${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath.git}
+: "${UniMath_CI_BRANCH:=master}"
+: "${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath.git}"
 
 ########################################################################
 # Unicoq + Metacoq
 ########################################################################
-: ${unicoq_CI_BRANCH:=master}
-: ${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq.git}
+: "${unicoq_CI_BRANCH:=master}"
+: "${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq.git}"
 
-: ${metacoq_CI_BRANCH:=master}
-: ${metacoq_CI_GITURL:=https://github.com/MetaCoq/MetaCoq.git}
+: "${metacoq_CI_BRANCH:=master}"
+: "${metacoq_CI_GITURL:=https://github.com/MetaCoq/MetaCoq.git}"
 
 ########################################################################
 # Mathclasses + Corn
 ########################################################################
-: ${math_classes_CI_BRANCH:=master}
-: ${math_classes_CI_GITURL:=https://github.com/math-classes/math-classes.git}
+: "${math_classes_CI_BRANCH:=master}"
+: "${math_classes_CI_GITURL:=https://github.com/math-classes/math-classes.git}"
 
-: ${Corn_CI_BRANCH:=master}
-: ${Corn_CI_GITURL:=https://github.com/c-corn/corn.git}
+: "${Corn_CI_BRANCH:=master}"
+: "${Corn_CI_GITURL:=https://github.com/c-corn/corn.git}"
 
 ########################################################################
 # Iris
 ########################################################################
-: ${stdpp_CI_BRANCH:=master}
-: ${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git}
+: "${stdpp_CI_BRANCH:=master}"
+: "${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git}"
 
-: ${Iris_CI_BRANCH:=master}
-: ${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq.git}
+: "${Iris_CI_BRANCH:=master}"
+: "${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq.git}"
 
-: ${lambdaRust_CI_BRANCH:=master}
-: ${lambdaRust_CI_GITURL:=https://gitlab.mpi-sws.org/FP/LambdaRust-coq.git}
+: "${lambdaRust_CI_BRANCH:=master}"
+: "${lambdaRust_CI_GITURL:=https://gitlab.mpi-sws.org/FP/LambdaRust-coq.git}"
 
 ########################################################################
 # HoTT
 ########################################################################
-: ${HoTT_CI_BRANCH:=master}
-: ${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT.git}
+: "${HoTT_CI_BRANCH:=master}"
+: "${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT.git}"
 
 ########################################################################
 # Ltac2
 ########################################################################
-: ${ltac2_CI_BRANCH:=master}
-: ${ltac2_CI_GITURL:=https://github.com/ppedrot/ltac2.git}
+: "${ltac2_CI_BRANCH:=master}"
+: "${ltac2_CI_GITURL:=https://github.com/ppedrot/ltac2.git}"
 
 ########################################################################
 # GeoCoq
 ########################################################################
-: ${GeoCoq_CI_BRANCH:=master}
-: ${GeoCoq_CI_GITURL:=https://github.com/GeoCoq/GeoCoq.git}
+: "${GeoCoq_CI_BRANCH:=master}"
+: "${GeoCoq_CI_GITURL:=https://github.com/GeoCoq/GeoCoq.git}"
 
 ########################################################################
 # Flocq
 ########################################################################
-: ${Flocq_CI_BRANCH:=master}
-: ${Flocq_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git}
+: "${Flocq_CI_BRANCH:=master}"
+: "${Flocq_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git}"
 
 ########################################################################
 # Coquelicot
 ########################################################################
-: ${Coquelicot_CI_BRANCH:=master}
-: ${Coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git}
+: "${Coquelicot_CI_BRANCH:=master}"
+: "${Coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git}"
 
 ########################################################################
 # CompCert
 ########################################################################
-: ${CompCert_CI_BRANCH:=master}
-: ${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert.git}
+: "${CompCert_CI_BRANCH:=master}"
+: "${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert.git}"
 
 ########################################################################
 # VST
 ########################################################################
-: ${VST_CI_BRANCH:=master}
-: ${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST.git}
+: "${VST_CI_BRANCH:=master}"
+: "${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST.git}"
 
 ########################################################################
 # fiat_parsers
 ########################################################################
-: ${fiat_parsers_CI_BRANCH:=master}
-: ${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat.git}
+: "${fiat_parsers_CI_BRANCH:=master}"
+: "${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat.git}"
 
 ########################################################################
 # fiat_crypto
 ########################################################################
-: ${fiat_crypto_CI_BRANCH:=master}
-: ${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto.git}
+: "${fiat_crypto_CI_BRANCH:=master}"
+: "${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto.git}"
 
 ########################################################################
 # formal-topology
 ########################################################################
-: ${formal_topology_CI_BRANCH:=ci}
-: ${formal_topology_CI_GITURL:=https://github.com/bmsherman/topology.git}
+: "${formal_topology_CI_BRANCH:=ci}"
+: "${formal_topology_CI_GITURL:=https://github.com/bmsherman/topology.git}"
 
 ########################################################################
 # coq-dpdgraph
 ########################################################################
-: ${coq_dpdgraph_CI_BRANCH:=coq-trunk}
-: ${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph.git}
+: "${coq_dpdgraph_CI_BRANCH:=coq-trunk}"
+: "${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph.git}"
 
 ########################################################################
 # CoLoR
 ########################################################################
-: ${CoLoR_CI_BRANCH:=master}
-: ${CoLoR_CI_GITURL:=https://github.com/fblanqui/color.git}
+: "${CoLoR_CI_BRANCH:=master}"
+: "${CoLoR_CI_GITURL:=https://github.com/fblanqui/color.git}"
 
 ########################################################################
 # SF
 ########################################################################
-: ${sf_lf_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/lf-current/lf.tgz}
-: ${sf_plf_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/plf-current/plf.tgz}
-: ${sf_vfa_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/vfa-current/vfa.tgz}
+: "${sf_lf_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/lf-current/lf.tgz}"
+: "${sf_plf_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/plf-current/plf.tgz}"
+: "${sf_vfa_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/vfa-current/vfa.tgz}"
 
 ########################################################################
 # TLC
 ########################################################################
-: ${tlc_CI_BRANCH:=master}
-: ${tlc_CI_GITURL:=https://gforge.inria.fr/git/tlc/tlc.git}
+: "${tlc_CI_BRANCH:=master}"
+: "${tlc_CI_GITURL:=https://gforge.inria.fr/git/tlc/tlc.git}"
 
 ########################################################################
 # Bignums
 ########################################################################
-: ${bignums_CI_BRANCH:=master}
-: ${bignums_CI_GITURL:=https://github.com/coq/bignums.git}
+: "${bignums_CI_BRANCH:=master}"
+: "${bignums_CI_GITURL:=https://github.com/coq/bignums.git}"
 
 ########################################################################
 # Equations
 ########################################################################
-: ${Equations_CI_BRANCH:=8.8+alpha}
-: ${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations.git}
+: "${Equations_CI_BRANCH:=8.8+alpha}"
+: "${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations.git}"
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 58c90ff11..1838db5d0 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -4,7 +4,7 @@ set -xe
 
 if [ -n "${GITLAB_CI}" ];
 then
-    export COQBIN=`pwd`/_install_ci/bin
+    export COQBIN="$PWD/_install_ci/bin"
     export CI_BRANCH="$CI_COMMIT_REF_NAME"
 else
     if [ -n "${TRAVIS}" ];
@@ -16,7 +16,7 @@ else
         export CI_PULL_REQUEST="$CIRCLE_PR_NUMBER"
         export CI_BRANCH="$CIRCLE_BRANCH"
     fi
-    export COQBIN=`pwd`/bin
+    export COQBIN="$PWD/bin"
 fi
 export PATH="$COQBIN:$PATH"
 
@@ -26,14 +26,16 @@ export COQBIN="$COQBIN/"
 ls "$COQBIN"
 
 # Where we clone and build external developments
-CI_BUILD_DIR=`pwd`/_build_ci
+CI_BUILD_DIR="$PWD/_build_ci"
 
-for overlay in ${ci_dir}/user-overlays/*.sh; do
-  source ${overlay}
+# shellcheck source=ci-basic-overlay.sh
+source "${ci_dir}/ci-basic-overlay.sh"
+for overlay in "${ci_dir}"/user-overlays/*.sh; do
+    # shellcheck source=/dev/null
+    source "${overlay}"
 done
-source ${ci_dir}/ci-basic-overlay.sh
 
-mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp
+mathcomp_CI_DIR="${CI_BUILD_DIR}/math-comp"
 
 # git_checkout branch url dest will create a git repository
 # in <dest> (if it does not exist already) and checkout the
@@ -46,15 +48,16 @@ git_checkout()
 
   # Allow an optional 4th argument for the commit
   local _COMMIT=${4:-FETCH_HEAD}
-  local _DEPTH=$(if [ -z "${4}" ]; then echo "--depth 1"; fi)
-
-  mkdir -p ${_DEST}
-  ( cd ${_DEST}                                                && \
-    if [ ! -d .git ] ; then git clone ${_DEPTH} ${_URL} . ; fi && \
-    echo "Checking out ${_DEST}"                               && \
-    git fetch ${_URL} ${_BRANCH}                               && \
-    git checkout ${_COMMIT}                                    && \
-    echo "${_DEST}: `git log -1 --format='%s | %H | %cd | %aN'`" )
+  local _DEPTH=()
+  if [ -z "${4}" ]; then _DEPTH=(--depth 1); fi
+
+  mkdir -p "${_DEST}"
+  ( cd "${_DEST}"                                                     && \
+    if [ ! -d .git ] ; then git clone "${_DEPTH[@]}" "${_URL}" . ; fi && \
+    echo "Checking out ${_DEST}"                                      && \
+    git fetch "${_URL}" "${_BRANCH}"                                  && \
+    git checkout "${_COMMIT}"                                         && \
+    echo "${_DEST}: $(git log -1 --format='%s | %H | %cd | %aN')" )
 }
 
 checkout_mathcomp()
@@ -79,8 +82,8 @@ install_ssreflect()
 {
   echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r'
 
-  checkout_mathcomp ${mathcomp_CI_DIR}
-  ( cd ${mathcomp_CI_DIR}/mathcomp   && \
+  checkout_mathcomp "${mathcomp_CI_DIR}"
+  ( cd "${mathcomp_CI_DIR}/mathcomp" && \
     sed -i.bak '/ssrtest/d'     Make && \
     sed -i.bak '/odd_order/d'   Make && \
     sed -i.bak '/all\/all.v/d'  Make && \
diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh
index 87a829746..e3ec51aeb 100755
--- a/dev/lint-repository.sh
+++ b/dev/lint-repository.sh
@@ -9,7 +9,7 @@
 
 CODE=0
 
-if [ "(" "-n" "${TRAVIS_PULL_REQUEST}" ")" "-a" "(" "${TRAVIS_PULL_REQUEST}" "!=" "false" ")" ];
+if [ -n "${TRAVIS_PULL_REQUEST}" ] && [ "${TRAVIS_PULL_REQUEST}" != false ];
 then
     # skip PRs from before the linter existed
     if [ -z "$(git ls-tree --name-only "${TRAVIS_PULL_REQUEST_SHA}" dev/lint-commits.sh)" ];
@@ -22,14 +22,13 @@ then
     # can still check that they don't worsen.
     CUR_HEAD=${TRAVIS_COMMIT_RANGE%%...*}
     PR_HEAD=${TRAVIS_COMMIT_RANGE##*...}
-    MERGE_BASE=$(git merge-base $CUR_HEAD $PR_HEAD)
-    dev/lint-commits.sh $MERGE_BASE $PR_HEAD || CODE=1
+    MERGE_BASE=$(git merge-base "$CUR_HEAD" "$PR_HEAD")
+    dev/lint-commits.sh "$MERGE_BASE" "$PR_HEAD" || CODE=1
 fi
 
 # Check that the files with 'whitespace' gitattribute end in a newline.
 # xargs exit status is 123 if any file failed the test
-find . "(" -path ./.git -prune ")" -type f \
--o "(" -exec dev/tools/should-check-whitespace.sh '{}' ';' ")" \
--print0 | xargs -0 -L 1 dev/tools/check-eof-newline.sh || CODE=1
+find . "(" -path ./.git -prune ")" -o -type f -print0 |
+    xargs -0 dev/tools/check-eof-newline.sh || CODE=1
 
 exit $CODE
diff --git a/dev/tools/check-eof-newline.sh b/dev/tools/check-eof-newline.sh
index 1c578c05c..9e4c8661d 100755
--- a/dev/tools/check-eof-newline.sh
+++ b/dev/tools/check-eof-newline.sh
@@ -1,9 +1,14 @@
 #!/usr/bin/env bash
 
-if [ -z "$(tail -c 1 "$1")" ]
-then
-    exit 0
-else
-    echo "No newline at end of file $1!"
-    exit 1
-fi
+CODE=0
+for f in "$@"; do
+    if git ls-files --error-unmatch "$f" >/dev/null 2>&1 && \
+           git check-attr whitespace -- "$f" | grep -q -v -e 'unset$' -e 'unspecified$' && \
+           [ -n "$(tail -c 1 "$f")" ]
+    then
+        echo "No newline at end of file $f!"
+        CODE=1
+    fi
+done
+
+exit "$CODE"
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index 0c4a79bfd..9f24960ff 100755
--- a/dev/tools/merge-pr.sh
+++ b/dev/tools/merge-pr.sh
@@ -9,18 +9,18 @@ set -e
 
 PR=$1
 
-CURRENT_LOCAL_BRANCH=`git rev-parse --abbrev-ref HEAD`
-REMOTE=`git config --get branch.$CURRENT_LOCAL_BRANCH.remote`
-git fetch $REMOTE refs/pull/$PR/head
+CURRENT_LOCAL_BRANCH=$(git rev-parse --abbrev-ref HEAD)
+REMOTE=$(git config --get "branch.$CURRENT_LOCAL_BRANCH.remote")
+git fetch "$REMOTE" "refs/pull/$PR/head"
 
 API=https://api.github.com/repos/coq/coq
 
-BASE_BRANCH=`curl -s $API/pulls/$PR | jq -r '.base.label'`
+BASE_BRANCH=$(curl -s "$API/pulls/$PR" | jq -r '.base.label')
 
-COMMIT=`git rev-parse FETCH_HEAD`
-STATUS=`curl -s $API/commits/$COMMIT/status | jq -r '.state'`
+COMMIT=$(git rev-parse FETCH_HEAD)
+STATUS=$(curl -s "$API/commits/$COMMIT/status" | jq -r '.state')
 
-if [ $BASE_BRANCH != "coq:$CURRENT_LOCAL_BRANCH" ]; then
+if [ "$BASE_BRANCH" != "coq:$CURRENT_LOCAL_BRANCH" ]; then
   echo "Wrong base branch"
   read -p "Bypass? [y/N] " -n 1 -r
   echo
@@ -30,7 +30,7 @@ if [ $BASE_BRANCH != "coq:$CURRENT_LOCAL_BRANCH" ]; then
   fi
 fi;
 
-if [ $STATUS != "success" ]; then
+if [ "$STATUS" != "success" ]; then
   echo "CI status is \"$STATUS\""
   read -p "Bypass? [y/N] " -n 1 -r
   echo
@@ -40,10 +40,10 @@ if [ $STATUS != "success" ]; then
   fi
 fi;
 
-git merge -S --no-ff FETCH_HEAD -m "Merge PR #$PR: `curl -s $API/pulls/$PR | jq -r '.title'`" -e
+git merge -S --no-ff FETCH_HEAD -m "Merge PR #$PR: $(curl -s "$API/pulls/$PR" | jq -r '.title')" -e
 
 # TODO: improve this check
-if [[ `git diff $REMOTE/$CURRENT_LOCAL_BRANCH dev/ci` ]]; then
+if ! git diff --quiet "$REMOTE/$CURRENT_LOCAL_BRANCH" -- dev/ci; then
   echo "******************************************"
   echo "** WARNING: does this PR have overlays? **"
   echo "******************************************"
diff --git a/dev/tools/should-check-whitespace.sh b/dev/tools/should-check-whitespace.sh
deleted file mode 100755
index d85d65107..000000000
--- a/dev/tools/should-check-whitespace.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-#!/usr/bin/env bash
-
-# determine if a file has whitespace checking enabled in .gitattributes
-
-git ls-files --error-unmatch "$1" >/dev/null 2>&1 &&
-git check-attr whitespace -- "$1" | grep -q -v -e 'unset$' -e 'unspecified$'