forked from leanprover-community/mathlib4
-
Notifications
You must be signed in to change notification settings - Fork 0
117 lines (99 loc) · 4.08 KB
/
commit_verification.yml
File metadata and controls
117 lines (99 loc) · 4.08 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
# Commit Verification CI
# Verifies transient and automated commits in PRs
#
# - Transient commits (prefix: "transient: ") must have zero net effect
# - Automated commits (prefix: "x: <command>") must match command output
# - Posts a summary comment categorizing commits for reviewers
name: Commit Verification
on:
pull_request:
types: [opened, synchronize, reopened]
# Cancel in-progress runs for the same PR
concurrency:
group: commit-verification-${{ github.event.pull_request.number }}
cancel-in-progress: true
permissions:
contents: read
pull-requests: write
env:
TRANSIENT_PREFIX: "transient: "
# Support both "x " and "x: " (legacy) prefixes
AUTO_PREFIX_COLON: "x: "
AUTO_PREFIX_SPACE: "x "
jobs:
verify:
name: Verify Transient and Automated Commits
runs-on: ubuntu-latest
# Only run if there are commits with special prefixes
# This is a quick check to avoid unnecessary runs
steps:
- name: Checkout PR head
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
with:
# Checkout the actual PR head, not the merge commit GitHub creates
ref: ${{ github.event.pull_request.head.sha }}
# Fetch full history to access all PR commits
fetch-depth: 0
- name: Check for special commits
id: check
run: |
BASE_SHA="${{ github.event.pull_request.base.sha }}"
HEAD_SHA="${{ github.event.pull_request.head.sha }}"
# Check if any commits have transient or auto prefix
# Auto prefix can be "x " or "x: " (legacy)
HAS_SPECIAL=$(git log --format="%s" "$BASE_SHA..$HEAD_SHA" | \
grep -E "^(${TRANSIENT_PREFIX}|${AUTO_PREFIX_COLON}|${AUTO_PREFIX_SPACE})" || true)
if [[ -n "$HAS_SPECIAL" ]]; then
echo "has_special=true" >> "$GITHUB_OUTPUT"
echo "Found commits requiring verification:"
echo "$HAS_SPECIAL"
else
echo "has_special=false" >> "$GITHUB_OUTPUT"
echo "No transient or automated commits found"
fi
- name: Verify commits
id: verify
if: steps.check.outputs.has_special == 'true'
run: |
BASE_SHA="${{ github.event.pull_request.base.sha }}"
# Run verification (human-readable to stdout, JSON to file)
set +e
./scripts/verify_commits.sh "$BASE_SHA" --json-file verification_result.json
EXIT_CODE=$?
set -e
# Set outputs
if [[ $EXIT_CODE -eq 0 ]]; then
echo "success=true" >> "$GITHUB_OUTPUT"
else
echo "success=false" >> "$GITHUB_OUTPUT"
fi
- name: Generate PR comment
if: steps.check.outputs.has_special == 'true'
id: comment
run: |
REPO="${{ github.repository }}"
PR_NUMBER="${{ github.event.pull_request.number }}"
COMMENT=$(cat verification_result.json | ./scripts/verify_commits_summary.sh "$REPO" "$PR_NUMBER")
# Save to file (GitHub Actions has issues with multiline outputs)
echo "$COMMENT" > comment_body.md
- name: Find existing comment
if: steps.check.outputs.has_special == 'true'
uses: peter-evans/find-comment@b30e6a3c0ed37e7c023ccd3f1db5c6c0b0c23aad # v4
id: find-comment
with:
issue-number: ${{ github.event.pull_request.number }}
comment-author: 'github-actions[bot]'
body-includes: 'Commit Verification Summary'
- name: Post or update comment
if: steps.check.outputs.has_special == 'true'
uses: peter-evans/create-or-update-comment@e8674b075228eee787fea43ef493e45ece1004c9 # v4
with:
comment-id: ${{ steps.find-comment.outputs.comment-id }}
issue-number: ${{ github.event.pull_request.number }}
body-path: comment_body.md
edit-mode: replace
- name: Set job status
if: steps.check.outputs.has_special == 'true' && steps.verify.outputs.success == 'false'
run: |
echo "::error::Commit verification failed. See PR comment for details."
exit 1