chore: CI: set up adaptation PRs

.github/actionlint.yaml

@@ -3,3 +3,10 @@ self-hosted-runner:
     - nscloud-ubuntu-22.04-amd64-4x16
     - nscloud-ubuntu-22.04-amd64-8x16
     - nscloud-macos-sonoma-arm64-6x14
+
+paths:
+  ".github/workflows/**/*.yml":
+    ignore:
+      # https://github.com/rhysd/actionlint/pull/652
+      - missing input "app-id" which is required by action "actions/create-github-app-token@v3"
+      - input "client-id" is not defined in action "actions/create-github-app-token@v3"

.github/workflows/adaptation-pr.yml

@@ -0,0 +1,78 @@
+# One half of the adaptation PR CI; the other half lives in `pr-release.yml`.
+name: Adaptation PR CI
+
+on:
+  pull_request_target:
+    types: [labeled]
+    branches: [master]
+
+jobs:
+  main:
+    runs-on: ubuntu-slim
+    if: github.event.label.name == 'downstream' && github.repository == 'leanprover/lean4'
+    steps:
+      # Determine the PR toolchain tag (see `pr-release.yml` for how it is
+      # produced) and whether the corresponding release already exists in
+      # `leanprover/lean4-pr-releases`.
+      - name: Check if PR toolchain exists
+        id: toolchain
+        uses: actions/github-script@v9
+        with:
+          script: |
+            const number = context.payload.pull_request.number;
+            const shortSha = context.payload.pull_request.head.sha.substring(0, 7);
+            const tag = `pr-release-${number}-${shortSha}`;
+            const toolchain = `leanprover/lean4-pr-releases:${tag}`;
+
+            let exists = false;
+            try {
+              await github.rest.repos.getReleaseByTag({
+                owner: 'leanprover',
+                repo: 'lean4-pr-releases',
+                tag,
+              });
+              exists = true;
+            } catch (e) {
+              if (e.status !== 404) throw e;
+            }
+
+            if (exists) core.info(`Toolchain ${toolchain} exists`);
+            else core.info(`Toolchain ${toolchain} does not exist yet`);
+
+            core.setOutput('toolchain', toolchain);
+            core.setOutput('exists', exists);
+
+      - name: Create GitHub App token
+        uses: actions/create-github-app-token@v3
+        id: app-token
+        with:
+          client-id: ${{ vars.DOWNSTREAM_LEAN4_APP_CLIENT_ID }}
+          private-key: ${{ secrets.DOWNSTREAM_LEAN4_APP_PRIVATE_KEY }}
+          repositories: lean4,downstream-lean4
+
+      - name: Configure git
+        uses: leanprover/downstream-lean4/.downstream/actions/configure-git@master
+        with:
+          name: ${{ steps.app-token.outputs.app-slug }}[bot]
+
+      - name: Checkout downstream repo
+        uses: actions/checkout@v6
+        with:
+          repository: leanprover/downstream-lean4
+          ref: green
+          token: ${{ steps.app-token.outputs.token }}
+          path: downstream
+          filter: tree:0
+          fetch-depth: 0
+
+      - name: Create adaptation PR
+        uses: leanprover/downstream-lean4/.downstream/actions/adaptation-pr@master
+        with:
+          app-token: ${{ steps.app-token.outputs.token }}
+          app-slug: ${{ steps.app-token.outputs.app-slug }}
+          upstream-pr: ${{ github.event.pull_request.number }}
+          upstream-ci-green: ${{ steps.toolchain.outputs.exists }}
+          downstream-repo: leanprover/downstream-lean4
+          downstream-clone: downstream
+          downstream-label: adaptation
+          override-toolchain: ${{ steps.toolchain.outputs.toolchain }}

.github/workflows/pr-release.yml

@@ -621,3 +621,46 @@ jobs:
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.reference-manual-ready.outputs.manual_ready == 'true'
         run: |
           git push origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
+
+      # Finally, create/update the adaptation PR in the downstream repo. This is
+      # the second entry point into the adaptation-pr action; the other lives in
+      # `adaptation-pr.yml`. Unlike there, the toolchain release was just
+      # created above, so it is known to exist and there is no need to look it
+      # up first.
+      - name: Create GitHub App token
+        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
+        uses: actions/create-github-app-token@v3
+        id: app-token
+        with:
+          client-id: ${{ vars.DOWNSTREAM_LEAN4_APP_CLIENT_ID }}
+          private-key: ${{ secrets.DOWNSTREAM_LEAN4_APP_PRIVATE_KEY }}
+          repositories: lean4,downstream-lean4
+
+      - name: Configure git
+        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
+        uses: leanprover/downstream-lean4/.downstream/actions/configure-git@master
+        with:
+          name: ${{ steps.app-token.outputs.app-slug }}[bot]
+
+      - name: Checkout downstream repo
+        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
+        uses: actions/checkout@v6
+        with:
+          repository: leanprover/downstream-lean4
+          ref: green
+          token: ${{ steps.app-token.outputs.token }}
+          path: downstream
+          filter: tree:0
+          fetch-depth: 0
+
+      - name: Create adaptation PR
+        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
+        uses: leanprover/downstream-lean4/.downstream/actions/adaptation-pr@master
+        with:
+          app-token: ${{ steps.app-token.outputs.token }}
+          app-slug: ${{ steps.app-token.outputs.app-slug }}
+          upstream-pr: ${{ steps.workflow-info.outputs.pullRequestNumber }}
+          downstream-repo: leanprover/downstream-lean4
+          downstream-clone: downstream
+          downstream-label: adaptation
+          override-toolchain: leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}