Skip to content

Commit 8310fed

Browse files
author
Dan Liew
committed
[TravisCI] Implement TravisCI build and testing infrastructure for Linux
The Linux builds rely on Docker (using Ubuntu 16.04LTS and Ubuntu 14.04LTS) to build and test Z3 so that builds are easily reproducible. A build status button has been added to `README.md` so that it is easy to see the current build status. More documentation can be found in `contrib/ci/README.md`. This implementation currently tests 13 different configurations. If build times become too long we can remove some of them. Although it would be nice to test macOS builds that requires significantly more work so I have left this as future work.
1 parent be4b0ff commit 8310fed

21 files changed

+1107
-3
lines changed

‎.dockerignore

+4
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
**/*.swp
2+
**/*.pyc
3+
.git
4+
**/*.Dockerfile

‎.travis.yml

+68
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,68 @@
1+
cache:
2+
# This persistent cache is used to cache the building of
3+
# docker base images.
4+
directories:
5+
- $DOCKER_TRAVIS_CI_CACHE_DIR
6+
sudo: required
7+
language: cpp
8+
services:
9+
- docker
10+
env:
11+
global:
12+
# This environment variable tells the `travis_ci_linux_entry_point.sh`
13+
# script to look for a cached Docker image.
14+
- DOCKER_TRAVIS_CI_CACHE_DIR=$HOME/.cache/docker
15+
# Configurations
16+
matrix:
17+
###############################################################################
18+
# Ubuntu 16.04 LTS
19+
###############################################################################
20+
# 64-bit GCC 5.4 RelWithDebInfo
21+
- 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
22+
# 64-bit Clang 3.9 RelWithDebInfo
23+
- 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
24+
25+
# 64-bit GCC 5.4 Debug
26+
- 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
27+
# 64-bit Clang Debug
28+
- 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
29+
30+
# 32-bit GCC 5.4 RelWithDebInfo
31+
- LINUX_BASE=ubuntu32_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=i686 Z3_BUILD_TYPE=RelWithDebInfo
32+
33+
# Both of the two configurations below build the docs because the current
34+
# implementation uses python as part of the building process.
35+
# TODO: Teach one of the configurations to upload built docs somewhere.
36+
# Test with Python 3 and API docs
37+
- LINUX_BASE=ubuntu_16.04 PYTHON_EXECUTABLE=/usr/bin/python3 BUILD_DOCS=1
38+
# Test with LibGMP and API docs
39+
- LINUX_BASE=ubuntu_16.04 TARGET_ARCH=x86_64 USE_LIBGMP=1 BUILD_DOCS=1 PYTHON_EXECUTABLE=/usr/bin/python2.7
40+
41+
# Test without OpenMP
42+
- 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
43+
44+
# Unix Makefile generator build
45+
- 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"
46+
47+
# LTO build
48+
- LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 USE_LTO=1
49+
50+
# Static build. Note we have disable building the bindings because they won't work with a static libz3
51+
- 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
52+
53+
###############################################################################
54+
# Ubuntu 14.04 LTS
55+
###############################################################################
56+
# GCC 4.8
57+
# 64-bit GCC 4.8 RelWithDebInfo
58+
- 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
59+
# 64-bit GCC 4.8 Debug
60+
- 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
61+
62+
# TODO: OSX support
63+
#matrix:
64+
# include:
65+
# - os: osx
66+
# osx_image: xcode 8.2
67+
script:
68+
- contrib/ci/scripts/travis_ci_entry_point.sh

‎README.md

+3-3
Original file line numberDiff line numberDiff line change
@@ -12,9 +12,9 @@ See the [release notes](RELEASE_NOTES) for notes on various stable releases of Z
1212

1313
## Build status
1414

15-
| Windows x86 | Windows x64 | Ubuntu x64 | Ubuntu x86 | Debian x64 | OSX |
16-
| ----------- | ----------- | ---------- | ---------- | ---------- | --- |
17-
![win32-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge) | ![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/7/badge) | ![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge) | ![ubuntu-x86-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/6/badge) | ![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge) | ![osx-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/2/badge)
15+
| Windows x86 | Windows x64 | Ubuntu x64 | Ubuntu x86 | Debian x64 | OSX | TravisCI |
16+
| ----------- | ----------- | ---------- | ---------- | ---------- | --- | -------- |
17+
![win32-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge) | ![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/7/badge) | ![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge) | ![ubuntu-x86-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/6/badge) | ![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge) | ![osx-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/2/badge) | [![Build Status](https://travis-ci.org/Z3Prover/z3.svg?branch=master)](https://travis-ci.org/Z3Prover/z3)
1818

1919
[1]: #building-z3-on-windows-using-visual-studio-command-prompt
2020
[2]: #building-z3-using-make-and-gccclang

‎contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile

+50
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
# This base image is not officially supported by Docker it
2+
# is generated by running
3+
# ```
4+
# ./update.sh xenial
5+
# ```
6+
# from [email protected]:daald/docker-brew-ubuntu-core-32bit.git
7+
# at commit 34ea593b40b423755b7d46b6c8c89fc8162ea74b
8+
#
9+
# We could actually store the image generated by this Dockerfile
10+
# rather than just the bare image. However given we have a TravisCI
11+
# cache I'm not sure if it faster to use the TravisCI cache or to
12+
# download from DockerHub everytime.
13+
FROM z3prover/ubuntu32:16.04
14+
15+
RUN apt-get update && \
16+
apt-get -y --no-install-recommends install \
17+
binutils \
18+
clang \
19+
clang-3.9 \
20+
cmake \
21+
doxygen \
22+
default-jdk \
23+
gcc \
24+
gcc-5 \
25+
git \
26+
graphviz \
27+
g++ \
28+
g++ \
29+
libgmp-dev \
30+
libgomp1 \
31+
libomp5 \
32+
libomp-dev \
33+
make \
34+
mono-devel \
35+
ninja-build \
36+
python3 \
37+
python3-setuptools \
38+
python2.7 \
39+
python-setuptools \
40+
sudo
41+
42+
# Create `user` user for container with password `user`. and give it
43+
# password-less sudo access
44+
RUN useradd -m user && \
45+
echo user:user | chpasswd && \
46+
cp /etc/sudoers /etc/sudoers.bak && \
47+
echo 'user ALL=(root) NOPASSWD: ALL' >> /etc/sudoers
48+
USER user
49+
WORKDIR /home/user
50+

‎contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile

+35
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
FROM ubuntu:14.04
2+
3+
RUN apt-get update && \
4+
apt-get -y --no-install-recommends install \
5+
binutils \
6+
clang-3.9 \
7+
cmake \
8+
doxygen \
9+
default-jdk \
10+
gcc-multilib \
11+
gcc-4.8-multilib \
12+
git \
13+
graphviz \
14+
g++-multilib \
15+
g++-4.8-multilib \
16+
libgmp-dev \
17+
libgomp1 \
18+
lib32gomp1 \
19+
make \
20+
mono-devel \
21+
ninja-build \
22+
python3 \
23+
python3-setuptools \
24+
python2.7 \
25+
python-setuptools
26+
27+
# Create `user` user for container with password `user`. and give it
28+
# password-less sudo access
29+
RUN useradd -m user && \
30+
echo user:user | chpasswd && \
31+
cp /etc/sudoers /etc/sudoers.bak && \
32+
echo 'user ALL=(root) NOPASSWD: ALL' >> /etc/sudoers
33+
USER user
34+
WORKDIR /home/user
35+

‎contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile

+38
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
FROM ubuntu:16.04
2+
3+
RUN apt-get update && \
4+
apt-get -y --no-install-recommends install \
5+
binutils \
6+
clang \
7+
clang-3.9 \
8+
cmake \
9+
doxygen \
10+
default-jdk \
11+
gcc-multilib \
12+
gcc-5-multilib \
13+
git \
14+
graphviz \
15+
g++-multilib \
16+
g++-5-multilib \
17+
libgmp-dev \
18+
libgomp1 \
19+
libomp5 \
20+
libomp-dev \
21+
make \
22+
mono-devel \
23+
ninja-build \
24+
python3 \
25+
python3-setuptools \
26+
python2.7 \
27+
python-setuptools \
28+
sudo
29+
30+
# Create `user` user for container with password `user`. and give it
31+
# password-less sudo access
32+
RUN useradd -m user && \
33+
echo user:user | chpasswd && \
34+
cp /etc/sudoers /etc/sudoers.bak && \
35+
echo 'user ALL=(root) NOPASSWD: ALL' >> /etc/sudoers
36+
USER user
37+
WORKDIR /home/user
38+

‎contrib/ci/Dockerfiles/z3_build.Dockerfile

+109
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,109 @@
1+
ARG DOCKER_IMAGE_BASE
2+
FROM ${DOCKER_IMAGE_BASE}
3+
4+
5+
# Specify defaults. This can be changed when invoking
6+
# `docker build`.
7+
ARG ASAN_BUILD=0
8+
ARG BUILD_DOCS=0
9+
ARG CC=gcc
10+
ARG CXX=g++
11+
ARG DOTNET_BINDINGS=1
12+
ARG JAVA_BINDINGS=1
13+
ARG NO_SUPPRESS_OUTPUT=0
14+
ARG PYTHON_BINDINGS=1
15+
ARG PYTHON_EXECUTABLE=/usr/bin/python2.7
16+
ARG RUN_SYSTEM_TESTS=1
17+
ARG RUN_UNIT_TESTS=1
18+
ARG TARGET_ARCH=x86_64
19+
ARG TEST_INSTALL=1
20+
ARG UBSAN_BUILD=0
21+
ARG USE_LIBGMP=0
22+
ARG USE_LTO=0
23+
ARG USE_OPENMP=1
24+
ARG Z3_SRC_DIR=/home/user/z3_src
25+
ARG Z3_BUILD_TYPE=RelWithDebInfo
26+
ARG Z3_CMAKE_GENERATOR=Ninja
27+
ARG Z3_INSTALL_PREFIX=/usr
28+
ARG Z3_STATIC_BUILD=0
29+
# Blank default indicates use latest.
30+
ARG Z3_SYSTEM_TEST_GIT_REVISION
31+
ARG Z3_VERBOSE_BUILD_OUTPUT=0
32+
33+
ENV \
34+
ASAN_BUILD=${ASAN_BUILD} \
35+
BUILD_DOCS=${BUILD_DOCS} \
36+
CC=${CC} \
37+
CXX=${CXX} \
38+
DOTNET_BINDINGS=${DOTNET_BINDINGS} \
39+
JAVA_BINDINGS=${JAVA_BINDINGS} \
40+
NO_SUPPRESS_OUTPUT=${NO_SUPPRESS_OUTPUT} \
41+
PYTHON_BINDINGS=${PYTHON_BINDINGS} \
42+
PYTHON_EXECUTABLE=${PYTHON_EXECUTABLE} \
43+
RUN_SYSTEM_TESTS=${RUN_SYSTEM_TESTS} \
44+
RUN_UNIT_TESTS=${RUN_UNIT_TESTS} \
45+
TARGET_ARCH=${TARGET_ARCH} \
46+
TEST_INSTALL=${TEST_INSTALL} \
47+
UBSAN_BUILD=${UBSAN_BUILD} \
48+
USE_LIBGMP=${USE_LIBGMP} \
49+
USE_LTO=${USE_LTO} \
50+
USE_OPENMP=${USE_OPENMP} \
51+
Z3_SRC_DIR=${Z3_SRC_DIR} \
52+
Z3_BUILD_DIR=/home/user/z3_build \
53+
Z3_CMAKE_GENERATOR=${Z3_CMAKE_GENERATOR} \
54+
Z3_VERBOSE_BUILD_OUTPUT=${Z3_VERBOSE_BUILD_OUTPUT} \
55+
Z3_STATIC_BUILD=${Z3_STATIC_BUILD} \
56+
Z3_SYSTEM_TEST_DIR=/home/user/z3_system_test \
57+
Z3_SYSTEM_TEST_GIT_REVISION=${Z3_SYSTEM_TEST_GIT_REVISION} \
58+
Z3_INSTALL_PREFIX=${Z3_INSTALL_PREFIX}
59+
60+
# We add context across incrementally to maximal cache reuse
61+
62+
# Build Z3
63+
RUN mkdir -p "${Z3_SRC_DIR}" && \
64+
mkdir -p "${Z3_SRC_DIR}/contrib/ci/scripts"
65+
# Deliberately leave out `contrib`
66+
ADD /cmake ${Z3_SRC_DIR}/cmake/
67+
ADD /doc ${Z3_SRC_DIR}/doc/
68+
ADD /examples ${Z3_SRC_DIR}/examples/
69+
ADD /scripts ${Z3_SRC_DIR}/scripts/
70+
ADD /src ${Z3_SRC_DIR}/src/
71+
ADD *.txt *.md RELEASE_NOTES ${Z3_SRC_DIR}/
72+
73+
ADD \
74+
/contrib/ci/scripts/build_z3_cmake.sh \
75+
/contrib/ci/scripts/set_compiler_flags.sh \
76+
/contrib/ci/scripts/set_generator_args.sh \
77+
${Z3_SRC_DIR}/contrib/ci/scripts/
78+
RUN ${Z3_SRC_DIR}/contrib/ci/scripts/build_z3_cmake.sh
79+
80+
# Test building docs
81+
ADD \
82+
/contrib/ci/scripts/test_z3_docs.sh \
83+
/contrib/ci/scripts/run_quiet.sh \
84+
${Z3_SRC_DIR}/contrib/ci/scripts/
85+
RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_docs.sh
86+
87+
# Test examples
88+
ADD \
89+
/contrib/ci/scripts/test_z3_examples_cmake.sh \
90+
${Z3_SRC_DIR}/contrib/ci/scripts/
91+
RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_examples_cmake.sh
92+
93+
# Run unit tests
94+
ADD \
95+
/contrib/ci/scripts/test_z3_unit_tests_cmake.sh \
96+
${Z3_SRC_DIR}/contrib/ci/scripts/
97+
RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_unit_tests_cmake.sh
98+
99+
# Run system tests
100+
ADD \
101+
/contrib/ci/scripts/test_z3_system_tests.sh \
102+
${Z3_SRC_DIR}/contrib/ci/scripts/
103+
RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_system_tests.sh
104+
105+
# Test install
106+
ADD \
107+
/contrib/ci/scripts/test_z3_install_cmake.sh \
108+
${Z3_SRC_DIR}/contrib/ci/scripts/
109+
RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_install_cmake.sh

0 commit comments

Comments
 (0)