Skip to content

Commit 5d777d6

Browse files
authored
chore: add check only keyword action (#1327)
1 parent eeb3f51 commit 5d777d6

File tree

1 file changed

+40
-0
lines changed

1 file changed

+40
-0
lines changed
+40
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
# This workflow checks if you are checking in dafny code
2+
# with the keyword {:only}, it adds a message to the pull
3+
# request to remind you to remove it.
4+
name: Check {:only} decorator presence
5+
6+
on:
7+
pull_request:
8+
9+
jobs:
10+
grep-only-verification-keyword:
11+
runs-on: ubuntu-latest
12+
permissions:
13+
issues: write
14+
pull-requests: write
15+
steps:
16+
- uses: actions/checkout@v3
17+
with:
18+
fetch-depth: 0
19+
20+
- name: Check only keyword
21+
id: only-keyword
22+
shell: bash
23+
run:
24+
# checking in code with the dafny decorator {:only}
25+
# will not verify the entire file or maybe the entire project depending on its configuration
26+
# This action checks if you are either adding or removing the {:only} decorator and posting on the pr if you are.
27+
echo "ONLY_KEYWORD=$(git diff origin/main origin/${GITHUB_HEAD_REF} **/*.dfy | grep -i {:only})" >> "$GITHUB_OUTPUT"
28+
29+
- name: Check if ONLY_KEYWORD is not empty
30+
id: comment
31+
env:
32+
PR_NUMBER: ${{ github.event.number }}
33+
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
34+
ONLY_KEYWORD: ${{ steps.only-keyword.outputs.ONLY_KEYWORD }}
35+
if: ${{env.ONLY_KEYWORD != ''}}
36+
run: |
37+
COMMENT="It looks like you are adding or removing the dafny keyword {:only}.\nIs this intended?"
38+
COMMENT_URL="https://api.github.com/repos/${{ github.repository }}/issues/${PR_NUMBER}/comments"
39+
curl -s -H "Authorization: token ${GITHUB_TOKEN}" -X POST $COMMENT_URL -d "{\"body\":\"$COMMENT\"}"
40+
exit 1

0 commit comments

Comments
 (0)