Skip to content

Add github actions ubuntu-20.04 make build #5449

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.

Sign up for GitHub

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 1 commit into from
Aug 18, 2020
Merged

Add github actions ubuntu-20.04 make build #5449

Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
36 changes: 36 additions & 0 deletions .github/workflows/pull-request-checks.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,42 @@ on:
branches: [ develop ]

jobs:
check-ubuntu-20_04-make-gcc:
runs-on: ubuntu-20.04
steps:
- uses: actions/checkout@v2
with:
submodules: true
- name: Fetch dependencies
env:
# This is needed in addition to -yq to prevent apt-get from asking for
# user input
DEBIAN_FRONTEND: noninteractive
TESTPL_JOBS: 4
run: |
sudo apt-get install -yq gcc gdb g++ maven jq flex bison libxml2-utils cpanminus
make -C src minisat2-download
Copy link
Contributor

Choose a reason for hiding this comment

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

I'd be more inclined to move this make invocation into the build section - it's part of the system-under-tests (i.e. the Makefiles) rather than general environment setup (the apt-get)

Copy link
Contributor

Choose a reason for hiding this comment

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

Yes, but afaik this doesn't really build minisat, does it? It only downloads the sources and applies a patch as far as I can recall?

Copy link
Contributor

Choose a reason for hiding this comment

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

All of which is defined in the Makefile, which is what is being tested here.

Copy link
Contributor

Choose a reason for hiding this comment

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

Yes, I recall correctly (https://github.com/diffblue/cbmc/blob/develop/src/Makefile#L120).

I would argue this is part of the configuration, as without minisat being downloaded, the build fails - but it's really because the sources are missing, not because of a compilation issue or anything else. And seeing as minisat is one of the SAT solvers we support, I would argue even more this is part of the configuration, even if it's just the default right now.

Copy link
Contributor

Choose a reason for hiding this comment

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

I don't have a massive issue with this - so I'm happy to approve if everyone else is happy. My logic was:

  1. Cmake does the minisat download as part of its configure/build steps, so my suggestion would be more consistent with that
  2. If the apt-get fails, or the cpanm fails, its mostly just a case of saying "shrug, infrastructure failed - hit retry", but if the minisat-download fails you do have to double check whether our own stuff needs to be modified. If you have the "setup our CI host" as a separate section to "run our own stuff" then it makes a clear distinction between stuff we may need to manage/modify and stuff that is just pure environment setup.

cpanm Thread::Pool::Simple
- name: Build with make
run: |
make -C src CXX='/usr/bin/g++' -j2
make -C unit CXX='/usr/bin/g++' -j2
make -C jbmc/src CXX='/usr/bin/g++' -j2
make -C jbmc/unit CXX='/usr/bin/g++' -j2
- name: Run unit tests
run: |
make -C unit test
Copy link
Contributor

Choose a reason for hiding this comment

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

I believe the unit tests, at least the jbmc ones, actually need to be run from the unit directory

Copy link
Contributor Author

Choose a reason for hiding this comment

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

The -C unit argument to make changes into the unit directory and changes back before exiting make. This is the same way as the make build is implemented in Travis right now.

make -C jbmc/unit test
echo "Running expected failure tests"
make TAGS="[!shouldfail]" -C unit test
make TAGS="[!shouldfail]" -C jbmc/unit test
- name: Run regression tests
run: |
make -C regression test
make -C regression/cbmc test-paths-lifo
env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
make -C jbmc/regression test

check-macos-10_15-make-clang:
runs-on: macos-10.15
steps:
Expand Down