feat: report CI results to Batteries for batteries-pr-testing-NNNN br…

…anches (#17144) This is the other end of leanprover-community/batteries#958. Again, we'll need to make sure the token used here can post comments at Batteries.
leanprover-community · Sep 27, 2024 · cc68ae7 · cc68ae7
1 parent 20ec679
commit cc68ae7
Show file tree

Hide file tree

Showing 5 changed files with 47 additions and 24 deletions.
diff --git a/.github/build.in.yml b/.github/build.in.yml
@@ -278,7 +278,7 @@ jobs:
       # Output is posted to the zulip topic
       # https://leanprover.zulipchat.com/#narrow/stream/345428-mathlib-reviewers/topic/lean4checker
 
-      - name: Post comments for lean-pr-testing branch
+      - name: Post comments for lean-pr-testing-NNNN and batteries-pr-testing-NNNN branches
         if: always()
         env:
           TOKEN: ${{ secrets.LEAN_PR_TESTING }}
@@ -291,7 +291,8 @@ jobs:
           LINT_OUTCOME: ${{ steps.lint.outcome }}
           TEST_OUTCOME: ${{ steps.test.outcome }}
         run: |
-          scripts/lean-pr-testing-comments.sh
+          scripts/lean-pr-testing-comments.sh lean
+          scripts/lean-pr-testing-comments.sh batteries
 
   final:
     name: Post-CI jobJOB_NAME

diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
@@ -288,7 +288,7 @@ jobs:
       # Output is posted to the zulip topic
       # https://leanprover.zulipchat.com/#narrow/stream/345428-mathlib-reviewers/topic/lean4checker
 
-      - name: Post comments for lean-pr-testing branch
+      - name: Post comments for lean-pr-testing-NNNN and batteries-pr-testing-NNNN branches
         if: always()
         env:
           TOKEN: ${{ secrets.LEAN_PR_TESTING }}
@@ -301,7 +301,8 @@ jobs:
           LINT_OUTCOME: ${{ steps.lint.outcome }}
           TEST_OUTCOME: ${{ steps.test.outcome }}
         run: |
-          scripts/lean-pr-testing-comments.sh
+          scripts/lean-pr-testing-comments.sh lean
+          scripts/lean-pr-testing-comments.sh batteries
 
   final:
     name: Post-CI job

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -295,7 +295,7 @@ jobs:
       # Output is posted to the zulip topic
       # https://leanprover.zulipchat.com/#narrow/stream/345428-mathlib-reviewers/topic/lean4checker
 
-      - name: Post comments for lean-pr-testing branch
+      - name: Post comments for lean-pr-testing-NNNN and batteries-pr-testing-NNNN branches
         if: always()
         env:
           TOKEN: ${{ secrets.LEAN_PR_TESTING }}
@@ -308,7 +308,8 @@ jobs:
           LINT_OUTCOME: ${{ steps.lint.outcome }}
           TEST_OUTCOME: ${{ steps.test.outcome }}
         run: |
-          scripts/lean-pr-testing-comments.sh
+          scripts/lean-pr-testing-comments.sh lean
+          scripts/lean-pr-testing-comments.sh batteries
 
   final:
     name: Post-CI job

diff --git a/.github/workflows/build_fork.yml b/.github/workflows/build_fork.yml
@@ -292,7 +292,7 @@ jobs:
       # Output is posted to the zulip topic
       # https://leanprover.zulipchat.com/#narrow/stream/345428-mathlib-reviewers/topic/lean4checker
 
-      - name: Post comments for lean-pr-testing branch
+      - name: Post comments for lean-pr-testing-NNNN and batteries-pr-testing-NNNN branches
         if: always()
         env:
           TOKEN: ${{ secrets.LEAN_PR_TESTING }}
@@ -305,7 +305,8 @@ jobs:
           LINT_OUTCOME: ${{ steps.lint.outcome }}
           TEST_OUTCOME: ${{ steps.test.outcome }}
         run: |
-          scripts/lean-pr-testing-comments.sh
+          scripts/lean-pr-testing-comments.sh lean
+          scripts/lean-pr-testing-comments.sh batteries
 
   final:
     name: Post-CI job (fork)

diff --git a/scripts/lean-pr-testing-comments.sh b/scripts/lean-pr-testing-comments.sh
@@ -1,8 +1,13 @@
-## Create comments and labels on a Lean 4 PR after CI has finished on a `lean-pr-testing-NNNN` branch.
+## Create comments and labels on a Lean 4 or Batteries PR after CI has finished on a `*-pr-testing-NNNN` branch.
 ##
 ## See https://leanprover-community.github.io/contribute/tags_and_branches.html
 set -e
 
+# Ensure first argument is either 'lean' or 'batteries'.
+if [ -z "$1" ]; then
+  echo "The first argument must be either 'lean' or 'batteries'"
+  exit 1
+fi
 
 # TODO: The whole script ought to be rewritten in javascript, to avoid having to use curl for API calls.
 #
@@ -19,36 +24,51 @@ set -e
 #   LINT_OUTCOME: ${{ steps.lint.outcome }}
 #   TEST_OUTCOME: ${{ steps.test.outcome }}
 
+# Adjust the branch pattern and URLs based on the repository.
+if [ "$1" == "lean" ]; then
+  branch_prefix="lean-pr-testing"
+  repo_url="https://api.github.com/repos/leanprover/lean4"
+  base_branch="nightly-testing" # This really should be the relevant `nightly-testing-YYYY-MM-DD` tag.
+elif [ "$1" == "batteries" ]; then
+  branch_prefix="batteries-pr-testing"
+  repo_url="https://api.github.com/repos/leanprover-community/batteries"
+  base_branch="master"
+else
+  echo "Unknown repository: $1. Must be either 'lean' or 'batteries'."
+  exit 1
+fi
+
 # Extract branch name and check if it matches the pattern.
 branch_name=$(echo "$GITHUB_CONTEXT" | jq -r .ref | cut -d'/' -f3)
-if [[ "$branch_name" =~ ^lean-pr-testing-([0-9]+)$ ]]; then
+if [[ "$branch_name" =~ ^$branch_prefix-([0-9]+)$ ]]; then
   pr_number="${BASH_REMATCH[1]}"
   current_time=$(date "+%Y-%m-%d %H:%M:%S")
 
-  echo "This is a 'lean-pr-testing-$pr_number' branch, so we need to adjust labels and write a comment."
+  echo "This is a '$branch_prefix-$pr_number' branch, so we need to adjust labels and write a comment."
 
+  # Perform actions based on outcomes (same logic as before)
   if [ "$TEST_OUTCOME" == "success" ]; then
     echo "Removing label awaiting-mathlib"
     curl -L -s \
       -X DELETE \
       -H "Accept: application/vnd.github+json" \
       -H "Authorization: Bearer $TOKEN" \
       -H "X-GitHub-Api-Version: 2022-11-28" \
-      https://api.github.com/repos/leanprover/lean4/issues/$pr_number/labels/awaiting-mathlib
+      $repo_url/issues/$pr_number/labels/awaiting-mathlib
     echo "Removing label breaks-mathlib"
     curl -L -s \
       -X DELETE \
       -H "Accept: application/vnd.github+json" \
       -H "Authorization: Bearer $TOKEN" \
       -H "X-GitHub-Api-Version: 2022-11-28" \
-      https://api.github.com/repos/leanprover/lean4/issues/$pr_number/labels/breaks-mathlib
+      $repo_url/issues/$pr_number/labels/breaks-mathlib
     echo "Adding label builds-mathlib"
     curl -L -s \
       -X POST \
       -H "Accept: application/vnd.github+json" \
       -H "Authorization: Bearer $TOKEN" \
       -H "X-GitHub-Api-Version: 2022-11-28" \
-      https://api.github.com/repos/leanprover/lean4/issues/$pr_number/labels \
+      $repo_url/issues/$pr_number/labels \
       -d '{"labels":["builds-mathlib"]}'
   elif [ "$LINT_OUTCOME" == "failure" ] || [ "$TEST_OUTCOME" == "failure" ] || [ "$COUNTEREXAMPLES_OUTCOME" == "failure" ] || [ "$ARCHIVE_OUTCOME" == "failure" ] || [ "$NOISY_OUTCOME" == "failure" ] || [ "$BUILD_OUTCOME" == "failure" ]; then
     echo "Removing label builds-mathlib"
@@ -57,32 +77,32 @@ if [[ "$branch_name" =~ ^lean-pr-testing-([0-9]+)$ ]]; then
       -H "Accept: application/vnd.github+json" \
       -H "Authorization: Bearer $TOKEN" \
       -H "X-GitHub-Api-Version: 2022-11-28" \
-      https://api.github.com/repos/leanprover/lean4/issues/$pr_number/labels/builds-mathlib
+      $repo_url/issues/$pr_number/labels/builds-mathlib
     echo "Adding label breaks-mathlib"
     curl -L -s \
       -X POST \
       -H "Accept: application/vnd.github+json" \
       -H "Authorization: Bearer $TOKEN" \
       -H "X-GitHub-Api-Version: 2022-11-28" \
-      https://api.github.com/repos/leanprover/lean4/issues/$pr_number/labels \
+      $repo_url/issues/$pr_number/labels \
       -d '{"labels":["breaks-mathlib"]}'
   fi
 
   # Use GitHub API to check if a comment already exists
   existing_comment=$(curl -L -s -H "Authorization: token $TOKEN" \
                           -H "Accept: application/vnd.github.v3+json" \
-                          "https://api.github.com/repos/leanprover/lean4/issues/$pr_number/comments" \
+                          "$repo_url/issues/$pr_number/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)
 
-  branch="[lean-pr-testing-$pr_number](https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-$pr_number)"
+  branch="[$branch_prefix-$pr_number](https://github.com/leanprover-community/mathlib4/compare/$base_branch...$branch_prefix-$pr_number)"
   # Depending on the success/failure, set the appropriate message
   if [ "$LINT_OUTCOME" == "cancelled" ] || [ "$TEST_OUTCOME" == "cancelled" ] || [ "$COUNTEREXAMPLES_OUTCOME" == "cancelled" ] || [ "$ARCHIVE_OUTCOME" == "cancelled" ] || [ "$NOISY_OUTCOME" == "cancelled" ] || [ "$BUILD_OUTCOME" == "cancelled" ]; then
     message="- 🟡 Mathlib branch $branch build against this PR was cancelled. ($current_time) [View Log]($WORKFLOW_URL)"
   elif [ "$TEST_OUTCOME" == "success" ]; then
     message="- ✅ Mathlib branch $branch has successfully built against this PR. ($current_time) [View Log]($WORKFLOW_URL)"
-  elif [ "$BUILD_OUTCOME" == "failure" ] ; then
+  elif [ "$BUILD_OUTCOME" == "failure" ]; then
     message="- 💥 Mathlib branch $branch build failed against this PR. ($current_time) [View Log]($WORKFLOW_URL)"
   elif [ "$LINT_OUTCOME" == "failure" ]; then
     message="- ❌ Mathlib branch $branch built against this PR, but linting failed. ($current_time) [View Log]($WORKFLOW_URL)"
@@ -103,23 +123,22 @@ if [[ "$branch_name" =~ ^lean-pr-testing-([0-9]+)$ ]]; then
   # Append new result to the existing comment or post a new comment
   if [ -z "$existing_comment_id" ]; then
     # Post new comment with a bullet point
-    # Keep message in sync with https://github.com/leanprover/lean4/blob/master/.github/workflows/pr-release.yml
     intro="Mathlib CI status ([docs](https://leanprover-community.github.io/contribute/tags_and_branches.html)):"
-    echo "Posting as new comment at leanprover/lean4/issues/$pr_number/comments"
+    echo "Posting as new comment at $repo_url/issues/$pr_number/comments"
     curl -L -s \
       -X POST \
       -H "Authorization: token $TOKEN" \
       -H "Accept: application/vnd.github.v3+json" \
       -d "$(jq --null-input --arg intro "$intro" --arg val "$message" '{"body": ($intro + "\n" + $val)}')" \
-      "https://api.github.com/repos/leanprover/lean4/issues/$pr_number/comments"
+      "$repo_url/issues/$pr_number/comments"
   else
     # Append new result to the existing comment
-    echo "Appending to existing comment at leanprover/lean4/issues/$pr_number/comments"
+    echo "Appending to existing comment at $repo_url/issues/$pr_number/comments"
     curl -L -s \
       -X PATCH \
       -H "Authorization: token $TOKEN" \
       -H "Accept: application/vnd.github.v3+json" \
       -d "$(jq --null-input --arg existing "$existing_comment_body" --arg message "$message" '{"body":($existing + "\n" + $message)}')" \
-      "https://api.github.com/repos/leanprover/lean4/issues/comments/$existing_comment_id"
+      "$repo_url/issues/comments/$existing_comment_id"
   fi
 fi