chore: CI looks for nightly-testing-YYYY-MM-DD at Mathlib as either a…

… branch or tag (#3199)

As discussed during the FRO meeting 2024-01-18, we are changing the
`nightly-testing-YYYY-MM-DD` branches at Std and Mathlib from branches
to tags, in:

* leanprover-community/batteries#545
* leanprover-community/mathlib4#9842

This PR updates the script that creates the `lean-pr-testing-NNNN`
branches at Mathlib so it is agnostic about whether
`nightly-testing-YYYY-MM-DD` will be a branch or a tag.

---------

Co-authored-by: Joachim Breitner <[email protected]>

.github/workflows/pr-release.yml

@@ -41,7 +41,7 @@ jobs:
           name: build-.*
           name_is_regexp: true
 
-      - name: Push branch and tag
+      - name: Push tag
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         run: |
           git init --bare lean4.git
@@ -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_TAGS="$(git ls-remote 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."
+            if [[ -n "$REMOTE_TAGS" ]]; then
+              echo "... and Mathlib has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
               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."
+              echo "... but Mathlib does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
+              MESSAGE="- ❗ Mathlib CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag 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
@@ -232,21 +232,21 @@ jobs:
           ref: nightly-testing
           fetch-depth: 0 # This ensures we check out all tags and branches.
 
-      - name: Check if branch exists
+      - name: Check if tag exists
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
-        id: check_branch
+        id: check_tag
         run: |
           git config user.name "leanprover-community-mathlib4-bot"
           git config user.email "[email protected]"
 
-          if git branch -r | grep -q "nightly-testing-${MOST_RECENT_NIGHTLY}"; then
+          if git ls-remote --heads --tags --exit-code origin "nightly-testing-${MOST_RECENT_NIGHTLY}" >/dev/null; then
             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"
+          echo "Using base tag: $BASE"
 
           git checkout "$BASE"
 
@@ -261,7 +261,8 @@ jobs:
           else
             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.
+            # The Mathlib `nightly-testing` or `nightly-testing-YYYY-MM-DD` tag may have moved since this branch was created, so merge their changes.
+            # (This should no longer be possible once `nightly-testing-YYYY-MM-DD` is a tag, but it is still safe to merge.)
             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