PR release #502
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
| # Push a release to the lean4-pr-releases repository, whenever someone pushes to a PR branch. | |
| # This needs to run with the `secrets.PR_RELEASES_TOKEN` token available, | |
| # but PR branches will generally come from forks, | |
| # so it is not possible to run this using the `pull_request` or `pull_request_target` workflows. | |
| # Instead we use `workflow_run`, which essentially allows us to escalate privileges | |
| # (but only runs the CI as described in the `master` branch, not in the PR branch). | |
| # The main specification/documentation for this workflow is at | |
| # https://leanprover-community.github.io/contribute/tags_and_branches.html | |
| # Keep that in sync! | |
| name: PR release | |
| on: | |
| workflow_run: # https://docs.github.com/en/actions/using-workflows/events-that-trigger-workflows#workflow_run | |
| workflows: [CI] | |
| types: [completed] | |
| jobs: | |
| on-success: | |
| runs-on: ubuntu-latest | |
| # Run even if CI fails, as long as build artifacts are available | |
| # The "Verify release artifacts exist" step will fail if necessary artifacts are missing | |
| if: github.event.workflow_run.event == 'pull_request' && github.repository == 'leanprover/lean4' | |
| steps: | |
| - name: Retrieve information about the original workflow | |
| uses: potiuk/get-workflow-origin@v1_1 # https://github.com/marketplace/actions/get-workflow-origin | |
| # This action is deprecated and archived, but it seems hard to find a better solution for getting the PR number | |
| # see https://github.com/orgs/community/discussions/25220 for some discussion | |
| id: workflow-info | |
| with: | |
| token: ${{ secrets.GITHUB_TOKEN }} | |
| sourceRunId: ${{ github.event.workflow_run.id }} | |
| - name: Download artifact from the previous workflow. | |
| if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} | |
| id: download-artifact | |
| uses: dawidd6/action-download-artifact@v11 # https://github.com/marketplace/actions/download-workflow-artifact | |
| with: | |
| run_id: ${{ github.event.workflow_run.id }} | |
| path: artifacts | |
| name: build-.* | |
| name_is_regexp: true | |
| # Verify artifacts were downloaded before any side effects (tag creation, release deletion). | |
| - name: Verify release artifacts exist | |
| if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} | |
| run: | | |
| shopt -s nullglob | |
| files=(artifacts/*/*) | |
| if [ ${#files[@]} -eq 0 ]; then | |
| echo "::error::No artifacts found matching artifacts/*/*" | |
| exit 1 | |
| fi | |
| echo "Found ${#files[@]} artifacts to upload:" | |
| printf '%s\n' "${files[@]}" | |
| - name: Push tag | |
| if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} | |
| run: | | |
| git init --bare lean4.git | |
| git -C lean4.git remote add origin https://github.com/${{ github.repository_owner }}/lean4.git | |
| git -C lean4.git fetch -n origin master | |
| git -C lean4.git fetch -n origin "${{ steps.workflow-info.outputs.sourceHeadSha }}" | |
| # Create both the original tag and the SHA-suffixed tag | |
| SHORT_SHA="${{ steps.workflow-info.outputs.sourceHeadSha }}" | |
| SHORT_SHA="${SHORT_SHA:0:7}" | |
| # Export the short SHA for use in subsequent steps | |
| echo "SHORT_SHA=${SHORT_SHA}" >> "$GITHUB_ENV" | |
| git -C lean4.git tag -f pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} "${{ steps.workflow-info.outputs.sourceHeadSha }}" | |
| git -C lean4.git tag -f pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-"${SHORT_SHA}" "${{ steps.workflow-info.outputs.sourceHeadSha }}" | |
| git -C lean4.git remote add pr-releases https://foo:'${{ secrets.PR_RELEASES_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-pr-releases.git | |
| git -C lean4.git push -f pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} | |
| git -C lean4.git push -f pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-"${SHORT_SHA}" | |
| - name: Delete existing releases if present | |
| if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} | |
| run: | | |
| # Delete any existing releases for this PR. | |
| # The short format release is always recreated with the latest commit. | |
| # The SHA-suffixed release should be unique per commit, but delete just in case. | |
| gh release delete --repo ${{ github.repository_owner }}/lean4-pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} -y || true | |
| gh release delete --repo ${{ github.repository_owner }}/lean4-pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }} -y || true | |
| env: | |
| GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }} | |
| # We use `gh release create` instead of `softprops/action-gh-release` because | |
| # the latter enumerates all releases to check for existing ones, which fails | |
| # when the repository has more than 10000 releases (GitHub API pagination limit). | |
| # Upstream fix: https://github.com/softprops/action-gh-release/pull/725 | |
| - name: Release (short format) | |
| if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} | |
| run: | | |
| # There are coredump files in deeper subdirectories; artifacts/*/* gets the release archives. | |
| gh release create \ | |
| --repo ${{ github.repository_owner }}/lean4-pr-releases \ | |
| --title "Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }}" \ | |
| --notes "" \ | |
| pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} \ | |
| artifacts/*/* | |
| env: | |
| GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }} | |
| - name: Release (SHA-suffixed format) | |
| if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} | |
| run: | | |
| gh release create \ | |
| --repo ${{ github.repository_owner }}/lean4-pr-releases \ | |
| --title "Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }} (${{ steps.workflow-info.outputs.sourceHeadSha }})" \ | |
| --notes "" \ | |
| pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }} \ | |
| artifacts/*/* | |
| env: | |
| GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }} | |
| - name: Report release status (short format) | |
| if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} | |
| uses: actions/github-script@v8 | |
| with: | |
| script: | | |
| await github.rest.repos.createCommitStatus({ | |
| owner: context.repo.owner, | |
| repo: context.repo.repo, | |
| sha: "${{ steps.workflow-info.outputs.sourceHeadSha }}", | |
| state: "success", | |
| context: "PR toolchain", | |
| description: "${{ github.repository_owner }}/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}", | |
| }); | |
| - name: Report release status (SHA-suffixed format) | |
| if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} | |
| uses: actions/github-script@v8 | |
| with: | |
| script: | | |
| await github.rest.repos.createCommitStatus({ | |
| owner: context.repo.owner, | |
| repo: context.repo.repo, | |
| sha: "${{ steps.workflow-info.outputs.sourceHeadSha }}", | |
| state: "success", | |
| context: "PR toolchain (SHA-suffixed)", | |
| description: "${{ github.repository_owner }}/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}", | |
| }); | |
| - name: Add toolchain-available label | |
| if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} | |
| uses: actions/github-script@v8 | |
| with: | |
| script: | | |
| await github.rest.issues.addLabels({ | |
| issue_number: ${{ steps.workflow-info.outputs.pullRequestNumber }}, | |
| owner: context.repo.owner, | |
| repo: context.repo.repo, | |
| labels: ['toolchain-available'] | |
| }) | |
| # Next, determine the most recent nightly release in this PR's history. | |
| - name: Find most recent nightly in feature branch | |
| id: most-recent-nightly-tag | |
| if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} | |
| run: | | |
| git -C lean4.git remote add nightly https://github.com/leanprover/lean4-nightly.git | |
| git -C lean4.git fetch nightly '+refs/tags/nightly-*:refs/tags/nightly-*' | |
| git -C lean4.git tag --merged "${{ steps.workflow-info.outputs.sourceHeadSha }}" --list "nightly-*" \ | |
| | sort -rV | head -n 1 | sed "s/^nightly-*/MOST_RECENT_NIGHTLY=/" | tee -a "$GITHUB_ENV" | |
| - name: 'Setup jq' | |
| if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} | |
| uses: dcarbone/install-jq-action@v3.2.0 | |
| # Generate a token for posting comments to Lean PRs about mathlib compatibility. | |
| # This app is in the leanprover org and installed on leanprover/lean4. | |
| - name: Generate GitHub App token for Lean PR comments | |
| if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} | |
| id: mathlib-comment-token | |
| uses: actions/create-github-app-token@3ff1caaa28b64c9cc276ce0a02e2ff584f3900c5 # v2.0.2 | |
| with: | |
| app-id: ${{ secrets.MATHLIB_LEAN_PR_TESTING_APP_ID }} | |
| private-key: ${{ secrets.MATHLIB_LEAN_PR_TESTING_PRIVATE_KEY }} | |
| owner: leanprover | |
| repositories: lean4 | |
| # Check that the most recently nightly coincides with 'git merge-base HEAD master' | |
| - name: Check merge-base and nightly-testing-YYYY-MM-DD for Mathlib/Batteries | |
| if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} | |
| id: ready | |
| run: | | |
| echo "Most recent nightly release in your branch: $MOST_RECENT_NIGHTLY" | |
| NIGHTLY_SHA=$(git -C lean4.git rev-parse "nightly-$MOST_RECENT_NIGHTLY^{commit}") | |
| echo "SHA of most recent nightly release: $NIGHTLY_SHA" | |
| MERGE_BASE_SHA=$(git -C lean4.git merge-base origin/master "${{ steps.workflow-info.outputs.sourceHeadSha }}") | |
| echo "SHA of merge-base: $MERGE_BASE_SHA" | |
| if [ "$NIGHTLY_SHA" = "$MERGE_BASE_SHA" ]; then | |
| echo "The merge base of this PR coincides with the nightly release" | |
| MATHLIB_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/mathlib4-nightly-testing.git nightly-testing-"$MOST_RECENT_NIGHTLY")" | |
| if [[ -n "$MATHLIB_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' 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 | |
| echo "The most recently nightly tag on this branch has SHA: $NIGHTLY_SHA" | |
| echo "but 'git merge-base origin/master HEAD' reported: $MERGE_BASE_SHA" | |
| git -C lean4.git log -10 origin/master | |
| git -C lean4.git fetch origin nightly-with-mathlib | |
| NIGHTLY_WITH_MATHLIB_SHA="$(git -C lean4.git rev-parse "origin/nightly-with-mathlib")" | |
| MESSAGE="- ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_WITH_MATHLIB_SHA\`." | |
| fi | |
| if [[ -n "$MESSAGE" ]]; then | |
| # Check if force-mathlib-ci label is present | |
| # Use GITHUB_TOKEN for read-only label fetch (MATHLIB4_COMMENT_BOT is only for posting comments) | |
| LABELS="$(curl --retry 3 --location --silent \ | |
| -H "Authorization: token ${{ secrets.GITHUB_TOKEN }}" \ | |
| -H "Accept: application/vnd.github.v3+json" \ | |
| "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/labels" \ | |
| | jq -r '.[].name')" | |
| if echo "$LABELS" | grep -q "^force-mathlib-ci$"; then | |
| echo "force-mathlib-ci label detected, forcing CI despite issues" | |
| MESSAGE="Forcing Mathlib CI because the \`force-mathlib-ci\` label is present, despite problem: $MESSAGE" | |
| FORCE_CI=true | |
| else | |
| MESSAGE="$MESSAGE You can force Mathlib CI using the \`force-mathlib-ci\` label." | |
| fi | |
| echo "Checking existing messages" | |
| # The code for updating comments is duplicated in mathlib's | |
| # scripts/lean-pr-testing-comments.sh | |
| # so keep in sync | |
| # Use GitHub API to check if a comment already exists | |
| existing_comment="$(curl --retry 3 --location --silent \ | |
| -H "Authorization: token ${{ steps.mathlib-comment-token.outputs.token }}" \ | |
| -H "Accept: application/vnd.github.v3+json" \ | |
| "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments" \ | |
| | jq 'first(.[] | select(.body | test("^- . Mathlib") or startswith("Mathlib CI status")) | select(.user.login == "mathlib-lean-pr-testing[bot]"))')" | |
| existing_comment_id="$(echo "$existing_comment" | jq -r .id)" | |
| existing_comment_body="$(echo "$existing_comment" | jq -r .body)" | |
| if [[ "$existing_comment_body" != *"$MESSAGE"* ]]; then | |
| MESSAGE="$MESSAGE ($(date "+%Y-%m-%d %H:%M:%S"))" | |
| echo "Posting message to the comments: $MESSAGE" | |
| # Append new result to the existing comment or post a new comment | |
| # Use the mathlib-lean-pr-testing app token so Mathlib CI can subsequently edit the comment. | |
| if [ -z "$existing_comment_id" ]; then | |
| INTRO="Mathlib CI status ([docs](https://leanprover-community.github.io/contribute/tags_and_branches.html)):" | |
| # Post new comment with a bullet point | |
| echo "Posting as new comment at leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments" | |
| curl -L -s \ | |
| -X POST \ | |
| -H "Authorization: token ${{ steps.mathlib-comment-token.outputs.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/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments" | |
| else | |
| # Append new result to the existing comment | |
| echo "Appending to existing comment at leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments" | |
| curl -L -s \ | |
| -X PATCH \ | |
| -H "Authorization: token ${{ steps.mathlib-comment-token.outputs.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" | |
| fi | |
| else | |
| echo "The message already exists in the comment body." | |
| fi | |
| if [[ "$FORCE_CI" == "true" ]]; then | |
| echo "mathlib_ready=true" >> "$GITHUB_OUTPUT" | |
| else | |
| echo "mathlib_ready=false" >> "$GITHUB_OUTPUT" | |
| fi | |
| else | |
| echo "mathlib_ready=true" >> "$GITHUB_OUTPUT" | |
| fi | |
| - name: Check merge-base and nightly-testing-YYYY-MM-DD for reference manual | |
| if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} | |
| id: reference-manual-ready | |
| run: | | |
| echo "Most recent nightly release in your branch: $MOST_RECENT_NIGHTLY" | |
| NIGHTLY_SHA=$(git -C lean4.git rev-parse "nightly-$MOST_RECENT_NIGHTLY^{commit}") | |
| echo "SHA of most recent nightly release: $NIGHTLY_SHA" | |
| MERGE_BASE_SHA=$(git -C lean4.git merge-base origin/master "${{ steps.workflow-info.outputs.sourceHeadSha }}") | |
| echo "SHA of merge-base: $MERGE_BASE_SHA" | |
| if [ "$NIGHTLY_SHA" = "$MERGE_BASE_SHA" ]; then | |
| echo "The merge base of this PR coincides with the nightly release" | |
| MANUAL_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover/reference-manual.git nightly-testing-"$MOST_RECENT_NIGHTLY")" | |
| if [[ -n "$MANUAL_REMOTE_TAGS" ]]; then | |
| echo "... and the reference manual has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag." | |
| MESSAGE="" | |
| else | |
| echo "... but the reference manual does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag." | |
| MESSAGE="- ❗ Reference manual 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-manual\`, reference manual CI should run now." | |
| fi | |
| else | |
| echo "The most recently nightly tag on this branch has SHA: $NIGHTLY_SHA" | |
| echo "but 'git merge-base origin/master HEAD' reported: $MERGE_BASE_SHA" | |
| git -C lean4.git log -10 origin/master | |
| git -C lean4.git fetch origin nightly-with-manual | |
| NIGHTLY_WITH_MANUAL_SHA="$(git -C lean4.git rev-parse "origin/nightly-with-manual")" | |
| MESSAGE="- ❗ Reference manual CI will not be attempted unless your PR branches off the \`nightly-with-manual\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_WITH_MANUAL_SHA\`." | |
| fi | |
| if [[ -n "$MESSAGE" ]]; then | |
| # Check if force-manual-ci label is present | |
| LABELS="$(curl --retry 3 --location --silent \ | |
| -H "Authorization: token ${{ secrets.MANUAL_COMMENT_BOT }}" \ | |
| -H "Accept: application/vnd.github.v3+json" \ | |
| "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/labels" \ | |
| | jq -r '.[].name')" | |
| if echo "$LABELS" | grep -q "^force-manual-ci$"; then | |
| echo "force-manual-ci label detected, forcing CI despite issues" | |
| MESSAGE="Forcing reference manual CI because the \`force-manual-ci\` label is present, despite problem: $MESSAGE" | |
| FORCE_CI=true | |
| else | |
| MESSAGE="$MESSAGE You can force reference manual CI using the \`force-manual-ci\` label." | |
| fi | |
| echo "Checking existing messages" | |
| # The code for updating comments is duplicated in the reference manual's | |
| # scripts/lean-pr-testing-comments.sh | |
| # so keep in sync | |
| # Use GitHub API to check if a comment already exists | |
| existing_comment="$(curl --retry 3 --location --silent \ | |
| -H "Authorization: token ${{ secrets.MANUAL_COMMENT_BOT }}" \ | |
| -H "Accept: application/vnd.github.v3+json" \ | |
| "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments" \ | |
| | jq 'first(.[] | select(.body | test("^- . Manual") or startswith("Reference manual CI status")) | select(.user.login == "leanprover-bot"))')" | |
| existing_comment_id="$(echo "$existing_comment" | jq -r .id)" | |
| existing_comment_body="$(echo "$existing_comment" | jq -r .body)" | |
| if [[ "$existing_comment_body" != *"$MESSAGE"* ]]; then | |
| MESSAGE="$MESSAGE ($(date "+%Y-%m-%d %H:%M:%S"))" | |
| echo "Posting message to the comments: $MESSAGE" | |
| # Append new result to the existing comment or post a new comment | |
| # It's essential we use the MANUAL_COMMENT_BOT token here, so that reference manual CI can subsequently edit the comment. | |
| if [ -z "$existing_comment_id" ]; then | |
| INTRO="Reference manual CI status:" | |
| # Post new comment with a bullet point | |
| echo "Posting as new comment at leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments" | |
| curl -L -s \ | |
| -X POST \ | |
| -H "Authorization: token ${{ secrets.MANUAL_COMMENT_BOT }}" \ | |
| -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/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments" | |
| else | |
| # Append new result to the existing comment | |
| echo "Appending to existing comment at leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments" | |
| curl -L -s \ | |
| -X PATCH \ | |
| -H "Authorization: token ${{ secrets.MANUAL_COMMENT_BOT }}" \ | |
| -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" | |
| fi | |
| else | |
| echo "The message already exists in the comment body." | |
| fi | |
| if [[ "$FORCE_CI" == "true" ]]; then | |
| echo "manual_ready=true" >> "$GITHUB_OUTPUT" | |
| else | |
| echo "manual_ready=false" >> "$GITHUB_OUTPUT" | |
| fi | |
| else | |
| echo "manual_ready=true" >> "$GITHUB_OUTPUT" | |
| fi | |
| - name: Report mathlib base | |
| if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true' }} | |
| uses: actions/github-script@v8 | |
| with: | |
| script: | | |
| const description = | |
| process.env.MOST_RECENT_NIGHTLY ? | |
| "nightly-" + process.env.MOST_RECENT_NIGHTLY : | |
| "not branched off nightly"; | |
| await github.rest.repos.createCommitStatus({ | |
| owner: context.repo.owner, | |
| repo: context.repo.repo, | |
| sha: "${{ steps.workflow-info.outputs.sourceHeadSha }}", | |
| state: "success", | |
| context: "PR branched off:", | |
| description: description, | |
| }); | |
| # We next automatically create a Batteries branch using this toolchain. | |
| # Batteries doesn't itself have a mechanism to report results of CI from this branch back to Lean | |
| # Instead this is taken care of by Mathlib CI, which will fail if Batteries fails. | |
| # Generate a token from the mathlib-nightly-testing GitHub App for cross-org access | |
| - name: Generate GitHub App token for leanprover-community repos | |
| if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true' | |
| id: mathlib-app-token | |
| uses: actions/create-github-app-token@3ff1caaa28b64c9cc276ce0a02e2ff584f3900c5 # v2.0.2 | |
| with: | |
| app-id: ${{ secrets.MATHLIB_NIGHTLY_TESTING_APP_ID }} | |
| private-key: ${{ secrets.MATHLIB_NIGHTLY_TESTING_PRIVATE_KEY }} | |
| owner: leanprover-community | |
| repositories: batteries,mathlib4-nightly-testing | |
| - name: Cleanup workspace | |
| if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true' | |
| run: | | |
| sudo rm -rf ./* | |
| # Checkout the Batteries repository with all branches | |
| - name: Checkout Batteries repository | |
| if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true' | |
| uses: actions/checkout@v6 | |
| with: | |
| repository: leanprover-community/batteries | |
| token: ${{ steps.mathlib-app-token.outputs.token }} | |
| ref: nightly-testing | |
| fetch-depth: 0 # This ensures we check out all tags and branches. | |
| filter: tree:0 | |
| - name: Check if tag exists | |
| if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true' | |
| id: check_batteries_tag | |
| run: | | |
| git config user.name "leanprover-community-mathlib4-bot" | |
| git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com" | |
| 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 "Couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' tag at Batteries. Falling back to 'nightly-testing'." | |
| BASE=nightly-testing | |
| fi | |
| echo "Using base branch: $BASE" | |
| EXISTS="$(git ls-remote --heads origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} | wc -l)" | |
| echo "Branch exists: $EXISTS" | |
| if [ "$EXISTS" = "0" ]; then | |
| echo "Branch does not exist, creating it." | |
| git switch -c lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} "$BASE" | |
| echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}" > lean-toolchain | |
| git add lean-toolchain | |
| git commit --allow-empty -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}" | |
| else | |
| echo "Branch already exists, updating lean-toolchain." | |
| git switch lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} | |
| # The Batteries `nightly-testing` or `nightly-testing-YYYY-MM-DD` branch 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 | |
| echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}" > lean-toolchain | |
| git add lean-toolchain | |
| git commit --allow-empty -m "Update lean-toolchain for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}" | |
| fi | |
| - name: Push changes | |
| if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true' | |
| run: | | |
| git push origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} | |
| # We next automatically create a Mathlib branch using this toolchain. | |
| # Mathlib CI will be responsible for reporting back success or failure | |
| # to the PR comments asynchronously. | |
| - name: Cleanup workspace | |
| if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true' | |
| run: | | |
| sudo rm -rf ./* | |
| # Checkout the mathlib4 repository with all branches | |
| - name: Checkout mathlib4 repository | |
| if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true' | |
| uses: actions/checkout@v6 | |
| with: | |
| repository: leanprover-community/mathlib4-nightly-testing | |
| token: ${{ steps.mathlib-app-token.outputs.token }} | |
| ref: nightly-testing | |
| fetch-depth: 0 # This ensures we check out all tags and branches. | |
| filter: tree:0 | |
| - name: install elan | |
| run: | | |
| set -o pipefail | |
| curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz | |
| ./elan-init -y --default-toolchain none | |
| echo "$HOME/.elan/bin" >> "${GITHUB_PATH}" | |
| - name: Check if tag exists | |
| if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true' | |
| id: check_mathlib_tag | |
| run: | | |
| git config user.name "leanprover-community-mathlib4-bot" | |
| git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com" | |
| 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 "Couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' branch at Mathlib. Falling back to 'nightly-testing'." | |
| BASE=nightly-testing | |
| fi | |
| echo "Using base tag: $BASE" | |
| EXISTS="$(git ls-remote --heads origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} | wc -l)" | |
| echo "Branch exists: $EXISTS" | |
| if [ "$EXISTS" = "0" ]; then | |
| echo "Branch does not exist, creating it." | |
| git switch -c lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} "$BASE" | |
| echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}" > lean-toolchain | |
| git add lean-toolchain | |
| sed -i 's,require "leanprover-community" / "batteries" @ git ".\+",require "leanprover-community" / "batteries" @ git "lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}",' lakefile.lean | |
| lake update batteries | |
| git add lakefile.lean lake-manifest.json | |
| git commit --allow-empty -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}" | |
| else | |
| echo "Branch already exists, updating lean-toolchain and bumping Batteries." | |
| git switch lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} | |
| # The Mathlib `nightly-testing` branch 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 | |
| echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}" > lean-toolchain | |
| git add lean-toolchain | |
| lake update batteries | |
| git add lake-manifest.json | |
| git commit --allow-empty -m "Update lean-toolchain for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}" | |
| fi | |
| - name: Push changes | |
| if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true' | |
| run: | | |
| git push origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} | |
| - name: Add mathlib4-nightly-available label | |
| if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true' | |
| uses: actions/github-script@v8 | |
| with: | |
| script: | | |
| await github.rest.issues.addLabels({ | |
| issue_number: ${{ steps.workflow-info.outputs.pullRequestNumber }}, | |
| owner: context.repo.owner, | |
| repo: context.repo.repo, | |
| labels: ['mathlib4-nightly-available'] | |
| }) | |
| # We next automatically create a reference manual branch using this toolchain. | |
| # Reference manual CI will be responsible for reporting back success or failure | |
| # to the PR comments asynchronously (and thus transitively SubVerso/Verso). | |
| - name: Cleanup workspace | |
| if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.reference-manual-ready.outputs.manual_ready == 'true' | |
| run: | | |
| sudo rm -rf ./* | |
| # Checkout the reference manual repository with all branches | |
| - name: Checkout mathlib4 repository | |
| if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.reference-manual-ready.outputs.manual_ready == 'true' | |
| uses: actions/checkout@v6 | |
| with: | |
| repository: leanprover/reference-manual | |
| token: ${{ secrets.MANUAL_PR_BOT }} | |
| ref: nightly-testing | |
| fetch-depth: 0 # This ensures we check out all tags and branches. | |
| filter: tree:0 | |
| - name: Check if tag in reference manual exists | |
| if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.reference-manual-ready.outputs.manual_ready == 'true' | |
| id: check_manual_tag | |
| run: | | |
| git config user.name "leanprover-bot" | |
| git config user.email "leanprover-bot@lean-fro.org" | |
| 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 "Couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' branch in the reference manual. Falling back to 'nightly-testing'." | |
| BASE=nightly-testing | |
| fi | |
| echo "Using base tag: $BASE" | |
| EXISTS="$(git ls-remote --heads origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} | wc -l)" | |
| echo "Branch exists: $EXISTS" | |
| if [ "$EXISTS" = "0" ]; then | |
| echo "Branch does not exist, creating it." | |
| git switch -c lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} "$BASE" | |
| echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}" > lean-toolchain | |
| git add lean-toolchain | |
| git add lakefile.lean lake-manifest.json | |
| git commit --allow-empty -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}" | |
| else | |
| echo "Branch already exists, updating lean-toolchain." | |
| git switch lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} | |
| # The reference manual's `nightly-testing` branch 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 | |
| echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}" > lean-toolchain | |
| git add lean-toolchain | |
| git add lake-manifest.json | |
| git commit --allow-empty -m "Update lean-toolchain for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}" | |
| fi | |
| - name: Push changes | |
| if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.reference-manual-ready.outputs.manual_ready == 'true' | |
| run: | | |
| git push origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} |