Skip to content

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

Merged
merged 4 commits into from
Aug 21, 2020
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
38 changes: 38 additions & 0 deletions .github/workflows/pull-request-check-clang-format.sh
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'

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?

Copy link
Contributor Author

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.

cat formatted.diff
exit 1
fi
echo 'No formatting errors found'
exit 0
24 changes: 24 additions & 0 deletions .github/workflows/pull-request-check-cpplint.sh
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"

Choose a reason for hiding this comment

The 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
47 changes: 47 additions & 0 deletions .github/workflows/pull-request-checks.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -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

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

To get this to work you’d want fetch_depth: 0 here to check out the entire repository rather than create a shallow clone (the default).

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