Repository navigation
Enable queue validation and independent project metadata #6129
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: PR Separation Guard | |
| # Pooled Lean content and repository infrastructure must be reviewed separately. | |
| # Lean/Mathlib version bumps may also include their Lake/toolchain metadata. | |
| on: | |
| merge_group: | |
| types: [checks_requested] | |
| pull_request: | |
| types: [opened, synchronize, reopened] | |
| workflow_dispatch: | |
| inputs: | |
| pr_number: | |
| description: "PR number to guard (re-triggers the gate without a push)" | |
| required: true | |
| type: string | |
| permissions: | |
| contents: read | |
| pull-requests: read | |
| concurrency: | |
| # On a workflow_dispatch the pull_request context is empty, so fall back to | |
| # the input PR number; otherwise group by the live PR number as before. | |
| group: >- | |
| content-pr-guard-${{ github.event.pull_request.number || | |
| inputs.pr_number || github.ref }} | |
| cancel-in-progress: true | |
| jobs: | |
| guard: | |
| runs-on: ubuntu-latest | |
| name: Content / non-content separation | |
| steps: | |
| - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd | |
| with: | |
| fetch-depth: 0 | |
| persist-credentials: false | |
| - name: Check every PR in the combined queue commit | |
| if: github.event_name == 'merge_group' | |
| env: | |
| BASE_SHA: ${{ github.event.merge_group.base_sha }} | |
| HEAD_SHA: ${{ github.event.merge_group.head_sha }} | |
| run: >- | |
| PYTHONPATH=python python3 -m lean_pool.queue_guard | |
| --base "$BASE_SHA" --head "$HEAD_SHA" | |
| - name: Reject mixed content and non-content changes | |
| if: github.event_name != 'merge_group' | |
| env: | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| REPO: ${{ github.repository }} | |
| PR_NUMBER: ${{ github.event.pull_request.number || inputs.pr_number }} | |
| run: | | |
| set -euo pipefail | |
| files="$(gh api "repos/$REPO/pulls/$PR_NUMBER/files" --paginate --jq '.[].filename')" | |
| echo "Files changed in this PR:" | |
| printf '%s\n' "$files" | sed 's/^/ /' | |
| echo | |
| base=$(gh api "repos/$REPO/pulls/$PR_NUMBER" --jq '.base.sha') | |
| content_re='^(LeanPool\.lean|LeanPool/.+\.lean|LeanPool/projects\.yml|LeanPool/projects/[A-Za-z0-9_-]+\.yaml)$' | |
| if ! git cat-file -e "$base:LeanPool/projects.yml" 2>/dev/null \ | |
| && printf '%s\n' "$files" | grep -qx 'LeanPool.lean'; then | |
| echo '::error::LeanPool.lean is fixed; PRs must not edit the shared root.' | |
| exit 1 | |
| fi | |
| content="$(printf '%s\n' "$files" | { grep -E "$content_re" || true; })" | |
| non_content="$(printf '%s\n' "$files" | { grep -vE "$content_re" || true; })" | |
| if [ -n "$content" ] && [ -n "$non_content" ]; then | |
| bump_metadata_re='^(lean-toolchain|lakefile\.toml|lake-manifest\.json|docbuild/(lean-toolchain|lakefile\.toml|lake-manifest\.json)|\.github/workflows/content-pr-guard\.yml)$' | |
| non_bump_metadata="$(printf '%s\n' "$non_content" | { grep -vE "$bump_metadata_re" || true; })" | |
| bump_metadata="$(printf '%s\n' "$non_content" | { grep -E "$bump_metadata_re" || true; })" | |
| if [ -n "$bump_metadata" ] && [ -z "$non_bump_metadata" ]; then | |
| echo "✓ Content plus Lean/lake version-bump metadata." | |
| echo "Allowed bump metadata files:" | |
| while IFS= read -r f; do | |
| [ -n "$f" ] || continue | |
| echo " - $f" | |
| done <<< "$bump_metadata" | |
| exit 0 | |
| fi | |
| echo "::error::This PR mixes content and non-content changes." | |
| echo "Content files may be changed only in content-only PRs:" | |
| echo " - LeanPool/**/*.lean" | |
| echo " - LeanPool/projects/*.yaml" | |
| echo "(Exception: a version bump may also touch lean-toolchain," | |
| echo " lake-manifest.json, and lakefile.toml.)" | |
| echo | |
| echo "Lean/lake bump PRs may additionally change only:" | |
| echo " - lean-toolchain" | |
| echo " - lakefile.toml" | |
| echo " - lake-manifest.json" | |
| echo " - docbuild/lean-toolchain" | |
| echo " - docbuild/lakefile.toml" | |
| echo " - docbuild/lake-manifest.json" | |
| echo | |
| echo "Content files in this PR:" | |
| while IFS= read -r f; do | |
| [ -n "$f" ] || continue | |
| echo " - $f" | |
| done <<< "$content" | |
| echo | |
| echo "Non-content files in this PR:" | |
| while IFS= read -r f; do | |
| [ -n "$f" ] || continue | |
| echo " - $f" | |
| echo "::error file=$f::mixed with LeanPool content; split content and non-content changes into separate PRs" | |
| done <<< "$non_bump_metadata" | |
| exit 1 | |
| fi | |
| if [ -n "$content" ] && [ -n "$non_content" ]; then | |
| echo "✓ Version-bump PR: content alongside toolchain/manifest only." | |
| elif [ -n "$content" ]; then | |
| echo "✓ Content-only PR." | |
| else | |
| echo "✓ Non-content-only PR." | |
| fi |