From c4540f75b8340b1081fbbe261f767c1df593dc44 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Thu, 31 Aug 2023 13:24:41 +1000
Subject: [PATCH] chore: create a mathlib branch for each Lean PR (#2473)

* chore: create a mathlib branch for each Lean PR

* use existing branch if present
---
 .github/workflows/pr-release.yml | 39 ++++++++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)

diff --git a/.github/workflows/pr-release.yml b/.github/workflows/pr-release.yml
index d8ecf7195b..c20746b10d 100644
--- a/.github/workflows/pr-release.yml
+++ b/.github/workflows/pr-release.yml
@@ -69,3 +69,42 @@ jobs:
         env:
           # The token used here must have `workflow` privileges.
           GITHUB_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
+
+      # We next automatically create a Mathlib branch using this toolchain.
+      # Mathlib CI will be responsible for reporting back success or failure
+      # to the PR comments asynchronously.
+      - name: Cleanup workspace
+        run: |
+          sudo rm -rf *
+
+      # Checkout the mathlib4 repository with all branches
+      - name: Checkout mathlib4 repository
+        uses: actions/checkout@v2
+        with:
+          repository: leanprover-community/mathlib4
+          token: ${{ secrets.MATHLIB4_BOT }}
+          ref: master
+          fetch-depth: 0
+
+      - name: Check if branch exists
+        id: check_branch
+        run: |
+          EXISTS=$(git ls-remote --heads origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} | wc -l)
+          echo "Branch exists: $EXISTS"
+          if [ "$EXISTS" = "0" ]; then
+            echo "Branch does not exist, creating it."
+            git checkout -b lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
+            echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}" > lean-toolchain
+            git add lean-toolchain
+            git commit -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
+          else
+            echo "Branch already exists, pushing an empty commit."
+            git checkout lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
+            git commit --allow-empty -m "Trigger CI for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
+          fi
+
+      - name: Push changes
+        run: |
+          git config user.name "leanprover-community-mathlib4-bot"
+          git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com"
+          git push origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}