mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
624 lines
35 KiB
YAML
624 lines
35 KiB
YAML
# 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 }}
|