From f8edf452dec50d2d310737c266a1db112386ecda Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 15 Jan 2024 18:53:04 +0100 Subject: [PATCH] chore: CI: add actionlint action, fix actions (#3156) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 (https://github.com/rhysd/actionlint/issues/389) --- .github/workflows/actionlint.yml | 22 +++++++++++++++++++++ .github/workflows/ci.yml | 34 +++++++++++++++++--------------- .github/workflows/pr-release.yml | 32 +++++++++++++++--------------- 3 files changed, 56 insertions(+), 32 deletions(-) create mode 100644 .github/workflows/actionlint.yml diff --git a/.github/workflows/actionlint.yml b/.github/workflows/actionlint.yml new file mode 100644 index 000000000000..1b0fe151005c --- /dev/null +++ b/.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 diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index d8e1349bcd4d..3b1c71f21d21 100644 --- a/.github/workflows/ci.yml +++ b/.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,8 +201,8 @@ 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 @@ -210,7 +210,7 @@ jobs: 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,7 +407,7 @@ 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/")" @@ -413,7 +415,7 @@ jobs: 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: diff --git a/.github/workflows/pr-release.yml b/.github/workflows/pr-release.yml index 4c33c254be54..09a9341d2ce0 100644 --- a/.github/workflows/pr-release.yml +++ b/.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,14 +126,14 @@ 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 @@ -141,7 +141,7 @@ jobs: 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,7 +240,7 @@ jobs: git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com" 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 @@ -248,9 +248,9 @@ jobs: 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