Test Mathlib #13
This file contains 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: Retrieve information about the original workflow | |
| uses: potiuk/get-workflow-origin@v1_1 | |
| id: workflow-info | |
| with: | |
| token: ${{ secrets.GITHUB_TOKEN }} | |
| sourceRunId: ${{ github.event.workflow_run.id }} | |
| - name: Checkout mathlib4 repository | |
| if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.workflow-info.outputs.targetBranch == 'main' | |
| uses: actions/checkout@v4 | |
| with: | |
| repository: leanprover-community/mathlib4 | |
| token: ${{ secrets.MATHLIB4_BOT }} | |
| ref: master | |
| fetch-depth: 0 | |
| - name: install elan | |
| if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.workflow-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: Retrieve PR information | |
| if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.workflow-info.outputs.targetBranch == 'main' | |
| id: pr-info | |
| uses: actions/github-script@v6 | |
| env: | |
| PR_NUMBER: ${{ steps.workflow-info.outputs.pullRequestNumber }} | |
| with: | |
| script: | | |
| const prNumber = process.env.PR_NUMBER; | |
| const { data: pr } = await github.rest.pulls.get({ | |
| owner: context.repo.owner, | |
| repo: context.repo.repo, | |
| pull_number: prNumber | |
| }); | |
| core.exportVariable('HEAD_REPO', pr.head.repo.full_name); | |
| core.exportVariable('HEAD_BRANCH', pr.head.ref); | |
| - name: Check if tag exists | |
| if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.workflow-info.outputs.targetBranch == 'main' | |
| id: check_mathlib_tag | |
| env: | |
| PR_NUMBER: ${{ steps.workflow-info.outputs.pullRequestNumber }} | |
| HEAD_REPO: ${{ env.HEAD_REPO }} | |
| HEAD_BRANCH: ${{ env.HEAD_BRANCH }} | |
| run: | | |
| git config user.name "leanprover-community-mathlib4-bot" | |
| git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com" | |
| echo "PR info: $HEAD_REPO $HEAD_BRANCH" | |
| BASE=master | |
| echo "Using base tag: $BASE" | |
| EXISTS="$(git ls-remote --heads origin 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" | |
| # Use the fork and branch name to modify the lakefile.lean | |
| 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.workflow-info.outputs.pullRequestNumber != '' && steps.workflow-info.outputs.targetBranch == 'main' | |
| env: | |
| PR_NUMBER: ${{ steps.workflow-info.outputs.pullRequestNumber }} | |
| run: | | |
| git push origin batteries-pr-testing-$PR_NUMBER |