chore: pr-release: revert to originally used action to get PR number (#…

…3072)

Getting the original PR number from a `workflow_run` cleanly and
reliably seems to be
basically impossible. See
<https://github.com/orgs/community/discussions/25220> for a discussion.
So for now let’s go back to the working state, even though it’s
deprecated and throws warnings.

.github/workflows/pr-release.yml

@@ -18,33 +18,15 @@ jobs:
     runs-on: ubuntu-latest
     if: github.event.workflow_run.conclusion == 'success' && github.event.workflow_run.event == 'pull_request' && github.repository == 'leanprover/lean4'
     steps:
-      - name: Retrieve PR number and head commit
-        uses: actions/github-script@v7
+      - name: Retrieve information about the original workflow
+        uses: potiuk/get-workflow-origin@v1_1 # https://github.com/marketplace/actions/get-workflow-origin
+        # This action is deprecated and archived, but it seems hard to find a better solution for getting the PR number
+        # see https://github.com/orgs/community/discussions/25220 for some discussion
         id: workflow-info
         with:
-          script: |
-            const run_id = context.payload.workflow_run.id;
-            console.log(`Querying workflow run data for run_id ${run_id}.`);
-            
-            github.rest.actions.getWorkflowRun({
-                owner: context.repo.owner,
-                repo: context.repo.repo,
-                run_id: run_id
-            })
-            .then(reply => {
-                if (reply.data.pull_requests && reply.data.pull_requests.length > 0) {
-                    core.setOutput('pullRequestNumber', reply.data.pull_requests[0].number);
-                    core.setOutput('sourceHeadSha', reply.data.pull_requests[0].head.sha);
-                } else {
-                    console.log("Odd, no pull-request-data in workflow data?");
-                    console.log(`reply.data: ${JSON.stringify(reply.data, null, 2)}`);
-                    core.setFailed("Unexpected result from github.rest.actions.getWorkflowRun");
-                }
-            })
-            .catch(error => {
-                console.error(error);
-                core.setFailed("Error querying workflow run data: " + error.message);
-            });
+          token: ${{ secrets.GITHUB_TOKEN }}
+          sourceRunId: ${{ github.event.workflow_run.id }}
+
       - name: Download artifact from the previous workflow.
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         id: download-artifact