Updates to compiling instructions for GCC 6 #682
Conversation
jgwilson42
changed the title
| On Red Hat/Fedora or derivates, do | ||
|
|
||
| yum install gcc gcc-c++ flex bison perl-libwww-perl patch | ||
| yum install gcc gcc-c++ flex bison perl-libwww-perl patch devtoolset-6 |
There was a problem hiding this comment.
I think that when you use devtoolset-6 you can remove some of dependencies. YUM should be fine with
yum install flex bison perl-libwww-perl patch devtoolset-6There was a problem hiding this comment.
Removing gcc and gcc-c++ makes the regression tests fail without the devtoolset-6 enabled. I cannot immediately see if this is a problem with the tests or with the cbmc binary. @kroening please let me know if you would like me to investigate further or you are happy with the instructions as is.
| cd cbmc-git/src | ||
| make minisat2-download | ||
| make CXX=g++-6 | ||
| scl enable devtoolset-6 bash |
There was a problem hiding this comment.
and then you probably need to run this before first make
There was a problem hiding this comment.
agreed this is required, if the above requested change is made.
There was a problem hiding this comment.
Yes, let's go for the "scl enable devtoolset-6 bash" change; it's better that the regressions work out-of-the box
There was a problem hiding this comment.
In which case I am happy with the state of this PR. The version here will ensure that the regression tests run under most scenarios.
Please let me know if you need anything else.
3 participants
The current instructions don't work for compiling on RedHat and need a small tweak to work for Ubuntu. I have tested these instructions on RedHat 7 and Ubuntu 16.10.