nightly_bump_and_merge.yml

name: Bump toolchain and merge pr-testing branches

# This workflow combines the former `nightly_bump_toolchain.yml` and `discover-lean-pr-testing.yml`
# into a single workflow. This ensures that when the toolchain is bumped, any relevant
# lean-pr-testing branches are merged in the same push, avoiding spurious CI failures
# on the intermediate state (bumped toolchain without the adaptations).

on:
  schedule:
    - cron: '45 9/3 * * *'
    # 10:45AM CET/1:45AM PT (and then every 3 hours thereafter),
    # This should be 2 hours and 45 minutes after lean4 starts building the nightly.
    # Mathlib's `nightly-testing` branch is bumped 15 minutes later.
  workflow_dispatch:

jobs:
  bump-and-merge:
    runs-on: ubuntu-latest
    if: github.repository_owner == 'leanprover-community'
    steps:
    - name: Generate app token
      id: app-token
      uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1
      with:
        app-id: ${{ secrets.MATHLIB_NIGHTLY_TESTING_APP_ID }}
        private-key: ${{ secrets.MATHLIB_NIGHTLY_TESTING_PRIVATE_KEY }}
    # The create-github-app-token README states that this token is masked and will not be logged accidentally.

    - name: Checkout nightly-testing branch
      uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
      with:
        ref: nightly-testing
        fetch-depth: 0  # Fetch all branches and history
        token: ${{ steps.app-token.outputs.token }}

    - name: Set up Git
      run: |
        git config --global user.name "mathlib-nightly-testing[bot]"
        git config --global user.email "mathlib-nightly-testing[bot]@users.noreply.github.com"

    - name: Configure Lean
      uses: leanprover/lean-action@f807b338d95de7813c5c50d018f1c23c9b93b4ec # 2025-04-24
      with:
        auto-config: false
        use-github-cache: false
        use-mathlib-cache: false

    # ============================================================================
    # Phase 1: Bump the toolchain (commit locally, don't push yet)
    # ============================================================================

    - name: Get old toolchain version
      id: old-toolchain
      run: |
        # Capture the current toolchain BEFORE we modify anything
        OLD=$(cut -f2 -d: lean-toolchain)
        echo "old=$OLD"
        echo "old=$OLD" >> "$GITHUB_OUTPUT"

    - name: Get latest release tag from leanprover/lean4-nightly
      id: get-latest-release
      env:
        GH_TOKEN: ${{ steps.app-token.outputs.token }}
      run: |
        RELEASE_TAG=$(gh api -X GET repos/leanprover/lean4-nightly/releases \
          -f per_page=1 --jq '.[0].tag_name')
        if [ -z "$RELEASE_TAG" ] || [ "$RELEASE_TAG" = "null" ]; then
          echo "::error::Could not determine latest lean4-nightly release"
          exit 1
        fi
        echo "RELEASE_TAG=$RELEASE_TAG"
        echo "RELEASE_TAG=$RELEASE_TAG" >> "$GITHUB_ENV"
        echo "new=$RELEASE_TAG" >> "$GITHUB_OUTPUT"

    - name: Update lean-toolchain file
      run: |
        echo "leanprover/lean4:${RELEASE_TAG}" > lean-toolchain

    - name: Commit toolchain bump (without pushing)
      id: commit-bump
      run: |
        git add lean-toolchain
        # Don't fail if there's nothing to commit (toolchain already up to date)
        if git commit -m "chore: bump to ${RELEASE_TAG}"; then
          echo "bumped=true" >> "$GITHUB_OUTPUT"
        else
          echo "bumped=false" >> "$GITHUB_OUTPUT"
          echo "Toolchain already at ${RELEASE_TAG}, no bump needed"
        fi

    # ============================================================================
    # Phase 2: Find and merge pr-testing branches
    # ============================================================================

    - name: Clone lean4-nightly and get PRs
      id: get-prs
      if: steps.commit-bump.outputs.bumped == 'true'
      run: |
        OLD="${{ steps.old-toolchain.outputs.old }}"
        NEW="${{ steps.get-latest-release.outputs.new }}"

        echo "Finding PRs between $OLD and $NEW"

        NIGHTLY_URL="https://github.com/leanprover/lean4-nightly.git"

        # Create a temporary directory for cloning
        cd "$(mktemp -d)" || exit 1

        # Clone the repository with a depth of 1
        git clone --depth 1 "$NIGHTLY_URL"

        # Navigate to the cloned repository
        cd lean4-nightly || exit 1

        # Fetch the $OLD tag
        git fetch --depth=1 origin tag "$OLD" --no-tags
        # Fetch the $NEW tag
        git fetch origin tag "$NEW" --no-tags

        # Get all commit SHAs between the $OLD and $NEW toolchains
        COMMIT_SHAS=$(git log --format="%H" "$OLD..$NEW")

        # Initialize an empty string to collect PR numbers
        PRS=""

        # For each commit, query the GitHub API to get associated PRs
        for commit_sha in $COMMIT_SHAS; do
          echo "Checking commit $commit_sha for associated PRs..."

          # Query GitHub API for PRs associated with this commit
          pr_numbers=$(curl -s -H "Accept: application/vnd.github.v3+json" \
            "https://api.github.com/repos/leanprover/lean4/commits/$commit_sha/pulls" | \
            jq -r '.[] | select(.merged_at != null) | .number | tostring' 2>/dev/null || echo "")

          # Add each PR number to our list (duplicates will be handled later)
          for pr_num in $pr_numbers; do
            if [[ "$pr_num" =~ ^[0-9]+$ ]]; then
              PRS="$PRS $pr_num"
              echo "Found PR #$pr_num associated with commit $commit_sha"
            fi
          done
        done

        # Remove duplicates and trim whitespace
        PRS=$(echo "$PRS" | tr ' ' '\n' | sort -u | tr '\n' ' ' | xargs)

        # Output the PRs
        echo "Found PRs: $PRS"
        printf "prs<<EOF\n%s\nEOF" "$PRS" >> "$GITHUB_OUTPUT"

    - name: Find matching pr-testing branches
      id: find-branches
      if: steps.commit-bump.outputs.bumped == 'true'
      run: |
        PRS="${{ steps.get-prs.outputs.prs }}"
        echo "=== PRS ========================="
        echo "$PRS"

        # CRITICAL: If no PRs were found, skip branch matching entirely.
        if [ -z "$PRS" ]; then
          echo "No PRs found between old and new nightlies. Skipping branch discovery."
          echo "branches_exist=false" >> "$GITHUB_ENV"
          printf "branches<<EOF\n\nEOF" >> "$GITHUB_OUTPUT"
          exit 0
        fi

        echo "$PRS" | tr ' ' '\n' > prs.txt
        echo "=== prs.txt ====================="
        cat prs.txt
        MATCHING_BRANCHES=$(git branch -r | grep -f prs.txt | grep "lean-pr-testing" || true)
        echo "=== MATCHING_BRANCHES ==========="
        echo "$MATCHING_BRANCHES"
        echo "================================="

        # Initialize an empty variable to store branches with relevant diffs
        RELEVANT_BRANCHES=""

        # Loop through each matching branch
        for BRANCH in $MATCHING_BRANCHES; do
            echo " === Testing $BRANCH for relevance."
            # Get the diff filenames
            DIFF_FILES=$(git diff --name-only "origin/nightly-testing...$BRANCH")

            # Check if the diff contains files other than the specified ones
            # Note: Batteries uses lakefile.toml, not lakefile.lean
            if echo "$DIFF_FILES" | grep -v -e 'lake-manifest.json' -e 'lakefile.toml' -e 'lean-toolchain'; then
                # Extract the actual branch name
                ACTUAL_BRANCH=${BRANCH#origin/}

                # Append the branch details to RELEVANT_BRANCHES
                RELEVANT_BRANCHES="$RELEVANT_BRANCHES""$ACTUAL_BRANCH"$' '
            fi
        done

        # Output the relevant branches
        echo "=== RELEVANT_BRANCHES ==========="
        echo "'$RELEVANT_BRANCHES'"
        printf "branches<<EOF\n%s\nEOF" "$RELEVANT_BRANCHES" >> "$GITHUB_OUTPUT"

        # Check if there are relevant branches
        if [ -z "${RELEVANT_BRANCHES}" ]; then
          echo "branches_exist=false" >> "$GITHUB_ENV"
        else
          echo "branches_exist=true" >> "$GITHUB_ENV"
        fi

    - name: Execute merge script for each branch
      id: execute-merges
      if: steps.commit-bump.outputs.bumped == 'true' && env.branches_exist == 'true'
      run: |
        BRANCHES="${{ steps.find-branches.outputs.branches }}"

        # Initialize arrays to track results
        SUCCESSFUL_MERGES=""
        FAILED_MERGES=""

        # Ensure the merge script is executable
        chmod +x scripts/merge-lean-testing-pr.sh

        # Process each branch
        for BRANCH in $BRANCHES; do
          # Extract PR number from branch name
          PR_NUMBER=$(echo "$BRANCH" | grep -oP '\d+$')

          # Make sure we're on nightly-testing branch before doing fetch operations
          git checkout nightly-testing

          # Fetch all tags in the repository
          git fetch --tags

          # Fetch the PR branch
          git fetch origin "$BRANCH"

          # Find the most recent nightly-testing-YYYY-MM-DD tag that is an ancestor of the branch
          git checkout origin/"$BRANCH" || {
            echo "Failed to checkout branch origin/$BRANCH, skipping"
            continue
          }

          # Find tags that are ancestors of this branch with the right format
          LATEST_TAG=$(git tag --merged HEAD | grep "nightly-testing-[0-9]\{4\}-[0-9]\{2\}-[0-9]\{2\}" | sort -r | head -n 1)
          echo "Latest tag found for $BRANCH: ${LATEST_TAG:-none}"

          # Return to nightly-testing branch
          git checkout nightly-testing

          # Default to nightly-testing if no tag is found
          if [ -z "$LATEST_TAG" ]; then
            COMPARE_BASE="nightly-testing"
          else
            COMPARE_BASE="$LATEST_TAG"
          fi

          GITHUB_DIFF="https://github.com/leanprover-community/batteries/compare/$COMPARE_BASE...lean-pr-testing-$PR_NUMBER"

          echo "Attempting to merge branch: $BRANCH (PR #$PR_NUMBER)"
          echo "Using diff URL: $GITHUB_DIFF (comparing with $COMPARE_BASE)"

          # Reset to a clean state before running merge script
          git reset --hard HEAD

          # Run the merge script and capture exit code
          # Note: The merge script does its own commit but NOT push
          if ./scripts/merge-lean-testing-pr.sh "$PR_NUMBER"; then
            echo "Successfully merged $BRANCH"
            SUCCESSFUL_MERGES="$SUCCESSFUL_MERGES$PR_NUMBER|$GITHUB_DIFF|$BRANCH "
          else
            echo "Failed to merge $BRANCH"
            FAILED_MERGES="$FAILED_MERGES$PR_NUMBER|$GITHUB_DIFF|$BRANCH "

            # Clean up - reset to a clean state
            git reset --hard HEAD
            git checkout nightly-testing
          fi
        done

        # Output the results
        echo "successful_merges=$SUCCESSFUL_MERGES" >> "$GITHUB_OUTPUT"
        echo "failed_merges=$FAILED_MERGES" >> "$GITHUB_OUTPUT"

    # ============================================================================
    # Phase 3: Push everything and notify
    # ============================================================================

    - name: Push all changes
      if: steps.commit-bump.outputs.bumped == 'true'
      run: |
        # This pushes the toolchain bump commit plus any successful merge commits
        git push origin nightly-testing

    - name: Prepare Zulip message
      id: zulip-message
      if: steps.commit-bump.outputs.bumped == 'true' && env.branches_exist == 'true'
      run: |
        SUCCESSFUL_MERGES="${{ steps.execute-merges.outputs.successful_merges }}"
        FAILED_MERGES="${{ steps.execute-merges.outputs.failed_merges }}"

        # Start building the message
        MESSAGE=""

        # Report successful merges
        if [ -n "$SUCCESSFUL_MERGES" ]; then
          MESSAGE+=$'### Successfully merged branches into Batteries\' \'nightly-testing\':\n\n'
          for MERGE_INFO in $SUCCESSFUL_MERGES; do
            IFS='|' read -r PR_NUMBER GITHUB_DIFF _ <<< "$MERGE_INFO"
            MESSAGE+=$(printf -- '- [lean-pr-testing-%s](%s) (adaptations for lean#%s)' "$PR_NUMBER" "$GITHUB_DIFF" "$PR_NUMBER")$'\n\n'
          done
          MESSAGE+=$'\n'
        else
          MESSAGE+=$'No branches were successfully merged into Batteries\' \'nightly-testing\'. \n\n'
        fi

        # Report failed merges
        if [ -n "$FAILED_MERGES" ]; then
          MESSAGE+=$'### Failed merges:\n\nThe following branches need to be merged manually into Batteries\' \'nightly-testing\':\n\n'
          for MERGE_INFO in $FAILED_MERGES; do
            IFS='|' read -r PR_NUMBER GITHUB_DIFF _ <<< "$MERGE_INFO"
            MESSAGE+=$(printf '- [lean-pr-testing-%s](%s) (adaptations for lean#%s)' "$PR_NUMBER" "$GITHUB_DIFF" "$PR_NUMBER")$'\n\n'
            MESSAGE+=$'```bash\n'
            MESSAGE+=$(printf 'scripts/merge-lean-testing-pr.sh %s' "$PR_NUMBER")$'\n'
            MESSAGE+=$'```\n\n'
          done
        else
          MESSAGE+=$'All branches were successfully merged!\n'
        fi

        # Output the message using the correct GitHub Actions syntax
        printf 'msg<<EOF\n%s\nEOF' "$MESSAGE" | tee "$GITHUB_OUTPUT"

    - name: Send message on Zulip
      if: steps.commit-bump.outputs.bumped == 'true' && env.branches_exist == 'true'
      uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2
      with:
        api-key: ${{ secrets.ZULIP_API_KEY }}
        email: 'github-mathlib4-bot@leanprover.zulipchat.com'
        organization-url: 'https://leanprover.zulipchat.com'
        to: 'nightly-testing'
        type: 'stream'
        topic: 'Mergeable lean testing PRs (Batteries)'
        content: |
          ${{ steps.zulip-message.outputs.msg }}