chore: CI: add actionlint action, fix actions (#3156)

I keep messing things up, so time for some guard rails, so check them
using
[actionlint](https://github.com/raven-actions/actionlint).

This also runs [shellcheck](https://www.shellcheck.net/) on the files.
Shellcheck
is a bit picky about putting double quotes around variables, and will
flag many
cases where we know it’s safe, but why not simply always write the safer
variant.

Unfortunately, actionlint does not (yet) check `actions/github-script`
scripts, which is
unfortunate. Maybe they will in the future
(rhysd/actionlint#389)

.github/workflows/actionlint.yml

@@ -0,0 +1,22 @@
+name: Actionlint
+on:
+  push:
+    branches:
+      - 'master'
+    paths:
+      - '.github/**'
+  pull_request:
+    paths:
+      - '.github/**'
+  merge_group:
+
+jobs:
+  actionlint:
+    runs-on: ubuntu-latest
+    steps:
+    - name: Checkout
+      uses: actions/checkout@v3
+    - name: actionlint
+      uses: raven-actions/actionlint@v1
+      with:
+        pyflakes: false # we do not use python scripts

.github/workflows/ci.yml

@@ -46,7 +46,7 @@ jobs:
             github.event_name == 'pull_request' && !contains( github.event.pull_request.labels.*.name, 'full-ci')
            }}
         run: |
-          echo "quick=${{env.quick}}" >> $GITHUB_OUTPUT
+          echo "quick=${{env.quick}}" >> "$GITHUB_OUTPUT"
 
       - name: Configure build matrix
         id: set-matrix
@@ -201,16 +201,16 @@ jobs:
             git fetch nightly --tags
             LEAN_VERSION_STRING="nightly-$(date -u +%F)"
             # do nothing if commit already has a different tag
-            if [[ $(git name-rev --name-only --tags --no-undefined HEAD 2> /dev/null || echo $LEAN_VERSION_STRING) == $LEAN_VERSION_STRING ]]; then
-              echo "nightly=$LEAN_VERSION_STRING" >> $GITHUB_OUTPUT
+            if [[ "$(git name-rev --name-only --tags --no-undefined HEAD 2> /dev/null || echo "$LEAN_VERSION_STRING")" == "$LEAN_VERSION_STRING" ]]; then
+              echo "nightly=$LEAN_VERSION_STRING" >> "$GITHUB_OUTPUT"
             fi
           fi
 
       - name: Check for official release
         if: startsWith(github.ref, 'refs/tags/') && github.repository == 'leanprover/lean4'
         id: set-release
         run: |
-          TAG_NAME=${GITHUB_REF##*/}
+          TAG_NAME="${GITHUB_REF##*/}"
 
           # From https://github.com/fsaintjacques/semver-tool/blob/master/src/semver
 
@@ -227,11 +227,13 @@ jobs:
 
           if [[ ${TAG_NAME} =~ ${SEMVER_REGEX} ]]; then
             echo "Tag ${TAG_NAME} matches SemVer regex, with groups ${BASH_REMATCH[1]} ${BASH_REMATCH[2]} ${BASH_REMATCH[3]} ${BASH_REMATCH[4]}"
-            echo "LEAN_VERSION_MAJOR=${BASH_REMATCH[1]}" >> $GITHUB_OUTPUT
-            echo "LEAN_VERSION_MINOR=${BASH_REMATCH[2]}" >> $GITHUB_OUTPUT
-            echo "LEAN_VERSION_PATCH=${BASH_REMATCH[3]}" >> $GITHUB_OUTPUT
-            echo "LEAN_SPECIAL_VERSION_DESC=${BASH_REMATCH[4]##-}" >> $GITHUB_OUTPUT
-            echo "RELEASE_TAG=$TAG_NAME" >> $GITHUB_OUTPUT
+            {
+              echo "LEAN_VERSION_MAJOR=${BASH_REMATCH[1]}"
+              echo "LEAN_VERSION_MINOR=${BASH_REMATCH[2]}"
+              echo "LEAN_VERSION_PATCH=${BASH_REMATCH[3]}"
+              echo "LEAN_SPECIAL_VERSION_DESC=${BASH_REMATCH[4]##-}"
+              echo "RELEASE_TAG=$TAG_NAME"
+            } >> "$GITHUB_OUTPUT"
           else
             echo "Tag ${TAG_NAME} did not match SemVer regex."
           fi
@@ -405,15 +407,15 @@ jobs:
       - name: CCache stats
         run: ccache -s
       - name: Show stacktrace for coredumps
-        if: ${{ failure() }} && matrix.os == 'ubuntu-latest'
+        if: ${{ failure() && matrix.os == 'ubuntu-latest' }}
         run: |
           for c in coredumps/*; do
             progbin="$(file $c | sed "s/.*execfn: '\([^']*\)'.*/\1/")"
             echo bt | $GDB/bin/gdb -q $progbin $c || true
           done
       - name: Upload coredumps
         uses: actions/upload-artifact@v3
-        if: ${{ failure() }} && matrix.os == 'ubuntu-latest'
+        if: ${{ failure() && matrix.os == 'ubuntu-latest' }}
         with:
           name: coredumps-${{ matrix.name }}
           path: |
@@ -480,16 +482,16 @@ jobs:
         run: |
           git remote add nightly https://foo:'${{ secrets.PUSH_NIGHTLY_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-nightly.git
           git fetch nightly --tags
-          git tag ${{ needs.configure.outputs.nightly }}
-          git push nightly ${{ needs.configure.outputs.nightly }}
+          git tag "${{ needs.configure.outputs.nightly }}"
+          git push nightly "${{ needs.configure.outputs.nightly }}"
           git push -f origin refs/tags/${{ needs.configure.outputs.nightly }}:refs/heads/nightly
-          last_tag=$(git log HEAD^ --simplify-by-decoration --pretty="format:%d" | grep -o "nightly-[-0-9]*" | head -n 1)
+          last_tag="$(git log HEAD^ --simplify-by-decoration --pretty="format:%d" | grep -o "nightly-[-0-9]*" | head -n 1)"
           echo -e "*Changes since ${last_tag}:*\n\n" > diff.md
-          git show $last_tag:RELEASES.md > old.md
+          git show "$last_tag":RELEASES.md > old.md
           #./script/diff_changelogs.py old.md doc/changes.md >> diff.md
           diff --changed-group-format='%>' --unchanged-group-format='' old.md RELEASES.md >> diff.md || true
           echo -e "\n*Full commit log*\n" >> diff.md
-          git log --oneline $last_tag..HEAD | sed 's/^/* /' >> diff.md
+          git log --oneline "$last_tag"..HEAD | sed 's/^/* /' >> diff.md
       - name: Release Nightly
         uses: softprops/action-gh-release@v1
         with:

.github/workflows/pr-release.yml

@@ -107,7 +107,7 @@ jobs:
           git -C lean4.git remote add nightly https://github.com/leanprover/lean4-nightly.git
           git -C lean4.git fetch nightly '+refs/tags/nightly-*:refs/tags/nightly-*'
           git -C lean4.git tag --merged "${{ steps.workflow-info.outputs.sourceHeadSha }}" --list "nightly-*" \
-            | sort -rV | head -n 1 | sed "s/^nightly-*/MOST_RECENT_NIGHTLY=/" | tee -a $GITHUB_ENV
+            | sort -rV | head -n 1 | sed "s/^nightly-*/MOST_RECENT_NIGHTLY=/" | tee -a "$GITHUB_ENV"
 
       - name: 'Setup jq'
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
@@ -126,22 +126,22 @@ jobs:
           if [ "$NIGHTLY_SHA" = "$MERGE_BASE_SHA" ]; then
             echo "The merge base of this PR coincides with the nightly release"
 
-            REMOTE_BRANCHES=$(git ls-remote -h https://github.com/leanprover-community/mathlib4.git nightly-testing-$MOST_RECENT_NIGHTLY)
+            REMOTE_BRANCHES="$(git ls-remote -h https://github.com/leanprover-community/mathlib4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
 
             if [[ -n "$REMOTE_BRANCHES" ]]; then
               echo "... and Mathlib has a 'nightly-testing-$MOST_RECENT_NIGHTLY' branch."
               MESSAGE=""
             else
               echo "... but Mathlib does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' branch."
-              MESSAGE="- ❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-$MOST_RECENT_NIGHTLY' branch does not exist there yet. We will retry when you push more commits. If you rebase your branch onto `nightly-with-mathlib`, Mathlib CI should run now."
+              MESSAGE="- ❗ Mathlib CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` branch does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Mathlib CI should run now."
             fi
 
           else
             echo "The most recently nightly tag on this branch has SHA: $NIGHTLY_SHA"
             echo "but 'git merge-base origin/master HEAD' reported: $MERGE_BASE_SHA"
             git -C lean4.git log -10 origin/master
 
-            MESSAGE="- ❗ Mathlib CI will not be attempted unless your PR branches off the 'nightly-with-mathlib' branch."
+            MESSAGE="- ❗ Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch."
           fi
 
           if [[ -n "$MESSAGE" ]]; then
@@ -153,12 +153,12 @@ jobs:
             # so keep in sync
 
             # Use GitHub API to check if a comment already exists
-            existing_comment=$(curl -L -s -H "Authorization: token ${{ secrets.MATHLIB4_BOT }}" \
+            existing_comment="$(curl -L -s -H "Authorization: token ${{ secrets.MATHLIB4_BOT }}" \
                                     -H "Accept: application/vnd.github.v3+json" \
                                     "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments" \
-                                    | jq 'first(.[] | select(.body | test("^- . Mathlib") or startswith("Mathlib CI status")) | select(.user.login == "leanprover-community-mathlib4-bot"))')
-            existing_comment_id=$(echo "$existing_comment" | jq -r .id)
-            existing_comment_body=$(echo "$existing_comment" | jq -r .body)
+                                    | jq 'first(.[] | select(.body | test("^- . Mathlib") or startswith("Mathlib CI status")) | select(.user.login == "leanprover-community-mathlib4-bot"))')"
+            existing_comment_id="$(echo "$existing_comment" | jq -r .id)"
+            existing_comment_body="$(echo "$existing_comment" | jq -r .body)"
 
             if [[ "$existing_comment_body" != *"$MESSAGE"* ]]; then
               MESSAGE="$MESSAGE ($(date "+%Y-%m-%d %H:%M:%S"))"
@@ -190,13 +190,13 @@ jobs:
             else
               echo "The message already exists in the comment body."
             fi
-            echo "mathlib_ready=false" >> $GITHUB_OUTPUT
+            echo "mathlib_ready=false" >> "$GITHUB_OUTPUT"
           else
-            echo "mathlib_ready=true" >> $GITHUB_OUTPUT
+            echo "mathlib_ready=true" >> "$GITHUB_OUTPUT"
           fi
 
       - name: Report mathlib base
-        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} && steps.ready.outputs.mathlib_ready == 'true'
+        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true' }}
         uses: actions/github-script@v6
         with:
           script: |
@@ -220,7 +220,7 @@ jobs:
       - name: Cleanup workspace
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
         run: |
-          sudo rm -rf *
+          sudo rm -rf ./*
 
       # Checkout the mathlib4 repository with all branches
       - name: Checkout mathlib4 repository
@@ -240,17 +240,17 @@ jobs:
           git config user.email "[email protected]"
 
           if git branch -r | grep -q "nightly-testing-${MOST_RECENT_NIGHTLY}"; then
-            BASE=nightly-testing-${MOST_RECENT_NIGHTLY}
+            BASE="nightly-testing-${MOST_RECENT_NIGHTLY}"
           else
             echo "This shouldn't be possible: couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' branch at Mathlib. Falling back to 'nightly-testing'."
             BASE=nightly-testing
           fi
 
           echo "Using base branch: $BASE"
 
-          git checkout $BASE
+          git checkout "$BASE"
 
-          EXISTS=$(git ls-remote --heads origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} | wc -l)
+          EXISTS="$(git ls-remote --heads origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} | wc -l)"
           echo "Branch exists: $EXISTS"
           if [ "$EXISTS" = "0" ]; then
             echo "Branch does not exist, creating it."
@@ -262,7 +262,7 @@ jobs:
             echo "Branch already exists, pushing an empty commit."
             git checkout lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
             # The Mathlib `nightly-testing` or `nightly-testing-YYYY-MM-DD` branch may have moved since this branch was created, so merge their changes.
-            git merge $BASE --strategy-option ours --no-commit --allow-unrelated-histories
+            git merge "$BASE" --strategy-option ours --no-commit --allow-unrelated-histories
             git commit --allow-empty -m "Trigger CI for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
           fi