Skip to content

Commit 1ede81f

Browse files
committed
ci: Use reusable workflow instead of bash-generated yamls (leanprover-community#34590)
- Replace bash‑generated CI workflows with a [reusable workflow](https://docs.github.com/en/actions/how-tos/reuse-automations/reuse-workflows) template (build_template.yml) and thin callers (build.yml, bors.yml, build_fork.yml). - Remove generator script and its actionlint check; update dependabot scope accordingly. - Move caller‑specific if conditions to the top‑level jobs
1 parent 0f2ba92 commit 1ede81f

8 files changed

Lines changed: 61 additions & 2499 deletions

File tree

.github/dependabot.yml

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,13 @@ version: 2 # Specifies the version of the Dependabot configuration file format
33
updates:
44
# Configuration for dependency updates
55
- package-ecosystem: "github-actions" # Specifies the ecosystem to check for updates
6-
directories:
7-
- "/.github/*" # covers `build.in.yml` as well, which is not in `.github/workflows/` because it shouldn't be run in CI.
6+
directories:
7+
- "/.github/workflows"
88
schedule:
99
# Check for updates to GitHub Actions every month
1010
interval: "monthly"
1111
groups:
12-
# group updates into single PRs since we want to update both build.in.yml and its outputs at the same time
12+
# group updates into single PRs
1313
actions-version-updates:
1414
applies-to: version-updates
1515
patterns:

.github/workflows/actionlint.yml

Lines changed: 0 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -17,20 +17,3 @@ jobs:
1717
with:
1818
tool_name: actionlint
1919
fail_level: error
20-
21-
check_build_yml:
22-
name: check workflows generated by build.in.yml
23-
runs-on: ubuntu-latest
24-
steps:
25-
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
26-
27-
- name: update workflows
28-
run: |
29-
cd .github/workflows/
30-
./mk_build_yml.sh
31-
32-
- name: suggester / build.in.yml
33-
uses: reviewdog/action-suggester@aa38384ceb608d00f84b4690cacc83a5aba307ff # v1.24.0
34-
with:
35-
tool_name: mk_build_yml.sh
36-
fail_level: error

.github/workflows/bors.yml

Lines changed: 10 additions & 786 deletions
Large diffs are not rendered by default.

.github/workflows/build.yml

Lines changed: 10 additions & 785 deletions
Large diffs are not rendered by default.

.github/workflows/build_fork.yml

Lines changed: 10 additions & 785 deletions
Large diffs are not rendered by default.
Lines changed: 27 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,21 @@
1-
### NB: This is the master file for autogenerating
2-
### NB: `.github/workflows/{bors, build_fork, build}.yml`.
3-
### NB: If you need to edit any of those files, you should edit this file instead,
4-
### NB: and regenerate those files by manually running
5-
### NB: .github/workflows/mk_build_yml.sh
1+
# Reusable workflow invoked by build.yml, bors.yml, and build_fork.yml.
2+
3+
on:
4+
workflow_call:
5+
inputs:
6+
concurrency_group:
7+
type: string
8+
required: true
9+
pr_branch_ref:
10+
type: string
11+
required: true
12+
job_name_suffix:
13+
type: string
14+
required: false
15+
default: ""
16+
runs_on:
17+
type: string
18+
required: true
619

720
env:
821
# Disable Lake's automatic fetching of cloud builds.
@@ -12,24 +25,10 @@ env:
1225
# not necessarily satisfy this property.
1326
LAKE_NO_CACHE: true
1427

15-
concurrency:
16-
# label each workflow run; only the latest with each label will run
17-
# workflows on master get more expressive labels
18-
group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}-${{ (github.event_name == 'push' && contains(fromJSON('["refs/heads/master", "refs/heads/staging"]'), github.ref) && github.run_id) || '' }}
19-
# cancel any running workflow with the same label
20-
cancel-in-progress: true
21-
22-
# Limit permissions for GITHUB_TOKEN for the entire workflow
23-
permissions:
24-
contents: read
25-
pull-requests: write # Only allow PR comments/labels
26-
# All other permissions are implicitly 'none'
27-
2828
jobs:
2929
build:
30-
if: FORK_CONDITION
31-
name: BuildJOB_NAME
32-
runs-on: RUNS_ON
30+
name: Build${{ inputs.job_name_suffix }}
31+
runs-on: ${{ inputs.runs_on }}
3332
outputs:
3433
build-outcome: ${{ steps.build.outcome }}
3534
archive-outcome: ${{ steps.archive.outcome }}
@@ -51,7 +50,7 @@ jobs:
5150
REF: ${{ github.ref }}
5251
EVENT_NAME: ${{ github.event_name }}
5352
RUN_ID: ${{ github.run_id }}
54-
CONCURRENCY_GROUP: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}-${{ (github.event_name == 'push' && contains(fromJSON('["refs/heads/master", "refs/heads/staging"]'), github.ref) && github.run_id) || '' }}
53+
CONCURRENCY_GROUP: ${{ inputs.concurrency_group }}
5554
shell: bash # there is no script body, so this is safe to "run" outside landrun.
5655
run: |
5756
# We just populate the env vars for this step to make them viewable in the logs
@@ -90,7 +89,7 @@ jobs:
9089
- name: Checkout PR branch
9190
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
9291
with:
93-
ref: "${{ PR_BRANCH_REF }}"
92+
ref: ${{ inputs.pr_branch_ref }}
9493
path: pr-branch
9594

9695
- name: Prepare DownstreamTest directory
@@ -591,15 +590,14 @@ jobs:
591590
master-branch/scripts/lean-pr-testing-comments.sh batteries
592591
593592
post_steps:
594-
name: Post-Build StepJOB_NAME
595-
if: FORK_CONDITION
593+
name: Post-Build Step${{ inputs.job_name_suffix }}
596594
needs: [build]
597595
runs-on: ubuntu-latest # Note these steps run on disposable GitHub runners, so no landrun sandboxing is needed.
598596
steps:
599597

600598
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
601599
with:
602-
ref: "${{ PR_BRANCH_REF }}"
600+
ref: ${{ inputs.pr_branch_ref }}
603601

604602
- name: Configure Lean
605603
uses: leanprover/lean-action@c544e89643240c6b398f14a431bcdc6309e36b3e # v1.4.0
@@ -671,19 +669,17 @@ jobs:
671669
# We no longer run `lean4checker` in regular CI, as it is quite expensive for little benefit.
672670
# Instead we run it in a cron job on master: see `daily.yml`.
673671
style_lint:
674-
name: Lint styleJOB_NAME
675-
if: FORK_CONDITION
672+
name: Lint style${{ inputs.job_name_suffix }}
676673
runs-on: ubuntu-latest
677674
steps:
678675
- uses: leanprover-community/lint-style-action@a7e7428fa44f9635d6eb8e01919d16fd498d387a # 2025-08-18
679676
with:
680677
mode: check
681678
lint-bib-file: true
682-
ref: ${{ PR_BRANCH_REF }}
679+
ref: ${{ inputs.pr_branch_ref }}
683680

684681
final:
685-
name: Post-CI jobJOB_NAME
686-
if: FORK_CONDITION
682+
name: Post-CI job${{ inputs.job_name_suffix }}
687683
needs: [style_lint, build, post_steps]
688684
runs-on: ubuntu-latest
689685
steps:

.github/workflows/mk_build_yml.sh

Lines changed: 0 additions & 91 deletions
This file was deleted.

bors.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
status = ["Build", "Lint style", "Post-Build Step"]
1+
status = ["build / Build", "build / Lint style", "build / Post-Build Step"]
22
use_squash_merge = true
33
timeout_sec = 7200
44
block_labels = ["WIP", "blocked-by-other-PR", "merge-conflict", "awaiting-CI"]

0 commit comments

Comments
 (0)