discover-lean-pr-testing.yml

name: Discover `lean-pr-testing` branches

# This is derived from the Mathlib automation

# When the nightly toolchain is modified, it figures out which Lean
# PRs were included in the new nightly relative to the old one. It
# then attempts to merge their adaptation branches automatically.

on:
    push:
        branches:
            - nightly-testing
        paths:
            - lean-toolchain

jobs:
    discover-lean-pr-testing:
        runs-on: ubuntu-latest
        if: github.repository == 'leanprover/reference-manual'

        steps:
            - name: Checkout reference manual repository
              uses: actions/checkout@v4
              with:
                  ref: nightly-testing
                  fetch-depth: 0 # Fetch all branches

            - name: Set up Git
              run: |
                  git config --global user.name "github-actions"
                  git config --global user.email "github-actions@github.com"

            - name: Install elan
              run: |
                  set -o pipefail
                  curl -sSfL https://github.com/leanprover/elan/releases/download/v4.2.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
                  ./elan-init -y --default-toolchain none
                  echo "$HOME/.elan/bin" >> "$GITHUB_PATH"

            - name: Determine old and new lean-toolchain
              id: determine-toolchains
              run: |
                  # `lean-toolchain` contains a string of the form "leanprover/lean4:nightly-2024-11-20"
                  # We grab the part after the ":"
                  NEW=$(cut -f2 -d: lean-toolchain)

                  # Find the commit hash of the previous change to `lean-toolchain`
                  PREV_COMMIT=$(git log -2 --format=format:%H -- lean-toolchain | tail -1)

                  # Get the contents of `lean-toolchain` from the previous commit
                  # The "./" in front of the path is important for `git show`
                  OLD=$(git show "$PREV_COMMIT":./lean-toolchain | cut -f2 -d:)

                  echo "old=$OLD"
                  echo "new=$NEW"
                  echo "old=$OLD" >> "$GITHUB_OUTPUT"
                  echo "new=$NEW" >> "$GITHUB_OUTPUT"

            - name: Clone lean4 repository and get PRs
              id: get-prs
              run: |
                  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

                  # Use the OLD and NEW toolchains determined in the previous step
                  OLD="${{ steps.determine-toolchains.outputs.old }}"
                  NEW="${{ steps.determine-toolchains.outputs.new }}"

                  # Fetch the $OLD tag
                  git fetch --depth=1 origin tag "$OLD" --no-tags
                  # Fetch the $NEW tag.
                  # This will only fetch commits newer than previously fetched commits (ie $OLD)
                  git fetch origin tag "$NEW" --no-tags

                  # Find all commits to lean4 between the $OLD and $NEW toolchains
                  # and extract the github PR numbers
                  # (drop anything that doesn't look like a PR number from the final result)
                  PRS=$(git log --oneline "$OLD..$NEW" | sed 's/.*(#\([0-9]\+\))$/\1/' | grep -E '^[0-9]+$')

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

            - name: Use merged PRs information
              id: find-branches
              run: |
                  # Use the PRs from the previous step
                  PRS="${{ steps.get-prs.outputs.prs }}"
                  echo "=== PRS ========================="
                  echo "$PRS"
                  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")
                  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
                      if echo "$DIFF_FILES" | grep -v -e 'lake-manifest.json' -e 'lakefile.lean' -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, recording the outcome in the `branches_exist` variable
                  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: 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
                    # Temporarily checkout 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/${{ github.repository }}/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
                    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"