Test Mathlib #9703
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
| # Test Mathlib against a Batteries PR | |
| name: Test Mathlib | |
| on: | |
| workflow_run: | |
| workflows: [ci] | |
| types: [completed] | |
| jobs: | |
| on-success: | |
| runs-on: ubuntu-latest | |
| if: github.event.workflow_run.conclusion == 'success' && github.event.workflow_run.event == 'pull_request' && github.repository == 'leanprover-community/batteries' | |
| steps: | |
| - name: Checkout PR | |
| uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 | |
| with: | |
| fetch-depth: 0 | |
| - name: Get PR info | |
| id: pr-info | |
| run: | | |
| echo "pullRequestNumber=$(gh pr list --search $SHA --json number -q '.[0].number' || echo '')" >> $GITHUB_OUTPUT | |
| echo "targetBranch=$(gh pr list --search $SHA --json baseRefName -q '.[0].baseRefName' || echo '')" >> $GITHUB_OUTPUT | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| SHA: ${{ github.event.workflow_run.head_sha }} | |
| - name: Generate app token | |
| if: steps.pr-info.outputs.pullRequestNumber != '' && steps.pr-info.outputs.targetBranch == 'main' | |
| 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 }} | |
| owner: leanprover-community | |
| repositories: mathlib4,mathlib4-nightly-testing | |
| - name: Checkout mathlib4 repository | |
| if: steps.pr-info.outputs.pullRequestNumber != '' && steps.pr-info.outputs.targetBranch == 'main' | |
| uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 | |
| with: | |
| repository: leanprover-community/mathlib4 | |
| token: ${{ steps.app-token.outputs.token }} | |
| ref: master | |
| fetch-depth: 0 | |
| - name: Add nightly-testing remote | |
| if: steps.pr-info.outputs.pullRequestNumber != '' && steps.pr-info.outputs.targetBranch == 'main' | |
| run: | | |
| git remote add nightly-testing https://github.com/leanprover-community/mathlib4-nightly-testing.git | |
| git fetch nightly-testing | |
| - name: Install elan | |
| if: steps.pr-info.outputs.pullRequestNumber != '' && steps.pr-info.outputs.targetBranch == 'main' | |
| 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 branch exists | |
| if: steps.pr-info.outputs.pullRequestNumber != '' && steps.pr-info.outputs.targetBranch == 'main' | |
| id: check_mathlib_tag | |
| env: | |
| PR_NUMBER: ${{ steps.pr-info.outputs.pullRequestNumber }} | |
| HEAD_REPO: ${{ github.event.workflow_run.head_repository.full_name }} | |
| HEAD_BRANCH: ${{ github.event.workflow_run.head_branch }} | |
| run: | | |
| git config user.name "mathlib-nightly-testing[bot]" | |
| git config user.email "mathlib-nightly-testing[bot]@users.noreply.github.com" | |
| echo "PR info: $HEAD_REPO $HEAD_BRANCH" | |
| BASE=master | |
| echo "Using base tag: $BASE" | |
| EXISTS="$(git ls-remote --heads nightly-testing batteries-pr-testing-$PR_NUMBER | wc -l)" | |
| echo "Branch exists: $EXISTS" | |
| if [ "$EXISTS" = "0" ]; then | |
| echo "Branch does not exist, creating it." | |
| git switch -c batteries-pr-testing-$PR_NUMBER "$BASE" | |
| # Modify the lakefile.lean with the fork and branch name | |
| sed -i "s,require \"leanprover-community\" / \"batteries\" @ git \".\+\",require \"leanprover-community\" / \"batteries\" from git \"https://github.com/$HEAD_REPO\" @ \"$HEAD_BRANCH\",g" lakefile.lean | |
| lake update batteries | |
| git add lakefile.lean lake-manifest.json | |
| git commit -m "Update Batteries branch for testing https://github.com/leanprover-community/batteries/pull/$PR_NUMBER" | |
| else | |
| echo "Branch already exists, merging $BASE and bumping Batteries." | |
| git switch batteries-pr-testing-$PR_NUMBER | |
| git merge "$BASE" --strategy-option ours --no-commit --allow-unrelated-histories | |
| lake update batteries | |
| git add lake-manifest.json | |
| git commit --allow-empty -m "Trigger CI for https://github.com/leanprover-community/batteries/pull/$PR_NUMBER" | |
| fi | |
| - name: Push changes | |
| if: steps.pr-info.outputs.pullRequestNumber != '' && steps.pr-info.outputs.targetBranch == 'main' | |
| env: | |
| PR_NUMBER: ${{ steps.pr-info.outputs.pullRequestNumber }} | |
| run: | | |
| git push nightly-testing batteries-pr-testing-$PR_NUMBER |