[TravisCI] Refactor as many CI default options as possible so that

the Docker and "TravisCI macOS" builds share most of the same defaults
by sourcing the `ci_defaults.sh` file.

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 ASAN_BUILD
-ARG BUILD_DOCS=0
+ARG BUILD_DOCS
-ARG CC=gcc
+ARG CC
-ARG CXX=g++
+ARG CXX
-ARG DOTNET_BINDINGS=1
+ARG DOTNET_BINDINGS
-ARG JAVA_BINDINGS=1
+ARG JAVA_BINDINGS
-ARG NO_SUPPRESS_OUTPUT=0
+ARG NO_SUPPRESS_OUTPUT
-ARG PYTHON_BINDINGS=1
+ARG PYTHON_BINDINGS
-ARG PYTHON_EXECUTABLE=/usr/bin/python2.7
+ARG PYTHON_EXECUTABLE
-ARG RUN_SYSTEM_TESTS=1
+ARG RUN_SYSTEM_TESTS
-ARG RUN_UNIT_TESTS=1
+ARG RUN_UNIT_TESTS
-ARG TARGET_ARCH=x86_64
+ARG TARGET_ARCH
-ARG TEST_INSTALL=1
+ARG TEST_INSTALL
-ARG UBSAN_BUILD=0
+ARG UBSAN_BUILD
-ARG USE_LIBGMP=0
+ARG USE_LIBGMP
-ARG USE_LTO=0
+ARG USE_LTO
-ARG USE_OPENMP=1
+ARG USE_OPENMP
 ARG Z3_SRC_DIR=/home/user/z3_src
-ARG Z3_BUILD_TYPE=RelWithDebInfo
+ARG Z3_BUILD_TYPE
-ARG Z3_CMAKE_GENERATOR=Ninja
+ARG Z3_CMAKE_GENERATOR
-ARG Z3_INSTALL_PREFIX=/usr
+ARG Z3_INSTALL_PREFIX
-ARG Z3_STATIC_BUILD=0
+ARG Z3_STATIC_BUILD
-# Blank default indicates use latest.
 ARG Z3_SYSTEM_TEST_GIT_REVISION
-ARG Z3_WARNINGS_AS_ERRORS=SERIOUS_ONLY
+ARG Z3_WARNINGS_AS_ERRORS
-ARG Z3_VERBOSE_BUILD_OUTPUT=0
+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/

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 PYTHON_EXECUTABLE="${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}"
+
+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
+# Z3_SRC_DIR
+# Z3_BUILD_DIR
+# Z3_SYSTEM_TEST_DIR

contrib/ci/scripts/travis_ci_linux_entry_point.sh

@@ -11,13 +11,15 @@ 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

contrib/ci/scripts/travis_ci_osx_entry_point.sh

@@ -6,26 +6,8 @@ set -x
 set -e
 set -o pipefail
 
-# Set defaults
+# Get defaults
-# FIXME: Refactor this so we don't need to stay in sync with
+source "${SCRIPT_DIR}/ci_defaults.sh"
-# `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"
@@ -37,15 +19,11 @@ if [ ! -d "${TRAVIS_BUILD_DIR}" ]; then
   exit 1
 fi
 
+# These three variables are specific to the macOS TravisCI
+# implementation and are not set in `ci_defaults.sh`.
 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}"