-
Notifications
You must be signed in to change notification settings - Fork 273
Port ancillary jobs from Travis to github actions #5457
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Changes from all commits
9b9c48f
7c3a076
5379a73
f34e22a
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,38 @@ | ||
#!/bin/bash | ||
|
||
# Stop on errors | ||
set -e | ||
|
||
# Log information about the run of this check. | ||
echo "Pull request's base branch is: ${BASE_BRANCH}" | ||
echo "Pull request's merge branch is: ${MERGE_BRANCH}" | ||
echo "Pull request's source branch is: ${GITHUB_HEAD_REF}" | ||
clang-format-7 --version | ||
|
||
# The checkout action leaves us in detatched head state. The following line | ||
# names the checked out commit, for simpler reference later. | ||
git checkout -b ${MERGE_BRANCH} | ||
|
||
# Build list of files to ignore | ||
while read file ; do EXCLUDES+="':(top,exclude)$file' " ; done < .clang-format-ignore | ||
|
||
# Make sure we can refer to ${BASE_BRANCH} by name | ||
git checkout ${BASE_BRANCH} | ||
git checkout ${MERGE_BRANCH} | ||
|
||
# Find the commit on which the PR is based. | ||
MERGE_BASE=$(git merge-base ${BASE_BRANCH} ${MERGE_BRANCH}) | ||
echo "Checking for formatting errors introduced since $MERGE_BASE" | ||
|
||
# Do the checking. "eval" is used so that quotes (as inserted into $EXCLUDES | ||
# above) are not interpreted as parts of file names. | ||
eval git-clang-format-7 --binary clang-format-7 $MERGE_BASE -- $EXCLUDES | ||
git diff > formatted.diff | ||
if [[ -s formatted.diff ]] ; then | ||
echo 'Formatting error! The following diff shows the required changes' | ||
echo 'Use the raw log to get a version of the diff that preserves spacing' | ||
cat formatted.diff | ||
exit 1 | ||
fi | ||
echo 'No formatting errors found' | ||
exit 0 |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,24 @@ | ||
#!/bin/bash | ||
|
||
# Stop on errors | ||
set -e | ||
|
||
# Log information about the run of this check. | ||
echo "Pull request's base branch is: ${BASE_BRANCH}" | ||
echo "Pull request's merge branch is: ${MERGE_BRANCH}" | ||
echo "Pull request's source branch is: ${GITHUB_HEAD_REF}" | ||
|
||
# The checkout action leaves us in detatched head state. The following line | ||
# names the checked out commit, for simpler reference later. | ||
git checkout -b ${MERGE_BRANCH} | ||
|
||
# Make sure we can refer to ${BASE_BRANCH} by name | ||
git checkout ${BASE_BRANCH} | ||
git checkout ${MERGE_BRANCH} | ||
|
||
# Find the commit on which the PR is based. | ||
MERGE_BASE=$(git merge-base ${BASE_BRANCH} ${MERGE_BRANCH}) | ||
echo "Checking standards of code touched since $MERGE_BASE" | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Something which would be really cool is if we could use https://github.com/marketplace/actions/annotations-action to display inline comments with the needed changes (not an action for this PR, just food for thought for follow-up work). |
||
|
||
# Do the checking. | ||
./scripts/run_diff.sh CPPLINT $MERGE_BASE |
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -124,3 +124,50 @@ jobs: | |
|
||
- name: Build cbmc | ||
run: "%SCRIPT_DIR%\\build-cbmc.bat" | ||
|
||
check-clang-format: | ||
runs-on: ubuntu-20.04 | ||
steps: | ||
- uses: actions/checkout@v2 | ||
with: | ||
submodules: true | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. To get this to work you’d want |
||
fetch-depth: 0 | ||
- name: Fetch dependencies | ||
env: | ||
# This is needed in addition to -yq to prevent apt-get from asking for | ||
# user input | ||
DEBIAN_FRONTEND: noninteractive | ||
run: | | ||
sudo apt-get install -yq clang-format-7 | ||
- name: Check updated lines of code match clang-format-7 style | ||
env: | ||
BASE_BRANCH: ${{ github.base_ref }} | ||
MERGE_BRANCH: ${{ github.ref }} | ||
run: ./.github/workflows/pull-request-check-clang-format.sh | ||
|
||
check-cpplint: | ||
runs-on: ubuntu-20.04 | ||
steps: | ||
- uses: actions/checkout@v2 | ||
with: | ||
submodules: true | ||
fetch-depth: 0 | ||
- name: Fetch dependencies | ||
env: | ||
# This is needed in addition to -yq to prevent apt-get from asking for | ||
# user input | ||
DEBIAN_FRONTEND: noninteractive | ||
run: | | ||
pip install unidiff | ||
- name: Check updated lines of code meet linting standards | ||
env: | ||
BASE_BRANCH: ${{ github.base_ref }} | ||
MERGE_BRANCH: ${{ github.ref }} | ||
run: ./.github/workflows/pull-request-check-cpplint.sh | ||
|
||
check-string-table: | ||
runs-on: ubuntu-20.04 | ||
steps: | ||
- uses: actions/checkout@v2 | ||
- name: Check for unused irep ids | ||
run: ./scripts/string_table_check.sh |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is this referring to how the github action log presents this?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This was just cut and paste from the Travis version. I am not sure if viewing in github actions preserves spacing or not.