Merge pull request #1 from batfish/ari-travis

Modifications for batfish (READY FOR REVIEW)

.travis.yml

@@ -17,63 +17,14 @@ env:
 ###############################################################################
 # Ubuntu 16.04 LTS
 ###############################################################################
-    # 64-bit UBSan Debug build
-    - 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 UBSAN_BUILD=1 RUN_UNIT_TESTS=SKIP
-    # 64-bit ASan Debug build
-    - 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 ASAN_BUILD=1 RUN_UNIT_TESTS=SKIP ASAN_DSO=/usr/lib/clang/3.9/lib/linux/libclang_rt.asan-x86_64.so
-    # Build for running unit tests under ASan/UBSan
-    # FIXME: We should really be doing a debug build but the unit tests run too
-    # slowly when we do that.
-    - 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 ASAN_BUILD=1 RUN_UNIT_TESTS=BUILD_AND_RUN ASAN_DSO=/usr/lib/clang/3.9/lib/linux/libclang_rt.asan-x86_64.so UBSAN_BUILD=1 RUN_API_EXAMPLES=0 RUN_SYSTEM_TESTS=0 DOTNET_BINDINGS=0 JAVA_BINDINGS=0 PYTHON_BINDINGS=0
-
-    # 64-bit GCC 5.4 RelWithDebInfo
-    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo
-    # 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 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 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
-
-    # Both of the two configurations below build the docs because the current
-    # implementation uses python as part of the building process.
-    # TODO: Teach one of the configurations to upload built docs somewhere.
-    # Test with Python 3 and API docs
-    - LINUX_BASE=ubuntu_16.04 PYTHON_EXECUTABLE=/usr/bin/python3 BUILD_DOCS=1
-    # Test with LibGMP and API docs
-    - LINUX_BASE=ubuntu_16.04 TARGET_ARCH=x86_64 USE_LIBGMP=1 BUILD_DOCS=1 PYTHON_EXECUTABLE=/usr/bin/python2.7
-
-    # Test without OpenMP
-    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo USE_OPENMP=0
-
-    # Unix Makefile generator build
-    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_CMAKE_GENERATOR="Unix Makefiles"
-
-    # LTO build
-    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 USE_LTO=1
-
-    # Static build. Note we have disable building the bindings because they won't work with a static libz3
-    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_STATIC_BUILD=1 DOTNET_BINDINGS=0 JAVA_BINDINGS=0 PYTHON_BINDINGS=0
+    # 64-bit default compilers RelWithDebInfo
+    - LINUX_BASE=ubuntu_16.04 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Release JAVA_BINDINGS=1
 
 ###############################################################################
 # Ubuntu 14.04 LTS
 ###############################################################################
-    # GCC 4.8
-    # 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 RUN_UNIT_TESTS=BUILD_ONLY
+    # 64-bit GCC 4.8 RelWithDebInfo java
+    - LINUX_BASE=ubuntu_14.04 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Release JAVA_BINDINGS=1
 
 # macOS (a.k.a OSX) support
 matrix:
@@ -82,9 +33,11 @@ matrix:
     # 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
+      osx_image: xcode9.2
+      env: Z3_BUILD_TYPE=Release USE_OPENMP=1 JAVA_BINDINGS=1
+    - os: osx
+      osx_image: xcode9.2
+      env: Z3_BUILD_TYPE=Release USE_OPENMP=0 JAVA_BINDINGS=1
 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

README.batfish

@@ -0,0 +1,16 @@
+To generate zips on your local machine, do:
+
+## Ubuntu 14,04 (USES DOCKER)
+LINUX_BASE=ubuntu_14.04 TRAVIS_OS_NAME=linux contrib/ci/scripts/travis_ci_entry_point.sh
+
+## Ubuntu 16,04 (USES DOCKER)
+LINUX_BASE=ubuntu_16.04 TRAVIS_OS_NAME=linux contrib/ci/scripts/travis_ci_entry_point.sh
+
+## OSX with OpenMP (RECOMMENDED, MUST BE RUN ON OSX, DOES NOT USE DOCKER)
+./package_z3_osx_openmp.sh
+
+## OSX without OpenMP (NOT RECOMMENDED, MUST BE RUN ON OSX, DOES NOT USE DOCKER)
+./package_z3_osx.sh
+
+
+Output zips are placed in build/generated-packages/

common.sh

@@ -0,0 +1,16 @@
+#!/usr/bin/env bash
+
+z3_git_version() {
+  if [ -n "${Z3_GIT_VERSION}" ]; then
+    echo "${Z3_GIT_VERSION}"
+  else
+    COMMIT_HASH="$(git rev-parse HEAD)"
+    if [ -z "${COMMIT_HASH}" ]; then
+       echo "Not a git repository" 1>&2
+       exit 1
+    fi
+    COMMIT_DATE="$(git show -s --format=%ci | awk '{ print $1 }')"
+    echo "${COMMIT_DATE}-${COMMIT_HASH}"
+  fi
+}
+

contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile

@@ -17,13 +17,14 @@ RUN apt-get update && \
         libgomp1 \
         lib32gomp1 \
         llvm-3.9 \
+        lsb-release \
         make \
-        mono-devel \
         ninja-build \
         python3 \
         python3-setuptools \
         python2.7 \
-        python-setuptools
+        python-setuptools \
+        zip
 
 # Create `user` user for container with password `user`.  and give it
 # password-less sudo access

contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile

@@ -19,14 +19,15 @@ RUN apt-get update && \
         libomp5 \
         libomp-dev \
         llvm-3.9 \
+        lsb-release \
         make \
-        mono-devel \
         ninja-build \
         python3 \
         python3-setuptools \
         python2.7 \
         python-setuptools \
-        sudo
+        sudo \
+        zip
 
 # Create `user` user for container with password `user`.  and give it
 # password-less sudo access

contrib/ci/Dockerfiles/z3_build.Dockerfile

@@ -1,7 +1,6 @@
 ARG DOCKER_IMAGE_BASE
 FROM ${DOCKER_IMAGE_BASE}
 
-
 # Build arguments. This can be changed when invoking
 # `docker build`.
 ARG ASAN_BUILD
@@ -27,99 +26,31 @@ ARG USE_OPENMP
 ARG Z3_SRC_DIR=/home/user/z3_src
 ARG Z3_BUILD_TYPE
 ARG Z3_CMAKE_GENERATOR
+ARG Z3_GIT_VERSION
 ARG Z3_INSTALL_PREFIX
 ARG Z3_STATIC_BUILD
 ARG Z3_SYSTEM_TEST_GIT_REVISION
 ARG Z3_WARNINGS_AS_ERRORS
 ARG Z3_VERBOSE_BUILD_OUTPUT
 
 ENV \
-  ASAN_BUILD=${ASAN_BUILD} \
-  ASAN_DSO=${ASAN_DSO} \
-  BUILD_DOCS=${BUILD_DOCS} \
   CC=${CC} \
+  Z3_GIT_VERSION=${Z3_GIT_VERSION} \
   CXX=${CXX} \
-  DOTNET_BINDINGS=${DOTNET_BINDINGS} \
-  JAVA_BINDINGS=${JAVA_BINDINGS} \
-  NO_SUPPRESS_OUTPUT=${NO_SUPPRESS_OUTPUT} \
-  PYTHON_BINDINGS=${PYTHON_BINDINGS} \
-  PYTHON_EXECUTABLE=${PYTHON_EXECUTABLE} \
-  SANITIZER_PRINT_SUPPRESSIONS=${SANITIZER_PRINT_SUPPRESSIONS} \
-  RUN_API_EXAMPLES=${RUN_API_EXAMPLES} \
-  RUN_SYSTEM_TESTS=${RUN_SYSTEM_TESTS} \
-  RUN_UNIT_TESTS=${RUN_UNIT_TESTS} \
-  TARGET_ARCH=${TARGET_ARCH} \
-  TEST_INSTALL=${TEST_INSTALL} \
-  UBSAN_BUILD=${UBSAN_BUILD} \
-  USE_LIBGMP=${USE_LIBGMP} \
-  USE_LTO=${USE_LTO} \
-  USE_OPENMP=${USE_OPENMP} \
   Z3_SRC_DIR=${Z3_SRC_DIR} \
   Z3_BUILD_DIR=/home/user/z3_build \
-  Z3_BUILD_TYPE=${Z3_BUILD_TYPE} \
-  Z3_CMAKE_GENERATOR=${Z3_CMAKE_GENERATOR} \
-  Z3_VERBOSE_BUILD_OUTPUT=${Z3_VERBOSE_BUILD_OUTPUT} \
-  Z3_STATIC_BUILD=${Z3_STATIC_BUILD} \
-  Z3_SYSTEM_TEST_DIR=/home/user/z3_system_test \
-  Z3_SYSTEM_TEST_GIT_REVISION=${Z3_SYSTEM_TEST_GIT_REVISION} \
-  Z3_WARNINGS_AS_ERRORS=${Z3_WARNINGS_AS_ERRORS} \
-  Z3_INSTALL_PREFIX=${Z3_INSTALL_PREFIX}
-
-# We add context across incrementally to maximal cache reuse
+  Z3_BUILD_TYPE=${Z3_BUILD_TYPE}
 
 # Build Z3
-RUN mkdir -p "${Z3_SRC_DIR}" && \
-  mkdir -p "${Z3_SRC_DIR}/contrib/ci/scripts" && \
-  mkdir -p "${Z3_SRC_DIR}/contrib/suppressions/sanitizers"
-# Deliberately leave out `contrib`
-ADD /cmake ${Z3_SRC_DIR}/cmake/
-ADD /doc ${Z3_SRC_DIR}/doc/
-ADD /examples ${Z3_SRC_DIR}/examples/
-ADD /scripts ${Z3_SRC_DIR}/scripts/
-ADD /src ${Z3_SRC_DIR}/src/
-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/
-RUN ${Z3_SRC_DIR}/contrib/ci/scripts/build_z3_cmake.sh
-
-# Test building docs
-ADD \
-  /contrib/ci/scripts/test_z3_docs.sh \
-  /contrib/ci/scripts/run_quiet.sh \
-  ${Z3_SRC_DIR}/contrib/ci/scripts/
-RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_docs.sh
-
-# Test examples
-ADD \
-  /contrib/ci/scripts/test_z3_examples_cmake.sh \
-  /contrib/ci/scripts/sanitizer_env.sh \
-  ${Z3_SRC_DIR}/contrib/ci/scripts/
-ADD \
-  /contrib/suppressions/sanitizers/asan.txt \
-  /contrib/suppressions/sanitizers/lsan.txt \
-  /contrib/suppressions/sanitizers/ubsan.txt \
-  ${Z3_SRC_DIR}/contrib/suppressions/sanitizers/
-RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_examples_cmake.sh
-
-# Run unit tests
-ADD \
-  /contrib/ci/scripts/test_z3_unit_tests_cmake.sh \
-  ${Z3_SRC_DIR}/contrib/ci/scripts/
-RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_unit_tests_cmake.sh
-
-# Run system tests
-ADD \
-  /contrib/ci/scripts/test_z3_system_tests.sh \
-  ${Z3_SRC_DIR}/contrib/ci/scripts/
-RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_system_tests.sh
+RUN mkdir -p "${Z3_SRC_DIR}"
+ADD --chown=user /cmake ${Z3_SRC_DIR}/cmake/
+ADD --chown=user /doc ${Z3_SRC_DIR}/doc/
+ADD --chown=user /examples ${Z3_SRC_DIR}/examples/
+ADD --chown=user /scripts ${Z3_SRC_DIR}/scripts/
+ADD --chown=user /src ${Z3_SRC_DIR}/src/
+ADD --chown=user *.txt *.md RELEASE_NOTES ${Z3_SRC_DIR}/
+ADD --chown=user /linux_common.sh ${Z3_SRC_DIR}/
+ADD --chown=user /common.sh ${Z3_SRC_DIR}/
+ADD --chown=user /package_z3_linux.sh ${Z3_SRC_DIR}/
+RUN ${Z3_SRC_DIR}/package_z3_linux.sh
 
-# Test install
-ADD \
-  /contrib/ci/scripts/test_z3_install_cmake.sh \
-  ${Z3_SRC_DIR}/contrib/ci/scripts/
-RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_install_cmake.sh

contrib/ci/scripts/install_deps_osx.sh

@@ -45,3 +45,5 @@ fi
 if [ "X${JAVA_BINDINGS}" = "X1" ]; then
   brew cask install java
 fi
+brew_install_or_upgrade llvm
+

contrib/ci/scripts/travis_ci_linux_entry_point.sh

@@ -6,6 +6,12 @@ set -x
 set -e
 set -o pipefail
 
+REPO_ROOT="${SCRIPT_DIR}/../../.."
+. "${REPO_ROOT}/common.sh"
+Z3_GIT_VERSION="$(z3_git_version)"
+PACKAGE_OUTPUT_DIR="${REPO_ROOT}/build/generated-packages"
+mkdir -p "${PACKAGE_OUTPUT_DIR}"
+
 DOCKER_FILE_DIR="$(cd ${SCRIPT_DIR}/../Dockerfiles; echo $PWD)"
 
 : ${LINUX_BASE?"LINUX_BASE must be specified"}
@@ -71,6 +77,8 @@ if [ -n "${C_COMPILER}" ]; then
   BUILD_OPTS+=("--build-arg" "CC=${C_COMPILER}")
 fi
 
+BUILD_OPTS+=("--build-arg" "Z3_GIT_VERSION=${Z3_GIT_VERSION}")
+
 # TravisCI reserves CXX for itself so use a different name
 if [ -n "${CXX_COMPILER}" ]; then
   BUILD_OPTS+=("--build-arg" "CXX=${CXX_COMPILER}")
@@ -153,10 +161,6 @@ case ${LINUX_BASE} in
     BASE_DOCKER_FILE="${DOCKER_FILE_DIR}/z3_base_ubuntu_16.04.Dockerfile"
     BASE_DOCKER_IMAGE_NAME="z3_base_ubuntu:16.04"
     ;;
-  ubuntu32_16.04)
-    BASE_DOCKER_FILE="${DOCKER_FILE_DIR}/z3_base_ubuntu32_16.04.Dockerfile"
-    BASE_DOCKER_IMAGE_NAME="z3_base_ubuntu32:16.04"
-    ;;
   *)
     echo "Unknown Linux base ${LINUX_BASE}"
     exit 1
@@ -226,7 +230,13 @@ else
 fi
 
 # Now build Z3 and test it using the created base image
+export POSTBUILD_IMAGE="batfish/z3-docker-postbuild-$(echo "${LINUX_BASE}" | tr -d '.')"
 docker build \
+  -t "${POSTBUILD_IMAGE}" \
   -f "${DOCKER_BUILD_FILE}" \
   "${BUILD_OPTS[@]}" \
   .
+DOCKER_REPO_ROOT="/home/user/z3_src"
+Z3_ZIP="$(docker run "${POSTBUILD_IMAGE}" /bin/bash -c ". ${DOCKER_REPO_ROOT}/linux_common.sh && linux_zip_name")"
+docker cp "$(docker create "${POSTBUILD_IMAGE}"):${DOCKER_REPO_ROOT}/build/generated-packages/${Z3_ZIP}" "${PACKAGE_OUTPUT_DIR}/"
+