Modify cmake build to build on MacOS #6344
Conversation
Codecov Report
@@ Coverage Diff @@
## develop #6344 +/- ##
===========================================
- Coverage 75.90% 75.90% -0.01%
===========================================
Files 1515 1515
Lines 164002 164004 +2
===========================================
+ Hits 124482 124483 +1
- Misses 39520 39521 +1
Continue to review full report at Codecov.
|
There was a problem hiding this comment.
I am not sure that forcing these settings on certain platforms, rather than fixing the build environment is the right approach. @NlightNFotis what do you think?
CMakeLists.txt
Outdated
| # Don't build jbmc on MacOS running on ARM | ||
| # See https://github.com/Homebrew/homebrew-core/blob/master/Formula/cbmc.rb | ||
| # See https://github.com/diffblue/cbmc/issues/6343 | ||
| execute_process(COMMAND uname -p |
There was a problem hiding this comment.
This I'm less happy about. Fundamentally, it looks like the issue is nothing to do with macos and/or M1 architecture. Its entirely down to Java version. It just happens that at this moment in time, brew will install a JVM 17 preview release on M1 macs (but still installs a JVM16 on x86 macs). I strongly suspect that as soon as more JVM17's are installed on other platforms (and OpenJDK 17 has just been officially released: https://mail.openjdk.java.net/pipermail/jdk-dev/2021-September/006037.html) this will bite other platforms.
There was a problem hiding this comment.
@chrisr-diffblue Done.
|
Instead of trying to force -DWITH_JBMC=OFF on Apple M1, I now suggest (for the inexperienced user) to try building with -DWITH_JBMC=OFF if jbmc fails to build on MacOS. Can we finish off the Java 16/17 issue quickly so we can delete this completely? |
markrtuttle
force-pushed
the
cmake-on-big-sur-arm
branch
from
8c9e9bd to
d40f23b
Compare
CMakeLists.txt
Outdated
| @@ -231,6 +240,10 @@ cprover_default_properties( | |||
| xml) | |||
|
|
|||
| option(WITH_JBMC "Build the JBMC Java front-end" ON) | |||
| if(CMAKE_HOST_SYSTEM_NAME STREQUAL Darwin) | |||
| # See https://github.com/diffblue/cbmc/issues/6343 | |||
| message(STATUS "Use -DWITH_JBMC=OFF if jbmc fails to build on MacOS") | |||
There was a problem hiding this comment.
I think (until we can fix the models library) this would be better as a check against the Java version, and then print a warning message and automatically set WITH_JBMC=OFF. Ultimately this is not about Darwin or any particular OS/architecture - its purely a Java version/API change.
There was a problem hiding this comment.
@chrisr-diffblue Done.
Build with CMAKE_C_COMPILER=/usr/bin/clang when building on MacOS. Build with -DWITH_JBMC=OFF when building with Java version > 16.
markrtuttle
force-pushed
the
cmake-on-big-sur-arm
branch
from
d40f23b to
8697cf3
Compare
|
Please do not merge this yet! We have fixed the issues in the Models Library, and we are now unblocked in terms of the Homebrew PR. I am looking into making the homebrew PR based on Java 17 (I can build with Java 17 locally no problem after the Models Library fix), and after this, then the only change required here is the default setup of the compiler to the |
| option(WITH_JBMC "Build the JBMC Java front-end" ON) | ||
| if(NOT JAVA_VERSION VERSION_LESS 17) |
There was a problem hiding this comment.
When https://github.com/Homebrew/homebrew-core/pull/85720/files gets merged to homebrew, cbmc (and jbmc by extension) will build cleanly with openJDK (version 17).
If you could drop the java version checks here (or at least, not deactivate jbmc building if java --version >= 17), then that would be great.
|
Closing in favor of #6359. The JDK 17 issues dealt with here are being fixed in another pull request. |
This pull request modifies the cmake build on MacOS to follow the instructions used in the homebrew cbmc formula for building cbmc on MacOS. This should make it easy to build cbmc on MacOS everywhere with just
cmake -S . -B build -GNinja.