From e898f515f75f12c363099f130e46bf638d1a42f9 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 12 Aug 2017 18:09:38 +0100 Subject: [PATCH 1/3] [CMake] Change how the default value of `USE_OPENMP` is set. This change means if the user explicitly passes `-DUSE_OPENMP=ON` to CMake during the first configure and the compiler does not support OpenMP the configure will fail but if the user doesn't specify it the build system will automatically enable/disable OpenMP support depending on whether it is supported by the compiler. This is an improvement on the previous behaviour because previously we would just emit a warning if `-DUSE_OPENMP=ON` was passed and the compiler didn't support OpenMP. --- CMakeLists.txt | 50 +++++++++++++++++++++++++++----------------------- 1 file changed, 27 insertions(+), 23 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 8845786f9..a3ed2a312 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -281,33 +281,37 @@ endif() ################################################################################ # OpenMP support ################################################################################ -option(USE_OPENMP "Use OpenMP" ON) -set(OPENMP_FOUND FALSE) -if (USE_OPENMP) - # Because this is on by default we make the configure succeed with a warning - # if OpenMP support is not detected. - find_package(OpenMP) - if (NOT OPENMP_FOUND) - message(WARNING "OpenMP support was requested but your compiler doesn't support it") - endif() -endif() - +find_package(OpenMP) if (OPENMP_FOUND) - list(APPEND Z3_COMPONENT_CXX_FLAGS ${OpenMP_CXX_FLAGS}) - # GCC and Clang need to have additional flags passed to the linker. - # We can't do ``target_link_libraries(libz3 INTERFACE ${OpenMP_CXX_FLAGS})`` - # because ``/openmp`` is interpreted as file name rather than a linker - # flag by MSVC and breaks the build - if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR - ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")) - list(APPEND Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS ${OpenMP_CXX_FLAGS}) - endif() - unset(CMAKE_REQUIRED_FLAGS) - message(STATUS "Using OpenMP") + set(USE_OPENMP_DEFAULT ON) +else() + set(USE_OPENMP_DEFAULT OFF) +endif() +# By setting `USE_OPENMP` this way configuration will fail during the first +# configure if the user explicitly passes `-DUSE_OPENMP=ON` and the compiler +# does not support OpenMP. However if the option is not set explicitly during +# the first configure OpenMP support will be automatically enabled/disabled +# depending on whether OpenMP is available. +option(USE_OPENMP "Use OpenMP" ${USE_OPENMP_DEFAULT}) + +if (USE_OPENMP) + if (NOT OPENMP_FOUND) + message(FATAL_ERROR "USE_OPENMP is ON but your compiler does not support OpenMP") + endif() + + list(APPEND Z3_COMPONENT_CXX_FLAGS ${OpenMP_CXX_FLAGS}) + # GCC and Clang need to have additional flags passed to the linker. + # We can't do ``target_link_libraries(libz3 INTERFACE ${OpenMP_CXX_FLAGS})`` + # because ``/openmp`` is interpreted as file name rather than a linker + # flag by MSVC and breaks the build + if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR + ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")) + list(APPEND Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS ${OpenMP_CXX_FLAGS}) + endif() + message(STATUS "Using OpenMP") else() list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_NO_OMP_") message(STATUS "Not using OpenMP") - set(USE_OPENMP OFF CACHE BOOL "Use OpenMP" FORCE) endif() ################################################################################ From e88f33ba949fce0c08d07c3c4c6c762bd01f1385 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 12 Aug 2017 17:18:31 +0100 Subject: [PATCH 2/3] [TravisCI] Unbreak showing interactive log output for non-LTO builds. c2f69ae9fbdcad143557309dd021aa7cafb21d36 added the use of the `travis_wait` command to all builds but this stops interactive build output from showing in the TravisCI web interface. To limit the scope of this change we only use it for LTO builds now. --- .travis.yml | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/.travis.yml b/.travis.yml index b179c5bfe..672d8ed52 100644 --- a/.travis.yml +++ b/.travis.yml @@ -65,7 +65,11 @@ env: # - os: osx # osx_image: xcode 8.2 script: - # Use `travis_wait` to handle commands that don't show output for a long period of time. - # Currently this is the LTO build which can be very slow. - # Allow at most 45 minutes for the build. - - travis_wait 45 contrib/ci/scripts/travis_ci_entry_point.sh + # Use `travis_wait` when doing LTO builds because this configuration will + # have long link times during which it will not show any output which + # TravisCI might kill due to perceived inactivity. + - if [ "X${USE_LTO}" = "X1" ]; then + travis_wait 45 contrib/ci/scripts/travis_ci_entry_point.sh || exit 1; + else + contrib/ci/scripts/travis_ci_entry_point.sh || exit 1; + fi From 850c2ebc0ca1bfbe11c3fa2040a367e89cc987d2 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 12 Aug 2017 13:52:30 +0100 Subject: [PATCH 3/3] [TravisCI] Add scripts to build and test Z3 on macOS (OSX) and add a single configuration to TravisCI to test. TravisCI is very slow at running macOS jobs so just have one configuration for now. --- .travis.yml | 15 +++-- contrib/ci/scripts/install_deps_osx.sh | 47 +++++++++++++ .../ci/scripts/travis_ci_osx_entry_point.sh | 66 ++++++++++++++++++- 3 files changed, 121 insertions(+), 7 deletions(-) create mode 100755 contrib/ci/scripts/install_deps_osx.sh diff --git a/.travis.yml b/.travis.yml index 672d8ed52..50d63e593 100644 --- a/.travis.yml +++ b/.travis.yml @@ -59,11 +59,16 @@ env: # 64-bit GCC 4.8 Debug - LINUX_BASE=ubuntu_14.04 C_COMPILER=/usr/bin/gcc-4.8 CXX_COMPILER=/usr/bin/g++-4.8 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug -# TODO: OSX support -#matrix: -# include: -# - os: osx -# osx_image: xcode 8.2 +# macOS (a.k.a OSX) support +matrix: + include: + # For now just test a single configuration. macOS builds on TravisCI are + # very slow so we should keep the number of configurations we test on this + # OS to a minimum. + - os: osx + osx_image: xcode8.3 + # Note: Apple Clang does not support OpenMP + env: Z3_BUILD_TYPE=RelWithDebInfo USE_OPENMP=0 script: # Use `travis_wait` when doing LTO builds because this configuration will # have long link times during which it will not show any output which diff --git a/contrib/ci/scripts/install_deps_osx.sh b/contrib/ci/scripts/install_deps_osx.sh new file mode 100755 index 000000000..f9eb5a844 --- /dev/null +++ b/contrib/ci/scripts/install_deps_osx.sh @@ -0,0 +1,47 @@ +#!/bin/bash + +SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )" +. ${SCRIPT_DIR}/run_quiet.sh + +set -x +set -e +set -o pipefail + +run_quiet brew update +export HOMEBREW_NO_AUTO_UPDATE=1 + +function brew_install_or_upgrade() { + if brew ls --versions "$1" > /dev/null 2>&1 ; then + brew upgrade "$1" + else + brew install "$1" + fi +} + +# FIXME: We should fix the versions of dependencies used +# so that we have reproducible builds. + +# HACK: Just use CMake version in TravisCI for now +if [ "X${MACOS_UPDATE_CMAKE}" = "X1" ]; then + brew_install_or_upgrade cmake +fi + +if [ "X${Z3_CMAKE_GENERATOR}" = "XNinja" ]; then + brew_install_or_upgrade ninja +fi + +if [ "X${USE_LIBGMP}" = "X1" ]; then + brew_install_or_upgrade gmp +fi + +if [ "X${BUILD_DOCS}" = "X1" ]; then + brew_install_or_upgrade doxygen +fi + +if [ "X${DOTNET_BINDINGS}" = "X1" ]; then + brew_install_or_upgrade mono +fi + +if [ "X${JAVA_BINDINGS}" = "X1" ]; then + brew cask install java +fi diff --git a/contrib/ci/scripts/travis_ci_osx_entry_point.sh b/contrib/ci/scripts/travis_ci_osx_entry_point.sh index 03be81647..c5e8b4c02 100755 --- a/contrib/ci/scripts/travis_ci_osx_entry_point.sh +++ b/contrib/ci/scripts/travis_ci_osx_entry_point.sh @@ -6,5 +6,67 @@ set -x set -e set -o pipefail -echo "Not implemented" -exit 1 +# Set defaults +# FIXME: Refactor this so we don't need to stay in sync with +# `z3_build.Dockerfile`. +export ASAN_BUILD="${ASAN_BUILD:-0}" +export BUILD_DOCS="${BUILD_DOCS:-0}" +export C_COMPILER="${C_COMPILER:-clang}" +export CXX_COMPILER="${CXX_COMPILER:-clang++}" +export DOTNET_BINDINGS="${DOTNET_BINDINGS:-1}" +export JAVA_BINDINGS="${JAVA_BINDINGS:-1}" +export NO_SUPPRESS_OUTPUT="${NO_SUPPRESS_OUTPUT:-0}" +export PYTHON_BINDINGS="${PYTHON_BINDINGS:-1}" +export PYTHON_EXECUTABLE="$(which python)" +export RUN_SYSTEM_TESTS="${RUN_SYSTEM_TESTS:-1}" +export RUN_UNIT_TESTS="${RUN_UNIT_TESTS:-1}" +export TARGET_ARCH="${TARGET_ARCH:-x86_64}" +export TEST_INSTALL="${TEST_INSTALL:-1}" +export UBSAN_BUILD="${UBSAN_BUILD:-0}" +export USE_LIBGMP="${USE_LIBGMP:-0}" +export USE_LTO="${USE_LTO:-0}" +export USE_OPENMP="${USE_OPENMP:-1}" + +if [ -z "${TRAVIS_BUILD_DIR}" ]; then + echo "TRAVIS_BUILD_DIR must be set to root of Z3 repository" + exit 1 +fi + +if [ ! -d "${TRAVIS_BUILD_DIR}" ]; then + echo "TRAVIS_BUILD_DIR must be a directory" + exit 1 +fi + +export Z3_SRC_DIR="${TRAVIS_BUILD_DIR}" +export Z3_BUILD_DIR="${Z3_SRC_DIR}/build" +export Z3_BUILD_TYPE="${Z3_BUILD_TYPE:-RelWithDebInfo}" +export Z3_CMAKE_GENERATOR="${Z3_CMAKE_GENERATOR:-Ninja}" +export Z3_INSTALL_PREFIX="${Z3_INSTALL_PREFIX:-/usr/local}" +export Z3_STATIC_BUILD="${Z3_STATIC_BUILD:-0}" +export Z3_SYSTEM_TEST_DIR="${Z3_SRC_DIR}/z3_system_test" +export Z3_WARNINGS_AS_ERRORS="${Z3_WARNINGS_AS_ERRORS:-SERIOUS_ONLY}" +export Z3_VERBOSE_BUILD_OUTPUT="${Z3_VERBOSE_BUILD_OUTPUT:-0}" + +# Overwrite whatever what set in TravisCI +export CC="${C_COMPILER}" +export CXX="${CXX_COMPILER}" + +if [ "X${MACOS_SKIP_DEPS_UPDATE}" = "X1" ]; then + # This is just for local testing to avoid updating + echo "Skipping dependency update" +else + "${SCRIPT_DIR}/install_deps_osx.sh" +fi + +# Build Z3 +"${SCRIPT_DIR}/build_z3_cmake.sh" +# Test building docs +"${SCRIPT_DIR}/test_z3_docs.sh" +# Test examples +"${SCRIPT_DIR}/test_z3_examples_cmake.sh" +# Run unit tests +"${SCRIPT_DIR}/test_z3_unit_tests_cmake.sh" +# Run system tests +"${SCRIPT_DIR}/test_z3_system_tests.sh" +# Test install +"${SCRIPT_DIR}/test_z3_install_cmake.sh"