From 6861474e012f3b72b218137699cda93731669602 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Tue, 29 Aug 2023 14:11:45 +1000
Subject: [PATCH] feat: create release at lean4-pr-releases for each PR (#2448)

---
 .github/workflows/pr-release.yml | 69 ++++++++++++++++++++++++++++++++
 1 file changed, 69 insertions(+)
 create mode 100644 .github/workflows/pr-release.yml

diff --git a/.github/workflows/pr-release.yml b/.github/workflows/pr-release.yml
new file mode 100644
index 0000000000..dc484669f2
--- /dev/null
+++ b/.github/workflows/pr-release.yml
@@ -0,0 +1,69 @@
+# Push a release to the lean4-pr-releases repository, whenever someone pushes to a PR branch.
+
+# This needs to run with the `secrets.PR_RELEASES_TOKEN` token available,
+# but PR branches will generally come from forks,
+# so it is not possible to run this using the `pull_request` or `pull_request_target` workflows.
+# Instead we use `workflow_run`, which essentially allows us to escalate privileges
+# (but only runs the CI as described in the `master` branch, not in the PR branch).
+
+name: PR release
+
+on:
+  workflow_run: # https://docs.github.com/en/actions/using-workflows/events-that-trigger-workflows#workflow_run
+    workflows: [CI]
+    types: [completed]
+
+jobs:
+  on-success:
+    runs-on: ubuntu-latest
+    if: ${{ github.event.workflow_run.conclusion == 'success' }}
+    steps:
+      - name: Retrieve information about the original workflow
+        uses: potiuk/get-workflow-origin@v1_1 # https://github.com/marketplace/actions/get-workflow-origin
+        id: workflow-info
+        with:
+          token: ${{ secrets.GITHUB_TOKEN }}
+          sourceRunId: ${{ github.event.workflow_run.id }}
+      - name: Checkout
+        # Only proceed if the previous workflow had a pull request number.
+        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
+        uses: actions/checkout@v3
+        with:
+          token: ${{ secrets.PR_RELEASES_TOKEN }}
+          # Since `workflow_run` runs on master, we need to specify which commit to check out,
+          # so that we tag the PR.
+          ref: ${{ steps.workflow-info.outputs.targetCommitSha }}
+          # We need a full checkout, so that we can push the PR commits to the `lean4-pr-releases` repo.
+          fetch-depth: 0
+
+      - name: Download artifact from the previous workflow.
+        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
+        id: download-artifact
+        uses: dawidd6/action-download-artifact@v2 # https://github.com/marketplace/actions/download-workflow-artifact
+        with:
+          run_id: ${{ github.event.workflow_run.id }}
+          path: artifacts
+      - name: Prepare release
+        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
+        run: |
+          git remote add pr-releases https://foo:'${{ secrets.PR_RELEASES_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-pr-releases.git
+          # Try to delete any existing release for the current PR.
+          gh release delete --repo ${{ github.repository_owner }}/lean4-pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} -y || true
+          git tag -f pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}
+          git push -f pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}
+        env:
+          GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
+      - name: Release
+        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
+        uses: softprops/action-gh-release@v1
+        with:
+          name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }}
+          # There are coredumps files here as well, but all in deeper subdirectories.
+          files: artifacts/*/*
+          fail_on_unmatched_files: true
+          draft: false
+          tag_name: pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}
+          repository: ${{ github.repository_owner }}/lean4-pr-releases
+        env:
+          # The token used here must have `workflow` privileges.
+          GITHUB_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}