diff --git a/.travis.yml b/.travis.yml index 50d63e593..81ddefb8b 100644 --- a/.travis.yml +++ b/.travis.yml @@ -22,10 +22,17 @@ env: # 64-bit Clang 3.9 RelWithDebInfo - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo + # Debug builds + # + # Note the unit tests for the debug builds are compiled but **not** + # executed. This is because the debug build of unit tests takes a large + # amount of time to execute compared to the optimized builds. The hope is + # that just running the optimized unit tests is sufficient. + # # 64-bit GCC 5.4 Debug - - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug + - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug RUN_UNIT_TESTS=BUILD_ONLY # 64-bit Clang Debug - - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug + - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug RUN_UNIT_TESTS=BUILD_ONLY # 32-bit GCC 5.4 RelWithDebInfo - LINUX_BASE=ubuntu32_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=i686 Z3_BUILD_TYPE=RelWithDebInfo @@ -57,7 +64,7 @@ env: # 64-bit GCC 4.8 RelWithDebInfo - 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=RelWithDebInfo # 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 + - 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 RUN_UNIT_TESTS=BUILD_ONLY # macOS (a.k.a OSX) support matrix: diff --git a/contrib/ci/Dockerfiles/z3_build.Dockerfile b/contrib/ci/Dockerfiles/z3_build.Dockerfile index 2d16d5394..07504e6b9 100644 --- a/contrib/ci/Dockerfiles/z3_build.Dockerfile +++ b/contrib/ci/Dockerfiles/z3_build.Dockerfile @@ -2,34 +2,33 @@ ARG DOCKER_IMAGE_BASE FROM ${DOCKER_IMAGE_BASE} -# Specify defaults. This can be changed when invoking +# Build arguments. This can be changed when invoking # `docker build`. -ARG ASAN_BUILD=0 -ARG BUILD_DOCS=0 -ARG CC=gcc -ARG CXX=g++ -ARG DOTNET_BINDINGS=1 -ARG JAVA_BINDINGS=1 -ARG NO_SUPPRESS_OUTPUT=0 -ARG PYTHON_BINDINGS=1 +ARG ASAN_BUILD +ARG BUILD_DOCS +ARG CC +ARG CXX +ARG DOTNET_BINDINGS +ARG JAVA_BINDINGS +ARG NO_SUPPRESS_OUTPUT +ARG PYTHON_BINDINGS ARG PYTHON_EXECUTABLE=/usr/bin/python2.7 -ARG RUN_SYSTEM_TESTS=1 -ARG RUN_UNIT_TESTS=1 -ARG TARGET_ARCH=x86_64 -ARG TEST_INSTALL=1 -ARG UBSAN_BUILD=0 -ARG USE_LIBGMP=0 -ARG USE_LTO=0 -ARG USE_OPENMP=1 +ARG RUN_SYSTEM_TESTS +ARG RUN_UNIT_TESTS +ARG TARGET_ARCH +ARG TEST_INSTALL +ARG UBSAN_BUILD +ARG USE_LIBGMP +ARG USE_LTO +ARG USE_OPENMP ARG Z3_SRC_DIR=/home/user/z3_src -ARG Z3_BUILD_TYPE=RelWithDebInfo -ARG Z3_CMAKE_GENERATOR=Ninja -ARG Z3_INSTALL_PREFIX=/usr -ARG Z3_STATIC_BUILD=0 -# Blank default indicates use latest. +ARG Z3_BUILD_TYPE +ARG Z3_CMAKE_GENERATOR +ARG Z3_INSTALL_PREFIX +ARG Z3_STATIC_BUILD ARG Z3_SYSTEM_TEST_GIT_REVISION -ARG Z3_WARNINGS_AS_ERRORS=SERIOUS_ONLY -ARG Z3_VERBOSE_BUILD_OUTPUT=0 +ARG Z3_WARNINGS_AS_ERRORS +ARG Z3_VERBOSE_BUILD_OUTPUT ENV \ ASAN_BUILD=${ASAN_BUILD} \ @@ -74,6 +73,7 @@ ADD *.txt *.md RELEASE_NOTES ${Z3_SRC_DIR}/ ADD \ /contrib/ci/scripts/build_z3_cmake.sh \ + /contrib/ci/scripts/ci_defaults.sh \ /contrib/ci/scripts/set_compiler_flags.sh \ /contrib/ci/scripts/set_generator_args.sh \ ${Z3_SRC_DIR}/contrib/ci/scripts/ diff --git a/contrib/ci/README.md b/contrib/ci/README.md index 2e117c8b1..99bbcd7a6 100644 --- a/contrib/ci/README.md +++ b/contrib/ci/README.md @@ -31,7 +31,7 @@ the future. * `NO_SUPPRESS_OUTPUT` - Don't suppress output of some commands (`0` or `1`) * `PYTHON_BINDINGS` - Build and test Python API bindings (`0` or `1`) * `RUN_SYSTEM_TESTS` - Run system tests (`0` or `1`) -* `RUN_UNIT_TESTS` - Run unit tests (`0` or `1`) +* `RUN_UNIT_TESTS` - Run unit tests (`BUILD_ONLY` or `BUILD_AND_RUN` or `SKIP`) * `TARGET_ARCH` - Target architecture (`x86_64` or `i686`) * `TEST_INSTALL` - Test running `install` target (`0` or `1`) * `UBSAN_BUILD` - Do [UndefinedBehaviourSanitizer](https://clang.llvm.org/docs/UndefinedBehaviorSanitizer.html) build (`0` or `1`) @@ -58,8 +58,9 @@ The `scripts/travis_ci_linux_entry_point.sh` script variables (if set) into the build using the `--build-arg` argument of the `docker run` command. -If an environemnt variable is not set a defaults value is used which can be -found in `Dockerfiles/z3_build.Dockerfile`. +The default values of the configuration environment variables +can be found in +[`scripts/ci_defaults.sh`](scripts/ci_defaults.sh). #### Linux specific configuration variables @@ -67,8 +68,9 @@ found in `Dockerfiles/z3_build.Dockerfile`. #### Reproducing a build locally -A build can be reproduced locally by using the `scripts/travis_ci_linux_entry_point.sh` -script and setting the appropriate environment variable. +A build can be reproduced locally by using the +`scripts/travis_ci_linux_entry_point.sh` script and setting the appropriate +environment variable. For example lets say we wanted to reproduce the build below. @@ -104,11 +106,43 @@ feature might be removed in the future. It may be better to just build the base image once (outside of TravisCI), upload it to [DockerHub](https://hub.docker.com/) and have the build pull down the pre-built -image everytime. +image every time. An [organization](https://hub.docker.com/u/z3prover/) has been created on DockerHub for this. ### macOS -Not yet implemented. +For macOS we execute directly on TravisCI's macOS environment. The entry point +for the TravisCI builds is the +[`scripts/travis_ci_osx_entry_point.sh`](scripts/travis_ci_osx_entry_point.sh) +scripts. + +#### macOS specific configuration variables + +* `MACOS_SKIP_DEPS_UPDATE` - If set to `1` installing the necessary build dependencies + is skipped. This is useful for local testing if the dependencies are already installed. +* `MACOS_UPDATE_CMAKE` - If set to `1` the installed version of CMake will be upgraded. + +#### Reproducing a build locally + +To reproduce a build (e.g. like the one shown below) + +```yaml +- os: osx + osx_image: xcode8.3 + # Note: Apple Clang does not support OpenMP + env: Z3_BUILD_TYPE=RelWithDebInfo USE_OPENMP=0 +``` + +Run the following: + +```bash +TRAVIS_BUILD_DIR=$(pwd) \ +Z3_BUILD_TYPE=RelWithDebInfo \ +USE_OPEN_MP=0 \ +contrib/ci/scripts/travis_ci_osx_entry_point.sh +``` + +Note this assumes that the current working directory is the root of the Z3 +git repository. diff --git a/contrib/ci/scripts/ci_defaults.sh b/contrib/ci/scripts/ci_defaults.sh new file mode 100644 index 000000000..d8e9376d8 --- /dev/null +++ b/contrib/ci/scripts/ci_defaults.sh @@ -0,0 +1,54 @@ +# This file should be sourced by other scripts +# and not executed directly + +# Set CI build defaults + +export ASAN_BUILD="${ASAN_BUILD:-0}" +export BUILD_DOCS="${BUILD_DOCS:-0}" +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 RUN_SYSTEM_TESTS="${RUN_SYSTEM_TESTS:-1}" +export RUN_UNIT_TESTS="${RUN_UNIT_TESTS:-BUILD_AND_RUN}" +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}" + +export Z3_BUILD_TYPE="${Z3_BUILD_TYPE:-RelWithDebInfo}" +export Z3_CMAKE_GENERATOR="${Z3_CMAKE_GENERATOR:-Ninja}" +export Z3_STATIC_BUILD="${Z3_STATIC_BUILD:-0}" +# Default is blank which means get latest revision +export Z3_SYSTEM_TEST_GIT_REVISION="${Z3_SYSTEM_TEST_GIT_REVISION:-}" +export Z3_WARNINGS_AS_ERRORS="${Z3_WARNINGS_AS_ERRORS:-SERIOUS_ONLY}" +export Z3_VERBOSE_BUILD_OUTPUT="${Z3_VERBOSE_BUILD_OUTPUT:-0}" + +# Platform specific defaults +PLATFORM="$(uname -s)" +case "${PLATFORM}" in + Linux*) + export C_COMPILER="${C_COMPILER:-gcc}" + export CXX_COMPILER="${CXX_COMPILER:-g++}" + export Z3_INSTALL_PREFIX="${Z3_INSTALL_PREFIX:-/usr}" + ;; + Darwin*) + export C_COMPILER="${C_COMPILER:-clang}" + export CXX_COMPILER="${CXX_COMPILER:-clang++}" + export Z3_INSTALL_PREFIX="${Z3_INSTALL_PREFIX:-/usr/local}" + ;; + *) + echo "Unknown platform \"${PLATFORM}\"" + exit 1 + ;; +esac +unset PLATFORM + +# NOTE: The following variables are not set here because +# they are specific to the CI implementation +# PYTHON_EXECUTABLE +# Z3_SRC_DIR +# Z3_BUILD_DIR +# Z3_SYSTEM_TEST_DIR diff --git a/contrib/ci/scripts/set_generator_args.sh b/contrib/ci/scripts/set_generator_args.sh index 0ef7b76aa..a704c518b 100644 --- a/contrib/ci/scripts/set_generator_args.sh +++ b/contrib/ci/scripts/set_generator_args.sh @@ -1,4 +1,4 @@ -# This script should is intended to be included by other +# This script is intended to be included by other # scripts and should not be executed directly : ${Z3_CMAKE_GENERATOR?"Z3_CMAKE_GENERATOR must be specified"} diff --git a/contrib/ci/scripts/test_z3_unit_tests_cmake.sh b/contrib/ci/scripts/test_z3_unit_tests_cmake.sh index 666673328..e1c927f58 100755 --- a/contrib/ci/scripts/test_z3_unit_tests_cmake.sh +++ b/contrib/ci/scripts/test_z3_unit_tests_cmake.sh @@ -10,17 +10,35 @@ set -o pipefail : ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"} : ${RUN_UNIT_TESTS?"RUN_UNIT_TESTS must be specified"} -if [ "X${RUN_UNIT_TESTS}" != "X1" ]; then - echo "Skipping unit tests" - exit 0 -fi - # Set CMake generator args source ${SCRIPT_DIR}/set_generator_args.sh cd "${Z3_BUILD_DIR}" -# Build and run internal tests -cmake --build $(pwd) --target test-z3 "${GENERATOR_ARGS[@]}" -# Run all tests that don't require arguments -run_quiet ./test-z3 /a +function build_unit_tests() { + # Build internal tests + cmake --build $(pwd) --target test-z3 "${GENERATOR_ARGS[@]}" +} + +function run_unit_tests() { + # Run all tests that don't require arguments + run_quiet ./test-z3 /a +} + +case "${RUN_UNIT_TESTS}" in + BUILD_AND_RUN) + build_unit_tests + run_unit_tests + ;; + BUILD_ONLY) + build_unit_tests + ;; + SKIP) + echo "RUN_UNIT_TESTS set to \"${RUN_UNIT_TESTS}\" so skipping build and run" + exit 0 + ;; + *) + echo "Error: RUN_UNIT_TESTS set to unhandled value \"${RUN_UNIT_TESTS}\"" + exit 1 + ;; +esac diff --git a/contrib/ci/scripts/travis_ci_linux_entry_point.sh b/contrib/ci/scripts/travis_ci_linux_entry_point.sh index 84b2dd400..bd2c9d2d1 100755 --- a/contrib/ci/scripts/travis_ci_linux_entry_point.sh +++ b/contrib/ci/scripts/travis_ci_linux_entry_point.sh @@ -11,16 +11,21 @@ DOCKER_FILE_DIR="$(cd ${SCRIPT_DIR}/../Dockerfiles; echo $PWD)" : ${LINUX_BASE?"LINUX_BASE must be specified"} - # Sanity check. Current working directory should be repo root if [ ! -f "./README.md" ]; then echo "Current working directory should be repo root" exit 1 fi +# Get defaults +source "${SCRIPT_DIR}/ci_defaults.sh" + BUILD_OPTS=() -# Override options if they have been provided. -# Otherwise the defaults in the Docker file will be used +# Pass Docker build arguments +if [ -n "${Z3_BUILD_TYPE}" ]; then + BUILD_OPTS+=("--build-arg" "Z3_BUILD_TYPE=${Z3_BUILD_TYPE}") +fi + if [ -n "${Z3_CMAKE_GENERATOR}" ]; then BUILD_OPTS+=("--build-arg" "Z3_CMAKE_GENERATOR=${Z3_CMAKE_GENERATOR}") fi diff --git a/contrib/ci/scripts/travis_ci_osx_entry_point.sh b/contrib/ci/scripts/travis_ci_osx_entry_point.sh index c5e8b4c02..ad3b0c7ab 100755 --- a/contrib/ci/scripts/travis_ci_osx_entry_point.sh +++ b/contrib/ci/scripts/travis_ci_osx_entry_point.sh @@ -6,26 +6,8 @@ set -x set -e set -o pipefail -# 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}" +# Get defaults +source "${SCRIPT_DIR}/ci_defaults.sh" if [ -z "${TRAVIS_BUILD_DIR}" ]; then echo "TRAVIS_BUILD_DIR must be set to root of Z3 repository" @@ -37,15 +19,12 @@ if [ ! -d "${TRAVIS_BUILD_DIR}" ]; then exit 1 fi +# These variables are specific to the macOS TravisCI +# implementation and are not set in `ci_defaults.sh`. +export PYTHON_EXECUTABLE="${PYTHON_EXECUTABLE:-$(which python)}" 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}"