fix: use pull_request_target for label-triggered workflows

[kim-em]

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

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-02-22 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-22 13:04:59)
• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-02-28 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-01 07:40:11)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-02-22 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-02-22 13:05:00)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-02-28 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-03-01 07:40:12)

[nomeata]

PR body

Did you (or claude) double check if PR body is safely handled and no risk of injections here?

[kim-em]

Claude audited all four workflows for injection risk under pull_request_target and says:

pr-body.yml — reads context.payload.pull_request.body (attacker-controlled), but only passes it to regex.test(body) — a pure read-only string match in JavaScript. The body is never interpolated into shell commands, eval'd, written to GITHUB_ENV/GITHUB_OUTPUT, or used in API calls. Same for title. Failure messages are constant strings. The regexes are simple/linear (no ReDoS risk).

awaiting-mathlib.yml / awaiting-manual.yml — only read label names via exact-match comparisons. The only output is a constant 'true' string. No attacker-controlled data reaches any sink.

check-stdlib-flags.yml — reads the file list via API (pulls.listFiles) and does a strict equality check against 'src/stdlib_flags.h'. Labels are checked by exact name. No attacker-controlled data is echoed or interpolated.

None of the workflows check out PR code, use ${{ }} expression interpolation with untrusted data, or write attacker input to env/output files. The permissions: pull-requests: read block further limits GITHUB_TOKEN scope.

(Also confirmed by a separate Codex security audit.)

[nomeata]

Thanks for the extra checks

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-12638 has successfully built against this PR. (2026-02-27 03:44:22) View Log

[kim-em]

As this changes the trigger, the check-awaiting-mathlib and check-pr-body checks aren't running, so I will merge this one manually, bypassing the queue.

For pull_request events, GitHub uses the workflow definition from the PR branch. The PR branch's definition says "only trigger on pull_request_target", so the pull_request event is ignored. But pull_request_target events use the base branch's workflow definition, and the base branch still says pull_request, not pull_request_target. Neither version matches!