From d4aa335685421f054143e0d8d7213ffec1a58e9c Mon Sep 17 00:00:00 2001 From: Joscha Date: Wed, 24 Jun 2026 14:37:10 +0200 Subject: [PATCH 1/7] chore: CI: set up adaptation PRs --- .github/workflows/adaptation-pr.yml | 74 +++++++++++++++++++++++++++++ 1 file changed, 74 insertions(+) create mode 100644 .github/workflows/adaptation-pr.yml diff --git a/.github/workflows/adaptation-pr.yml b/.github/workflows/adaptation-pr.yml new file mode 100644 index 000000000000..bade9d24a7db --- /dev/null +++ b/.github/workflows/adaptation-pr.yml @@ -0,0 +1,74 @@ +# One half of the adaptation PR CI; the other half lives in `pr-release.yml`. +name: Adaptation PR CI + +on: + pull_request: + types: [labeled] + branches: [master] + +jobs: + on-success: + runs-on: ubuntu-slim + if: 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: pr-info + 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}`; + + let green = false; + try { + await github.rest.repos.getReleaseByTag({ + owner: 'leanprover', + repo: 'lean4-pr-releases', + tag, + }); + green = true; + } catch (e) { + if (e.status !== 404) throw e; + } + + core.setOutput('override-toolchain', `leanprover/lean4-pr-releases:${tag}`); + core.setOutput('upstream-ci-green', green); + + - name: Create GitHub App token + uses: actions/create-github-app-token@v3 + id: app-token + with: + client-id: ${{ vars.DOWNSTREAM_APP_CLIENT_ID }} + private-key: ${{ secrets.DOWNSTREAM_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@v7 + 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.pr-info.outputs.upstream-ci-green }} + downstream-repo: leanprover/downstream-lean4 + downstream-clone: downstream + downstream-label: adaptation + override-toolchain: ${{ steps.pr-info.outputs.override-toolchain }} From b56addbc664aada17760c329b844000cce809ce7 Mon Sep 17 00:00:00 2001 From: Joscha Date: Wed, 24 Jun 2026 14:39:50 +0200 Subject: [PATCH 2/7] tweaks --- .github/workflows/adaptation-pr.yml | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/.github/workflows/adaptation-pr.yml b/.github/workflows/adaptation-pr.yml index bade9d24a7db..9c351cc17839 100644 --- a/.github/workflows/adaptation-pr.yml +++ b/.github/workflows/adaptation-pr.yml @@ -15,28 +15,32 @@ jobs: # produced) and whether the corresponding release already exists in # `leanprover/lean4-pr-releases`. - name: Check if PR toolchain exists - id: pr-info + 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 green = false; + let exists = false; try { await github.rest.repos.getReleaseByTag({ owner: 'leanprover', repo: 'lean4-pr-releases', tag, }); - green = true; + exists = true; } catch (e) { if (e.status !== 404) throw e; } - core.setOutput('override-toolchain', `leanprover/lean4-pr-releases:${tag}`); - core.setOutput('upstream-ci-green', green); + 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 @@ -67,8 +71,8 @@ jobs: 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.pr-info.outputs.upstream-ci-green }} + upstream-ci-green: ${{ steps.toolchain.outputs.exists }} downstream-repo: leanprover/downstream-lean4 downstream-clone: downstream downstream-label: adaptation - override-toolchain: ${{ steps.pr-info.outputs.override-toolchain }} + override-toolchain: ${{ steps.toolchain.outputs.toolchain }} From a661b65d6493f5977da846fe1796835922d88a29 Mon Sep 17 00:00:00 2001 From: Joscha Date: Wed, 24 Jun 2026 15:06:31 +0200 Subject: [PATCH 3/7] more tweaks --- .github/workflows/adaptation-pr.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/adaptation-pr.yml b/.github/workflows/adaptation-pr.yml index 9c351cc17839..32ea81a9fe99 100644 --- a/.github/workflows/adaptation-pr.yml +++ b/.github/workflows/adaptation-pr.yml @@ -2,12 +2,12 @@ name: Adaptation PR CI on: - pull_request: + pull_request_target: types: [labeled] branches: [master] jobs: - on-success: + main: runs-on: ubuntu-slim if: github.repository == 'leanprover/lean4' steps: From fd5a137fc94f408bd6d3e7ff806db1a50d680076 Mon Sep 17 00:00:00 2001 From: Joscha Date: Wed, 24 Jun 2026 15:14:56 +0200 Subject: [PATCH 4/7] run in pr-release as well --- .github/workflows/pr-release.yml | 43 ++++++++++++++++++++++++++++++++ 1 file changed, 43 insertions(+) diff --git a/.github/workflows/pr-release.yml b/.github/workflows/pr-release.yml index b9d37f237b08..1dceb5767d72 100644 --- a/.github/workflows/pr-release.yml +++ b/.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_APP_CLIENT_ID }} + private-key: ${{ secrets.DOWNSTREAM_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@v7 + 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 }} From 6bbc3ab5bb5b7194cd28dcd591d52d1aeb45047e Mon Sep 17 00:00:00 2001 From: Joscha Date: Wed, 24 Jun 2026 15:34:50 +0200 Subject: [PATCH 5/7] fix secret names --- .github/workflows/adaptation-pr.yml | 4 ++-- .github/workflows/pr-release.yml | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/workflows/adaptation-pr.yml b/.github/workflows/adaptation-pr.yml index 32ea81a9fe99..41fd07d56fb4 100644 --- a/.github/workflows/adaptation-pr.yml +++ b/.github/workflows/adaptation-pr.yml @@ -46,8 +46,8 @@ jobs: uses: actions/create-github-app-token@v3 id: app-token with: - client-id: ${{ vars.DOWNSTREAM_APP_CLIENT_ID }} - private-key: ${{ secrets.DOWNSTREAM_APP_PRIVATE_KEY }} + client-id: ${{ vars.DOWNSTREAM_LEAN4_APP_CLIENT_ID }} + private-key: ${{ secrets.DOWNSTREAM_LEAN4_APP_PRIVATE_KEY }} repositories: lean4,downstream-lean4 - name: Configure git diff --git a/.github/workflows/pr-release.yml b/.github/workflows/pr-release.yml index 1dceb5767d72..b246922c138e 100644 --- a/.github/workflows/pr-release.yml +++ b/.github/workflows/pr-release.yml @@ -632,8 +632,8 @@ jobs: uses: actions/create-github-app-token@v3 id: app-token with: - client-id: ${{ vars.DOWNSTREAM_APP_CLIENT_ID }} - private-key: ${{ secrets.DOWNSTREAM_APP_PRIVATE_KEY }} + client-id: ${{ vars.DOWNSTREAM_LEAN4_APP_CLIENT_ID }} + private-key: ${{ secrets.DOWNSTREAM_LEAN4_APP_PRIVATE_KEY }} repositories: lean4,downstream-lean4 - name: Configure git From 0831ff7faf664bbaf4555fce8bb92ef3cdb58234 Mon Sep 17 00:00:00 2001 From: Joscha Date: Wed, 24 Jun 2026 15:41:29 +0200 Subject: [PATCH 6/7] fix actionlint --- .github/actionlint.yaml | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/.github/actionlint.yaml b/.github/actionlint.yaml index c7539a4b51d0..63cc86e375d2 100644 --- a/.github/actionlint.yaml +++ b/.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" From d0d3d9c3abd9d3955ada7124f59ce99dd71abf8b Mon Sep 17 00:00:00 2001 From: Joscha Date: Wed, 24 Jun 2026 16:01:15 +0200 Subject: [PATCH 7/7] tweaks again --- .github/workflows/adaptation-pr.yml | 4 ++-- .github/workflows/pr-release.yml | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/adaptation-pr.yml b/.github/workflows/adaptation-pr.yml index 41fd07d56fb4..25840f4a500e 100644 --- a/.github/workflows/adaptation-pr.yml +++ b/.github/workflows/adaptation-pr.yml @@ -9,7 +9,7 @@ on: jobs: main: runs-on: ubuntu-slim - if: github.repository == 'leanprover/lean4' + 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 @@ -56,7 +56,7 @@ jobs: name: ${{ steps.app-token.outputs.app-slug }}[bot] - name: Checkout downstream repo - uses: actions/checkout@v7 + uses: actions/checkout@v6 with: repository: leanprover/downstream-lean4 ref: green diff --git a/.github/workflows/pr-release.yml b/.github/workflows/pr-release.yml index b246922c138e..62810640b178 100644 --- a/.github/workflows/pr-release.yml +++ b/.github/workflows/pr-release.yml @@ -644,7 +644,7 @@ jobs: - name: Checkout downstream repo if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} - uses: actions/checkout@v7 + uses: actions/checkout@v6 with: repository: leanprover/downstream-lean4 ref: green