From cc0bc876eeef0518ddc1c8d3bd6f48cc83e68901 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Thu, 17 Oct 2024 17:42:39 +1100
Subject: [PATCH] chore: attempt to restore Mathlib CI (#999)

---
 .github/workflows/test_mathlib.yml | 52 +++++++++++++-----------------
 1 file changed, 22 insertions(+), 30 deletions(-)

diff --git a/.github/workflows/test_mathlib.yml b/.github/workflows/test_mathlib.yml
index 8eca882a4c..efce8db636 100644
--- a/.github/workflows/test_mathlib.yml
+++ b/.github/workflows/test_mathlib.yml
@@ -12,15 +12,24 @@ 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
@@ -28,36 +37,19 @@ jobs:
           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