Skip to content

Commit

Permalink
chore: only test Mathlib on PRs to main (#977)
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em authored Oct 3, 2024
1 parent 7815c9d commit 34e690e
Showing 1 changed file with 5 additions and 4 deletions.
9 changes: 5 additions & 4 deletions .github/workflows/test_mathlib.yml
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ jobs:
sourceRunId: ${{ github.event.workflow_run.id }}

- name: Checkout mathlib4 repository
if: steps.workflow-info.outputs.pullRequestNumber != ''
if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.workflow-info.outputs.targetBranch == 'main'
uses: actions/checkout@v4
with:
repository: leanprover-community/mathlib4
Expand All @@ -29,14 +29,15 @@ jobs:
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 != ''
if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.workflow-info.outputs.targetBranch == 'main'
id: pr-info
uses: actions/github-script@v6
env:
Expand All @@ -53,7 +54,7 @@ jobs:
core.exportVariable('HEAD_BRANCH', pr.head.ref);
- name: Check if tag exists
if: steps.workflow-info.outputs.pullRequestNumber != ''
if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.workflow-info.outputs.targetBranch == 'main'
id: check_mathlib_tag
env:
PR_NUMBER: ${{ steps.workflow-info.outputs.pullRequestNumber }}
Expand Down Expand Up @@ -90,7 +91,7 @@ jobs:
fi
- name: Push changes
if: steps.workflow-info.outputs.pullRequestNumber != ''
if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.workflow-info.outputs.targetBranch == 'main'
env:
PR_NUMBER: ${{ steps.workflow-info.outputs.pullRequestNumber }}
run: |
Expand Down

0 comments on commit 34e690e

Please sign in to comment.