Bump toolchain and merge pr-testing branches #150
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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 }} |