ci: allow scripts/challenge/pins.env as version-bump metadata

[Vilin97]

Summary

• Adds scripts/challenge/pins.env to the content-PR guard's version-bump metadata allowlist (regex, header comment, and error-message listing).
• Rationale: LEAN4EXPORT_COMMIT in pins.env must match lean-toolchain — lean4export reads the oleans our build produces — so a toolchain bump has to move it in the same PR, exactly like the toolchain and manifest files already exempted.
• Unblocks chore: bump Lean and Mathlib to v4.33.0-rc1 #295, whose only guard failure is this file.

Test plan

• Ran the new bump_metadata_re against chore: bump Lean and Mathlib to v4.33.0-rc1 #295's full non-content file list: all seven bump files pass; an arbitrary neighbor (scripts/challenge/verify-solution.sh) is still rejected.

🤖 Generated with Claude Code

[greptile-apps]

Greptile Summary

This PR extends the content-pr-guard.yml CI gate to allow scripts/challenge/pins.env alongside content files during Lean/Mathlib toolchain bump PRs. The motivation is correct: LEAN4EXPORT_COMMIT in pins.env must be kept in sync with lean-toolchain because lean4export reads the oleans produced by the current toolchain, so a toolchain bump unavoidably requires updating both in the same PR.

• The bump_metadata_re regex is updated to include scripts/challenge/pins\.env, properly escaped and anchored within the existing alternation group.
• The workflow's header comment and the human-readable error-message listing are both updated to document the new exemption, keeping all three representations in sync.

Confidence Score: 5/5

Safe to merge — all three locations (regex, header comment, error message) are updated consistently, and the rationale for the exemption is technically sound.

The change is a one-line regex addition with two accompanying documentation updates. The regex scripts/challenge/pins\.env is correctly escaped and sits properly within the anchored alternation group. The rationale — that LEAN4EXPORT_COMMIT must move in lockstep with lean-toolchain because lean4export reads the oleans the current toolchain produced — is clearly explained in pins.env itself and in the new header comment. All three representations of the allowlist (regex, header comment, error output) are in sync after this change.

Files Needing Attention: No files require special attention.

Important Files Changed

Filename	Overview
.github/workflows/content-pr-guard.yml	Adds scripts/challenge/pins.env to the bump-metadata allowlist in three consistent places: the header comment, the bump_metadata_re regex (correctly escaped and anchored), and the human-readable error message. No other logic is altered.

Flowchart

%%{init: {'theme': 'neutral'}}%%
flowchart TD
    A[PR files] --> B{Any content files?}
    B -- No --> Z1[✓ Non-content-only PR]
    B -- Yes --> C{Any non-content files?}
    C -- No --> Z2[✓ Content-only PR]
    C -- Yes --> D{All non-content files\nmatch bump_metadata_re?}
    D -- Yes --> Z3[✓ Version-bump PR allowed]
    D -- No --> Z4[✗ FAIL: mixed content\nand non-content]

    style Z3 fill:#2d8a4e,color:#fff
    style Z1 fill:#2d8a4e,color:#fff
    style Z2 fill:#2d8a4e,color:#fff
    style Z4 fill:#c0392b,color:#fff

    subgraph bump_metadata_re [bump_metadata_re allowlist]
        M1[lean-toolchain]
        M2[lakefile.toml]
        M3[lake-manifest.json]
        M4[docbuild/lean-toolchain / docbuild/lakefile.toml / docbuild/lake-manifest.json]
        M5[scripts/challenge/pins.env NEW]
        M6[.github/workflows/content-pr-guard.yml]
    end

    D -- checked against --> bump_metadata_re

Loading

_{Reviews (1): Last reviewed commit: "ci: allow scripts/challenge/pins.env as ..." | Re-trigger Greptile}