search

TeamAmalgam / kodkod

Kodkod relational model finder
Other
3 stars 0 forks source link

Fix Kodkod build on Mavericks #58

Open mhyee opened 10 years ago

mhyee commented 10 years ago

OS X 10.9.x (Mavericks) aliases gcc to clang, so some of the solvers fail to compile. We could fix the code, but lingeling requires OpenMP, which apparently isn't supported by clang. (We could remove the dependency on lingeling.)

The workaround I've been using is to configure waf to use real gcc and g++ (I already have GCC 4.9 installed via homebrew): CC=/usr/local/bin/gcc-4.9 CXX=/usr/local/bin/g++-4.9 ./waf configure

This workaround isn't great; I have to set the environment variables every time I run configure, and this also means GCC is a dependency of Kodkod.

cpkleynhans commented 10 years ago

While removing lingeling from kodkod entirely is a possible solution, I don't think that it is correct thing to do in this case.

In this particular case, we should be able to just disable OpenMP entirely if we detect that clang is being used. Best practices are that programs that use OpenMP should still be correct if the pragmas are ignored so in theory that should be all we need.

If we can't just disable OpenMP, then we should either disable lingeling from building when clang is the compiler (not sure how we can detect this if gcc is aliasing clang but maybe its possible), or disable lingeling on OS X entirely (which is simple since this is already done on Windows).

mhyee commented 10 years ago

lingeling seems to build fine without OpenMP, but then cryptominisat has #include <omp.h> and explicitly calls OpenMP functions. So we would also have to disable cryptominisat as well.

We don't have to disable the libraries entirely under OS X, just under Mavericks. Python allows us to check for the OS X version, but annoyingly, it's returned as a string (i.e. "10.9.2")