Skip to content

Commit c50c2ba

Browse files
GarmelonGarmelon
authored
chore: CI: set up adaptation PRs (#14169)
1 parent 2e00abb commit c50c2ba

3 files changed

Lines changed: 128 additions & 0 deletions

File tree

‎.github/actionlint.yaml‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,3 +3,10 @@ self-hosted-runner:
33
- nscloud-ubuntu-22.04-amd64-4x16
44
- nscloud-ubuntu-22.04-amd64-8x16
55
- nscloud-macos-sonoma-arm64-6x14
6+
7+
paths:
8+
".github/workflows/**/*.yml":
9+
ignore:
10+
# https://github.com/rhysd/actionlint/pull/652
11+
- missing input "app-id" which is required by action "actions/create-github-app-token@v3"
12+
- input "client-id" is not defined in action "actions/create-github-app-token@v3"

‎.github/workflows/adaptation-pr.yml‎

Lines changed: 78 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,78 @@
1+
# One half of the adaptation PR CI; the other half lives in `pr-release.yml`.
2+
name: Adaptation PR CI
3+
4+
on:
5+
pull_request_target:
6+
types: [labeled]
7+
branches: [master]
8+
9+
jobs:
10+
main:
11+
runs-on: ubuntu-slim
12+
if: github.event.label.name == 'downstream' && github.repository == 'leanprover/lean4'
13+
steps:
14+
# Determine the PR toolchain tag (see `pr-release.yml` for how it is
15+
# produced) and whether the corresponding release already exists in
16+
# `leanprover/lean4-pr-releases`.
17+
- name: Check if PR toolchain exists
18+
id: toolchain
19+
uses: actions/github-script@v9
20+
with:
21+
script: |
22+
const number = context.payload.pull_request.number;
23+
const shortSha = context.payload.pull_request.head.sha.substring(0, 7);
24+
const tag = `pr-release-${number}-${shortSha}`;
25+
const toolchain = `leanprover/lean4-pr-releases:${tag}`;
26+
27+
let exists = false;
28+
try {
29+
await github.rest.repos.getReleaseByTag({
30+
owner: 'leanprover',
31+
repo: 'lean4-pr-releases',
32+
tag,
33+
});
34+
exists = true;
35+
} catch (e) {
36+
if (e.status !== 404) throw e;
37+
}
38+
39+
if (exists) core.info(`Toolchain ${toolchain} exists`);
40+
else core.info(`Toolchain ${toolchain} does not exist yet`);
41+
42+
core.setOutput('toolchain', toolchain);
43+
core.setOutput('exists', exists);
44+
45+
- name: Create GitHub App token
46+
uses: actions/create-github-app-token@v3
47+
id: app-token
48+
with:
49+
client-id: ${{ vars.DOWNSTREAM_LEAN4_APP_CLIENT_ID }}
50+
private-key: ${{ secrets.DOWNSTREAM_LEAN4_APP_PRIVATE_KEY }}
51+
repositories: lean4,downstream-lean4
52+
53+
- name: Configure git
54+
uses: leanprover/downstream-lean4/.downstream/actions/configure-git@master
55+
with:
56+
name: ${{ steps.app-token.outputs.app-slug }}[bot]
57+
58+
- name: Checkout downstream repo
59+
uses: actions/checkout@v6
60+
with:
61+
repository: leanprover/downstream-lean4
62+
ref: green
63+
token: ${{ steps.app-token.outputs.token }}
64+
path: downstream
65+
filter: tree:0
66+
fetch-depth: 0
67+
68+
- name: Create adaptation PR
69+
uses: leanprover/downstream-lean4/.downstream/actions/adaptation-pr@master
70+
with:
71+
app-token: ${{ steps.app-token.outputs.token }}
72+
app-slug: ${{ steps.app-token.outputs.app-slug }}
73+
upstream-pr: ${{ github.event.pull_request.number }}
74+
upstream-ci-green: ${{ steps.toolchain.outputs.exists }}
75+
downstream-repo: leanprover/downstream-lean4
76+
downstream-clone: downstream
77+
downstream-label: adaptation
78+
override-toolchain: ${{ steps.toolchain.outputs.toolchain }}

‎.github/workflows/pr-release.yml‎

Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -621,3 +621,46 @@ jobs:
621621
if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.reference-manual-ready.outputs.manual_ready == 'true'
622622
run: |
623623
git push origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
624+
625+
# Finally, create/update the adaptation PR in the downstream repo. This is
626+
# the second entry point into the adaptation-pr action; the other lives in
627+
# `adaptation-pr.yml`. Unlike there, the toolchain release was just
628+
# created above, so it is known to exist and there is no need to look it
629+
# up first.
630+
- name: Create GitHub App token
631+
if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
632+
uses: actions/create-github-app-token@v3
633+
id: app-token
634+
with:
635+
client-id: ${{ vars.DOWNSTREAM_LEAN4_APP_CLIENT_ID }}
636+
private-key: ${{ secrets.DOWNSTREAM_LEAN4_APP_PRIVATE_KEY }}
637+
repositories: lean4,downstream-lean4
638+
639+
- name: Configure git
640+
if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
641+
uses: leanprover/downstream-lean4/.downstream/actions/configure-git@master
642+
with:
643+
name: ${{ steps.app-token.outputs.app-slug }}[bot]
644+
645+
- name: Checkout downstream repo
646+
if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
647+
uses: actions/checkout@v6
648+
with:
649+
repository: leanprover/downstream-lean4
650+
ref: green
651+
token: ${{ steps.app-token.outputs.token }}
652+
path: downstream
653+
filter: tree:0
654+
fetch-depth: 0
655+
656+
- name: Create adaptation PR
657+
if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
658+
uses: leanprover/downstream-lean4/.downstream/actions/adaptation-pr@master
659+
with:
660+
app-token: ${{ steps.app-token.outputs.token }}
661+
app-slug: ${{ steps.app-token.outputs.app-slug }}
662+
upstream-pr: ${{ steps.workflow-info.outputs.pullRequestNumber }}
663+
downstream-repo: leanprover/downstream-lean4
664+
downstream-clone: downstream
665+
downstream-label: adaptation
666+
override-toolchain: leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}

0 commit comments

Comments
 (0)