Add github actions ubuntu-20.04 make build #5449
Conversation
Codecov Report
@@ Coverage Diff @@
## develop #5449 +/- ##
========================================
Coverage 68.22% 68.22%
========================================
Files 1178 1178
Lines 97585 97585
========================================
Hits 66581 66581
Misses 31004 31004
Flags with carried forward coverage won't be shown. Click here to find out more. Continue to review full report at Codecov.
|
Codecov Report
@@ Coverage Diff @@
## develop #5449 +/- ##
============================================
+ Coverage 32.23% 68.25% +36.01%
============================================
Files 927 1180 +253
Lines 81237 97722 +16485
============================================
+ Hits 26187 66698 +40511
+ Misses 55050 31024 -24026
Flags with carried forward coverage won't be shown. Click here to find out more.
Continue to review full report at Codecov.
|
| make -C jbmc/unit CXX='/usr/bin/g++' -j2 | ||
| - name: Run unit tests | ||
| run: | | ||
| make -C unit test |
There was a problem hiding this comment.
I believe the unit tests, at least the jbmc ones, actually need to be run from the unit directory
There was a problem hiding this comment.
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.
thomasspriggs
force-pushed
the
tas/gha_ubuntu20_make
branch
3 times, most recently
from
5a49d8a to
a8ebed7
Compare
thomasspriggs
requested review from
chrisr-diffblue,
kroening,
peterschrammel,
smowton and
tautschnig
as code owners
|
So yeah, the |
thomasspriggs
force-pushed
the
tas/gha_ubuntu20_make
branch
from
a8ebed7 to
ad13e66
Compare
| TESTPL_JOBS: 4 | ||
| run: | | ||
| sudo apt-get install -yq gcc gdb g++ maven jq flex bison libxml2-utils cpanminus | ||
| make -C src minisat2-download |
There was a problem hiding this comment.
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)
There was a problem hiding this comment.
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?
There was a problem hiding this comment.
All of which is defined in the Makefile, which is what is being tested here.
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
I don't have a massive issue with this - so I'm happy to approve if everyone else is happy. My logic was:
- Cmake does the minisat download as part of its configure/build steps, so my suggestion would be more consistent with that
- 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.
So that we have testing of the make build on Ubuntu-20.04. Adding gdb installation is required for unit tests. Installation of `libxml2-utils` providing `xmllint` is so that the tests for valid XML output can run.
thomasspriggs
force-pushed
the
tas/gha_ubuntu20_make
branch
from
ad13e66 to
f58407f
Compare
So that we have testing of the make build on Ubuntu-20.04.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).My commit message includes data points confirming performance improvements (if claimed).White-space or formatting changes outside the feature-related changed lines are in commits of their own.