File tree Expand file tree Collapse file tree 1 file changed +40
-0
lines changed Expand file tree Collapse file tree 1 file changed +40
-0
lines changed Original file line number Diff line number Diff line change 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
You can’t perform that action at this time.
0 commit comments