Updates to compiling instructions for GCC 6 #682
Conversation
jgwilson42
changed the title
| @@ -36,7 +36,7 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution. | |||
|
|
|||
| 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.
|
|
||
| On Redhat/Fedora etc., do | ||
|
|
||
| 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.
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.