mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
fix: use pull_request_target for label-triggered workflows (#12638)
This PR switches four lightweight workflows from `pull_request` to `pull_request_target` to stop GitHub from requiring manual approval when the `mathlib-lean-pr-testing[bot]` app triggers label events (e.g. adding `builds-mathlib`). Since the bot never lands commits on master, it is perpetually treated as a "first-time contributor" and every `pull_request` event it triggers requires approval. `pull_request_target` events always run without approval because they execute trusted code from the base branch. This is safe for all four workflows because none check out or execute code from the PR branch — they only read labels, PR body, and file lists from the event payload and API: - `awaiting-mathlib.yml` — checks label combinations - `awaiting-manual.yml` — checks label combinations - `pr-body.yml` — checks PR body formatting - `check-stdlib-flags.yml` — checks if stdlib_flags.h was modified via API Also adds explicit `permissions: pull-requests: read` to each workflow as a least-privilege hardening measure, since `pull_request_target` has access to secrets. Addresses the issue reported by Sebastian: https://lean-fro.zulipchat.com/#narrow/channel/398861-general/topic/mathlib.20pr-testing.20breakage.3F/near/575084348 🤖 Prepared with Claude Code --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This commit is contained in:
9
.github/workflows/awaiting-manual.yml
vendored
9
.github/workflows/awaiting-manual.yml
vendored
@@ -2,16 +2,19 @@ name: Check awaiting-manual label
|
||||
|
||||
on:
|
||||
merge_group:
|
||||
pull_request:
|
||||
pull_request_target:
|
||||
types: [opened, synchronize, reopened, labeled, unlabeled]
|
||||
|
||||
permissions:
|
||||
pull-requests: read
|
||||
|
||||
jobs:
|
||||
check-awaiting-manual:
|
||||
runs-on: ubuntu-latest
|
||||
steps:
|
||||
- name: Check awaiting-manual label
|
||||
id: check-awaiting-manual-label
|
||||
if: github.event_name == 'pull_request'
|
||||
if: github.event_name == 'pull_request_target'
|
||||
uses: actions/github-script@v8
|
||||
with:
|
||||
script: |
|
||||
@@ -28,7 +31,7 @@ jobs:
|
||||
}
|
||||
|
||||
- name: Wait for manual compatibility
|
||||
if: github.event_name == 'pull_request' && steps.check-awaiting-manual-label.outputs.awaiting == 'true'
|
||||
if: github.event_name == 'pull_request_target' && steps.check-awaiting-manual-label.outputs.awaiting == 'true'
|
||||
run: |
|
||||
echo "::notice title=Awaiting manual::PR is marked 'awaiting-manual' but neither 'breaks-manual' nor 'builds-manual' labels are present."
|
||||
echo "This check will remain in progress until the PR is updated with appropriate manual compatibility labels."
|
||||
|
||||
9
.github/workflows/awaiting-mathlib.yml
vendored
9
.github/workflows/awaiting-mathlib.yml
vendored
@@ -2,16 +2,19 @@ name: Check awaiting-mathlib label
|
||||
|
||||
on:
|
||||
merge_group:
|
||||
pull_request:
|
||||
pull_request_target:
|
||||
types: [opened, synchronize, reopened, labeled, unlabeled]
|
||||
|
||||
permissions:
|
||||
pull-requests: read
|
||||
|
||||
jobs:
|
||||
check-awaiting-mathlib:
|
||||
runs-on: ubuntu-latest
|
||||
steps:
|
||||
- name: Check awaiting-mathlib label
|
||||
id: check-awaiting-mathlib-label
|
||||
if: github.event_name == 'pull_request'
|
||||
if: github.event_name == 'pull_request_target'
|
||||
uses: actions/github-script@v8
|
||||
with:
|
||||
script: |
|
||||
@@ -28,7 +31,7 @@ jobs:
|
||||
}
|
||||
|
||||
- name: Wait for mathlib compatibility
|
||||
if: github.event_name == 'pull_request' && steps.check-awaiting-mathlib-label.outputs.awaiting == 'true'
|
||||
if: github.event_name == 'pull_request_target' && steps.check-awaiting-mathlib-label.outputs.awaiting == 'true'
|
||||
run: |
|
||||
echo "::notice title=Awaiting mathlib::PR is marked 'awaiting-mathlib' but neither 'breaks-mathlib' nor 'builds-mathlib' labels are present."
|
||||
echo "This check will remain in progress until the PR is updated with appropriate mathlib compatibility labels."
|
||||
|
||||
5
.github/workflows/check-stdlib-flags.yml
vendored
5
.github/workflows/check-stdlib-flags.yml
vendored
@@ -1,9 +1,12 @@
|
||||
name: Check stdlib_flags.h modifications
|
||||
|
||||
on:
|
||||
pull_request:
|
||||
pull_request_target:
|
||||
types: [opened, synchronize, reopened, labeled, unlabeled]
|
||||
|
||||
permissions:
|
||||
pull-requests: read
|
||||
|
||||
jobs:
|
||||
check-stdlib-flags:
|
||||
runs-on: ubuntu-latest
|
||||
|
||||
10
.github/workflows/pr-body.yml
vendored
10
.github/workflows/pr-body.yml
vendored
@@ -2,17 +2,23 @@ name: Check PR body for changelog convention
|
||||
|
||||
on:
|
||||
merge_group:
|
||||
pull_request:
|
||||
pull_request_target:
|
||||
types: [opened, synchronize, reopened, edited, labeled, converted_to_draft, ready_for_review]
|
||||
|
||||
permissions:
|
||||
pull-requests: read
|
||||
|
||||
jobs:
|
||||
check-pr-body:
|
||||
runs-on: ubuntu-latest
|
||||
steps:
|
||||
- name: Check PR body
|
||||
if: github.event_name == 'pull_request'
|
||||
if: github.event_name == 'pull_request_target'
|
||||
uses: actions/github-script@v8
|
||||
with:
|
||||
# Safety note: this uses pull_request_target, so the workflow has elevated privileges.
|
||||
# The PR title and body are only used in regex tests (read-only string matching),
|
||||
# never interpolated into shell commands, eval'd, or written to GITHUB_ENV/GITHUB_OUTPUT.
|
||||
script: |
|
||||
const { title, body, labels, draft } = context.payload.pull_request;
|
||||
if (!draft && /^(feat|fix):/.test(title) && !labels.some(label => label.name == "changelog-no")) {
|
||||
|
||||
Reference in New Issue
Block a user