chore: attempt to restore Mathlib CI (#999)

leanprover-community · Oct 17, 2024 · cc0bc87 · fgdorais · Oct 18, 2024 · cc0bc87
1 parent d011c00
commit cc0bc87
Showing 1 changed file with 22 additions and 30 deletions.
diff --git a/.github/workflows/test_mathlib.yml b/.github/workflows/test_mathlib.yml
@@ -12,52 +12,44 @@ jobs:
     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
+      - name: Retrieve PR information
+        id: pr-info
+        uses: actions/github-script@v6
         with:
-          token: ${{ secrets.GITHUB_TOKEN }}
-          sourceRunId: ${{ github.event.workflow_run.id }}
+          script: |
+            const prNumber = context.payload.workflow_run.pull_requests[0].number;
+            const { data: pr } = await github.rest.pulls.get({
+              owner: context.repo.owner,
+              repo: context.repo.name,
+              pull_number: prNumber
+            });
+            core.setOutput('targetBranch', pr.base.ref);
+            core.setOutput('pullRequestNumber', pr.number);
+            core.exportVariable('HEAD_REPO', pr.head.repo.full_name);
+            core.exportVariable('HEAD_BRANCH', pr.head.ref);
 
       - name: Checkout mathlib4 repository
-        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.workflow-info.outputs.targetBranch == 'main'
+        if: steps.pr-info.outputs.pullRequestNumber != '' && steps.pr-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'
+      - 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: 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'
+        if: steps.pr-info.outputs.pullRequestNumber != '' && steps.pr-info.outputs.targetBranch == 'main'
         id: check_mathlib_tag
         env:
-          PR_NUMBER: ${{ steps.workflow-info.outputs.pullRequestNumber }}
+          PR_NUMBER: ${{ steps.pr-info.outputs.pullRequestNumber }}
           HEAD_REPO: ${{ env.HEAD_REPO }}
           HEAD_BRANCH: ${{ env.HEAD_BRANCH }}
         run: |
@@ -75,7 +67,7 @@ jobs:
             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
+            # 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
@@ -91,8 +83,8 @@ jobs:
           fi
 
       - name: Push changes
-        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.workflow-info.outputs.targetBranch == 'main'
+        if: steps.pr-info.outputs.pullRequestNumber != '' && steps.pr-info.outputs.targetBranch == 'main'
         env:
-          PR_NUMBER: ${{ steps.workflow-info.outputs.pullRequestNumber }}
+          PR_NUMBER: ${{ steps.pr-info.outputs.pullRequestNumber }}
         run: |
           git push origin batteries-pr-testing-$PR_NUMBER