mirror of
https://github.com/Z3Prover/z3
synced 2025-04-05 17:14:07 +00:00
Remove Travis CI configs.
This commit is contained in:
Bruce Mitchener
Nikolaj Bjorner
parent
774ce3d7ab
commit
3ab96281eb
|
|
@ -1,53 +0,0 @@
|
|||
cache:
|
||||
# This persistent cache is used to cache the building of
|
||||
# docker base images.
|
||||
directories:
|
||||
- $DOCKER_TRAVIS_CI_CACHE_DIR
|
||||
sudo: required
|
||||
language: cpp
|
||||
services:
|
||||
- docker
|
||||
env:
|
||||
global:
|
||||
# This environment variable tells the `travis_ci_linux_entry_point.sh`
|
||||
# script to look for a cached Docker image.
|
||||
- DOCKER_TRAVIS_CI_CACHE_DIR=$HOME/.cache/docker
|
||||
# Configurations
|
||||
matrix:
|
||||
###############################################################################
|
||||
# Ubuntu 20.04 LTS
|
||||
###############################################################################
|
||||
# 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.
|
||||
|
||||
# clang
|
||||
- LINUX_BASE=ubuntu_20.04 C_COMPILER=clang CXX_COMPILER=clang++ TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug
|
||||
- LINUX_BASE=ubuntu_20.04 C_COMPILER=clang CXX_COMPILER=clang++ TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Release UBSAN_BUILD=1
|
||||
- LINUX_BASE=ubuntu_20.04 C_COMPILER=clang CXX_COMPILER=clang++ TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Release ASAN_BUILD=1 DOTNET_BINDINGS=0 JAVA_BINDINGS=0 PYTHON_BINDINGS=0
|
||||
|
||||
# gcc
|
||||
# ubsan/msan builds too slow
|
||||
- LINUX_BASE=ubuntu_20.04 C_COMPILER=gcc CXX_COMPILER=g++ TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Release BUILD_DOCS=1
|
||||
- LINUX_BASE=ubuntu_20.04 C_COMPILER=gcc CXX_COMPILER=g++ TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug
|
||||
|
||||
# GMP library
|
||||
- LINUX_BASE=ubuntu_20.04 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Release USE_LIBGMP=1
|
||||
- LINUX_BASE=ubuntu_20.04 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug USE_LIBGMP=1
|
||||
|
||||
# Unix Makefile generator build
|
||||
- LINUX_BASE=ubuntu_20.04 TARGET_ARCH=x86_64 Z3_CMAKE_GENERATOR="Unix Makefiles"
|
||||
|
||||
# LTO build
|
||||
# too slow
|
||||
#- LINUX_BASE=ubuntu_20.04 C_COMPILER=gcc CXX_COMPILER=g++ TARGET_ARCH=x86_64 USE_LTO=1 RUN_UNIT_TESTS=BUILD_ONLY RUN_SYSTEM_TESTS=0
|
||||
#- LINUX_BASE=ubuntu_20.04 C_COMPILER=clang CXX_COMPILER=clang++ TARGET_ARCH=x86_64 USE_LTO=1 RUN_UNIT_TESTS=BUILD_ONLY RUN_SYSTEM_TESTS=0
|
||||
|
||||
# Static build. Note we have disable building the bindings because they won't work with a static libz3
|
||||
- LINUX_BASE=ubuntu_20.04 TARGET_ARCH=x86_64 Z3_STATIC_BUILD=1 DOTNET_BINDINGS=0 JAVA_BINDINGS=0 PYTHON_BINDINGS=0
|
||||
|
||||
|
||||
script:
|
||||
# Use `travis_wait` when building because some configurations don't produce an
|
||||
# output for a long time (linking & testing)
|
||||
- travis_wait 55 contrib/ci/scripts/travis_ci_entry_point.sh || exit 1;
|
||||
|
|
@ -1,34 +0,0 @@
|
|||
FROM ubuntu:20.04
|
||||
|
||||
ARG DEBIAN_FRONTEND=noninteractive
|
||||
RUN apt-get update && \
|
||||
apt-get -y --no-install-recommends install \
|
||||
cmake \
|
||||
make \
|
||||
ninja-build \
|
||||
clang \
|
||||
g++ \
|
||||
curl \
|
||||
doxygen \
|
||||
default-jdk \
|
||||
git \
|
||||
graphviz \
|
||||
python3 \
|
||||
python3-setuptools \
|
||||
python-is-python3 \
|
||||
sudo
|
||||
|
||||
RUN curl -SL https://packages.microsoft.com/config/ubuntu/20.04/packages-microsoft-prod.deb --output packages-microsoft-prod.deb && \
|
||||
dpkg -i packages-microsoft-prod.deb && \
|
||||
apt-get update && \
|
||||
apt-get -y --no-install-recommends install dotnet-sdk-2.1
|
||||
|
||||
# Create `user` user for container with password `user`. and give it
|
||||
# password-less sudo access
|
||||
RUN useradd -m user && \
|
||||
echo user:user | chpasswd && \
|
||||
cp /etc/sudoers /etc/sudoers.bak && \
|
||||
echo 'user ALL=(root) NOPASSWD: ALL' >> /etc/sudoers
|
||||
USER user
|
||||
WORKDIR /home/user
|
||||
#ENV ASAN_SYMBOLIZER_PATH=/usr/lib/llvm-7/bin/llvm-symbolizer
|
||||
|
|
@ -1,121 +0,0 @@
|
|||
ARG DOCKER_IMAGE_BASE
|
||||
FROM ${DOCKER_IMAGE_BASE}
|
||||
|
||||
|
||||
# Build arguments. This can be changed when invoking
|
||||
# `docker build`.
|
||||
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/python
|
||||
ARG RUN_API_EXAMPLES
|
||||
ARG RUN_SYSTEM_TESTS
|
||||
ARG RUN_UNIT_TESTS
|
||||
ARG SANITIZER_PRINT_SUPPRESSIONS
|
||||
ARG TARGET_ARCH
|
||||
ARG TEST_INSTALL
|
||||
ARG UBSAN_BUILD
|
||||
ARG Z3_USE_LIBGMP
|
||||
ARG USE_LTO
|
||||
ARG Z3_SRC_DIR=/home/user/z3_src
|
||||
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
|
||||
ARG Z3_VERBOSE_BUILD_OUTPUT
|
||||
|
||||
ENV \
|
||||
ASAN_BUILD=${ASAN_BUILD} \
|
||||
BUILD_DOCS=${BUILD_DOCS} \
|
||||
CC=${CC} \
|
||||
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} \
|
||||
Z3_USE_LIBGMP=${Z3_USE_LIBGMP} \
|
||||
USE_LTO=${USE_LTO} \
|
||||
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
|
||||
|
||||
# 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 *.cmake.in 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
|
||||
|
||||
# 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
|
||||
|
|
@ -1,147 +0,0 @@
|
|||
# Continuous integration scripts
|
||||
|
||||
## TravisCI
|
||||
|
||||
For testing on Linux and macOS we use [TravisCI](https://travis-ci.org/)
|
||||
|
||||
TravisCI consumes the `.travis.yml` file in the root of the repository
|
||||
to tell it how to build and test Z3.
|
||||
|
||||
However the logic for building and test Z3 is kept out of this file
|
||||
and instead in a set of scripts in `scripts/`. This avoids
|
||||
coupling the build to TravisCI tightly so we can migrate to another
|
||||
service if required in the future.
|
||||
|
||||
The scripts rely on a set of environment variables to control the configuration
|
||||
of the build. The `.travis.yml` declares a list of configuration with each
|
||||
configuration setting different environment variables.
|
||||
|
||||
Note that the build scripts currently only support Z3 built with CMake. Support
|
||||
for building Z3 using the older Python/Makefile build system might be added in
|
||||
the future.
|
||||
|
||||
### Configuration variables
|
||||
|
||||
* `ASAN_BUILD` - Do [AddressSanitizer](https://github.com/google/sanitizers/wiki/AddressSanitizer) build (`0` or `1`)
|
||||
* `BUILD_DOCS` - Build API documentation (`0` or `1`)
|
||||
* `C_COMPILER` - Path to C Compiler
|
||||
* `CXX_COMPILER` - Path to C++ Compiler
|
||||
* `DOTNET_BINDINGS` - Build and test .NET API bindings (`0` or `1`)
|
||||
* `JAVA_BINDINGS` - Build and test Java API bindings (`0` or `1`)
|
||||
* `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_API_EXAMPLES` - Build and run API examples (`0` or `1`)
|
||||
* `RUN_SYSTEM_TESTS` - Run system tests (`0` or `1`)
|
||||
* `RUN_UNIT_TESTS` - Run unit tests (`BUILD_ONLY` or `BUILD_AND_RUN` or `SKIP`)
|
||||
* `SANITIZER_PRINT_SUPPRESSIONS` - Show ASan/UBSan suppressions (`0` or `1`)
|
||||
* `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`)
|
||||
* `Z3_USE_LIBGMP` - Use [GNU multiple precision library](https://gmplib.org/) (`0` or `1`)
|
||||
* `USE_LTO` - Link binaries using link time optimization (`0` or `1`)
|
||||
* `Z3_BUILD_TYPE` - CMake build type (`RelWithDebInfo`, `Release`, `Debug`, or `MinSizeRel`)
|
||||
* `Z3_CMAKE_GENERATOR` - CMake generator (`Ninja` or `Unix Makefiles`)
|
||||
* `Z3_VERBOSE_BUILD_OUTPUT` - Show compile commands in CMake builds (`0` or `1`)
|
||||
* `Z3_BUILD_LIBZ3_SHARED` - Build Z3 binaries and libraries dynamically/statically (`0` or `1`)
|
||||
* `Z3_SYSTEM_TEST_GIT_REVISION` - Git revision of [z3test](https://github.com/Z3Prover/z3test). If empty latest revision will be used.
|
||||
* `Z3_WARNINGS_AS_ERRORS` - Set the `WARNINGS_AS_ERRORS` CMake option passed to Z3 (`OFF`, `ON`, or `SERIOUS_ONLY`)
|
||||
|
||||
### Linux
|
||||
|
||||
For Linux we use Docker to perform the build so that it easily reproducible
|
||||
on a local machine and so that we can avoid depending on TravisCI's environment
|
||||
and instead use a Linux distribution of our choice.
|
||||
|
||||
The `scripts/travis_ci_linux_entry_point.sh` script
|
||||
|
||||
1. Creates a base image containing all the dependencies needed to build and test Z3
|
||||
2. Builds and tests Z3 using the base image propagating configuration environment
|
||||
variables (if set) into the build using the `--build-arg` argument of the `docker run`
|
||||
command.
|
||||
|
||||
The default values of the configuration environment variables
|
||||
can be found in
|
||||
[`scripts/ci_defaults.sh`](scripts/ci_defaults.sh).
|
||||
|
||||
#### Linux specific configuration variables
|
||||
|
||||
* `LINUX_BASE` - The base docker image identifier to use (`ubuntu_16.04`, `ubuntu32_16.04`, or `ubuntu_14.04`).
|
||||
|
||||
#### 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.
|
||||
|
||||
For example lets say we wanted to reproduce the build below.
|
||||
|
||||
```yaml
|
||||
|
||||
- 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
|
||||
```
|
||||
|
||||
This can be done by running the command
|
||||
|
||||
```bash
|
||||
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 scripts/travis_ci_linux_entry_point.sh
|
||||
```
|
||||
|
||||
The `docker build` command which we use internally supports caching. What this
|
||||
means in practice is that re-running the above command will re-use successfully
|
||||
completed stages of the build provided they haven't changed. This requires that
|
||||
the `Dockerfiles/z3_build.Dockerfile` is carefully crafted to avoid invalidating
|
||||
the cache when unrelated files sent to the build context change.
|
||||
|
||||
#### TravisCI docker image cache
|
||||
|
||||
To improve build times the Z3 base docker images are cached using
|
||||
[TravisCI's cache directory feature](https://docs.travis-ci.com/user/caching).
|
||||
If the `DOCKER_TRAVIS_CI_CACHE_DIR` environment variable is set (see `.travis.yml`)
|
||||
then the directory pointed to by the environment variable is used as a cache
|
||||
for Docker images.
|
||||
|
||||
The logic for this can be found in `scripts/travis_ci_linux_entry_point.sh`.
|
||||
The build time improvements are rather modest (~ 2 minutes) and the cache is
|
||||
rather large due to TravisCI giving each configuration its own cache. So this
|
||||
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 every time.
|
||||
|
||||
An [organization](https://hub.docker.com/u/z3prover/) has been created on
|
||||
DockerHub for this.
|
||||
|
||||
### macOS
|
||||
|
||||
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
|
||||
env: Z3_BUILD_TYPE=RelWithDebInfo
|
||||
```
|
||||
|
||||
Run the following:
|
||||
|
||||
```bash
|
||||
TRAVIS_BUILD_DIR=$(pwd) \
|
||||
Z3_BUILD_TYPE=RelWithDebInfo \
|
||||
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.
|
||||
|
|
@ -1,3 +0,0 @@
|
|||
# Maintainers
|
||||
|
||||
- Dan Liew (@delcypher)
|
||||
|
|
@ -1,133 +0,0 @@
|
|||
#!/bin/bash
|
||||
# This script builds Z3
|
||||
|
||||
SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )"
|
||||
|
||||
set -x
|
||||
set -e
|
||||
set -o pipefail
|
||||
|
||||
: ${Z3_SRC_DIR?"Z3_SRC_DIR must be specified"}
|
||||
: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"}
|
||||
: ${Z3_BUILD_TYPE?"Z3_BUILD_TYPE must be specified"}
|
||||
: ${Z3_CMAKE_GENERATOR?"Z3_CMAKE_GENERATOR must be specified"}
|
||||
: ${Z3_STATIC_BUILD?"Z3_STATIC_BUILD must be specified"}
|
||||
: ${Z3_USE_LIBGMP?"Z3_USE_LIBGMP must be specified"}
|
||||
: ${BUILD_DOCS?"BUILD_DOCS must be specified"}
|
||||
: ${PYTHON_EXECUTABLE?"PYTHON_EXECUTABLE must be specified"}
|
||||
: ${PYTHON_BINDINGS?"PYTHON_BINDINGS must be specified"}
|
||||
: ${DOTNET_BINDINGS?"DOTNET_BINDINGS must be specified"}
|
||||
: ${JAVA_BINDINGS?"JAVA_BINDINGS must be specified"}
|
||||
: ${USE_LTO?"USE_LTO must be specified"}
|
||||
: ${Z3_INSTALL_PREFIX?"Z3_INSTALL_PREFIX must be specified"}
|
||||
: ${Z3_WARNINGS_AS_ERRORS?"Z3_WARNINGS_AS_ERRORS must be specified"}
|
||||
: ${UBSAN_BUILD?"UBSAN_BUILD must be specified"}
|
||||
|
||||
ADDITIONAL_Z3_OPTS=()
|
||||
|
||||
# Static or dynamic libz3
|
||||
if [ "X${Z3_STATIC_BUILD}" = "X1" ]; then
|
||||
ADDITIONAL_Z3_OPTS+=('-DZ3_BUILD_LIBZ3_SHARED=OFF')
|
||||
else
|
||||
ADDITIONAL_Z3_OPTS+=('-DZ3_BUILD_LIBZ3_SHARED=ON')
|
||||
fi
|
||||
|
||||
# Use LibGMP?
|
||||
if [ "X${Z3_USE_LIBGMP}" = "X1" ]; then
|
||||
ADDITIONAL_Z3_OPTS+=('-DZ3_USE_LIB_GMP=ON')
|
||||
else
|
||||
ADDITIONAL_Z3_OPTS+=('-DZ3_USE_LIB_GMP=OFF')
|
||||
fi
|
||||
|
||||
# Use link time optimziation?
|
||||
if [ "X${USE_LTO}" = "X1" ]; then
|
||||
ADDITIONAL_Z3_OPTS+=('-DZ3_LINK_TIME_OPTIMIZATION=ON')
|
||||
else
|
||||
ADDITIONAL_Z3_OPTS+=('-DZ3_LINK_TIME_OPTIMIZATION=OFF')
|
||||
fi
|
||||
|
||||
# Build API docs?
|
||||
if [ "X${BUILD_DOCS}" = "X1" ]; then
|
||||
ADDITIONAL_Z3_OPTS+=( \
|
||||
'-DZ3_BUILD_DOCUMENTATION=ON' \
|
||||
'-DZ3_ALWAYS_BUILD_DOCS=OFF' \
|
||||
)
|
||||
else
|
||||
ADDITIONAL_Z3_OPTS+=('-DZ3_BUILD_DOCUMENTATION=OFF')
|
||||
fi
|
||||
|
||||
# Python bindings?
|
||||
if [ "X${PYTHON_BINDINGS}" = "X1" ]; then
|
||||
ADDITIONAL_Z3_OPTS+=( \
|
||||
'-DZ3_BUILD_PYTHON_BINDINGS=ON' \
|
||||
'-DZ3_INSTALL_PYTHON_BINDINGS=ON' \
|
||||
)
|
||||
else
|
||||
ADDITIONAL_Z3_OPTS+=( \
|
||||
'-DZ3_BUILD_PYTHON_BINDINGS=OFF' \
|
||||
'-DZ3_INSTALL_PYTHON_BINDINGS=OFF' \
|
||||
)
|
||||
fi
|
||||
|
||||
# .NET bindings?
|
||||
if [ "X${DOTNET_BINDINGS}" = "X1" ]; then
|
||||
ADDITIONAL_Z3_OPTS+=( \
|
||||
'-DZ3_BUILD_DOTNET_BINDINGS=ON' \
|
||||
'-DZ3_INSTALL_DOTNET_BINDINGS=ON' \
|
||||
)
|
||||
else
|
||||
ADDITIONAL_Z3_OPTS+=( \
|
||||
'-DZ3_BUILD_DOTNET_BINDINGS=OFF' \
|
||||
'-DZ3_INSTALL_DOTNET_BINDINGS=OFF' \
|
||||
)
|
||||
fi
|
||||
|
||||
# Java bindings?
|
||||
if [ "X${JAVA_BINDINGS}" = "X1" ]; then
|
||||
ADDITIONAL_Z3_OPTS+=( \
|
||||
'-DZ3_BUILD_JAVA_BINDINGS=ON' \
|
||||
'-DZ3_INSTALL_JAVA_BINDINGS=ON' \
|
||||
)
|
||||
else
|
||||
ADDITIONAL_Z3_OPTS+=( \
|
||||
'-DZ3_BUILD_JAVA_BINDINGS=OFF' \
|
||||
'-DZ3_INSTALL_JAVA_BINDINGS=OFF' \
|
||||
)
|
||||
fi
|
||||
|
||||
# Set compiler flags
|
||||
source ${SCRIPT_DIR}/set_compiler_flags.sh
|
||||
|
||||
if [ "X${UBSAN_BUILD}" = "X1" ]; then
|
||||
# HACK: When building with UBSan the C++ linker
|
||||
# must be used to avoid the following linker errors.
|
||||
# undefined reference to `__ubsan_vptr_type_cache'
|
||||
# undefined reference to `__ubsan_handle_dynamic_type_cache_miss'
|
||||
ADDITIONAL_Z3_OPTS+=( \
|
||||
'-DZ3_C_EXAMPLES_FORCE_CXX_LINKER=ON' \
|
||||
)
|
||||
fi
|
||||
|
||||
# Sanity check
|
||||
if [ ! -e "${Z3_SRC_DIR}/CMakeLists.txt" ]; then
|
||||
echo "Z3_SRC_DIR is invalid"
|
||||
exit 1
|
||||
fi
|
||||
|
||||
# Make build tree
|
||||
mkdir -p "${Z3_BUILD_DIR}"
|
||||
cd "${Z3_BUILD_DIR}"
|
||||
|
||||
# Configure
|
||||
cmake \
|
||||
-G "${Z3_CMAKE_GENERATOR}" \
|
||||
-DCMAKE_BUILD_TYPE=${Z3_BUILD_TYPE} \
|
||||
-DPYTHON_EXECUTABLE=${PYTHON_EXECUTABLE} \
|
||||
-DCMAKE_INSTALL_PREFIX=${Z3_INSTALL_PREFIX} \
|
||||
-DWARNINGS_AS_ERRORS=${Z3_WARNINGS_AS_ERRORS} \
|
||||
"${ADDITIONAL_Z3_OPTS[@]}" \
|
||||
"${Z3_SRC_DIR}"
|
||||
|
||||
# Build
|
||||
source ${SCRIPT_DIR}/set_generator_args.sh
|
||||
cmake --build $(pwd) "${GENERATOR_ARGS[@]}"
|
||||
|
|
@ -1,59 +0,0 @@
|
|||
# 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_API_EXAMPLES="${RUN_API_EXAMPLES:-1}"
|
||||
export RUN_SYSTEM_TESTS="${RUN_SYSTEM_TESTS:-1}"
|
||||
export RUN_UNIT_TESTS="${RUN_UNIT_TESTS:-BUILD_AND_RUN}"
|
||||
# Don't print suppressions by default because that breaks the Z3
|
||||
# regression tests because they don't expect them to appear in Z3's
|
||||
# output.
|
||||
export SANITIZER_PRINT_SUPPRESSIONS="${SANITIZER_PRINT_SUPPRESSIONS:-0}"
|
||||
export TARGET_ARCH="${TARGET_ARCH:-x86_64}"
|
||||
export TEST_INSTALL="${TEST_INSTALL:-1}"
|
||||
export UBSAN_BUILD="${UBSAN_BUILD:-0}"
|
||||
export Z3_USE_LIBGMP="${Z3_USE_LIBGMP:-0}"
|
||||
export USE_LTO="${USE_LTO:-0}"
|
||||
|
||||
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
|
||||
# ASAN_DSO
|
||||
# Z3_SRC_DIR
|
||||
# Z3_BUILD_DIR
|
||||
# Z3_SYSTEM_TEST_DIR
|
||||
|
|
@ -1,47 +0,0 @@
|
|||
#!/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${Z3_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
|
||||
|
|
@ -1,41 +0,0 @@
|
|||
# Simple wrapper function that runs a command suppressing
|
||||
# it's output. However it's output will be shown in the
|
||||
# case that `NO_SUPPRESS_OUTPUT` is set to `1` or the command
|
||||
# fails.
|
||||
#
|
||||
# The use case for this trying to avoid large logs on TravisCI
|
||||
function run_quiet() {
|
||||
if [ "X${NO_SUPPRESS_OUTPUT}" = "X1" ]; then
|
||||
"${@}"
|
||||
else
|
||||
OLD_SETTINGS="$-"
|
||||
set +x
|
||||
set +e
|
||||
TMP_DIR="${TMP_DIR:-/tmp/}"
|
||||
STDOUT="${TMP_DIR}/$$.stdout"
|
||||
STDERR="${TMP_DIR}/$$.stderr"
|
||||
"${@}" > "${STDOUT}" 2> "${STDERR}"
|
||||
EXIT_STATUS="$?"
|
||||
if [ "${EXIT_STATUS}" -ne 0 ]; then
|
||||
echo "Command \"$@\" failed"
|
||||
echo "EXIT CODE: ${EXIT_STATUS}"
|
||||
echo "STDOUT"
|
||||
echo ""
|
||||
echo "\`\`\`"
|
||||
cat ${STDOUT}
|
||||
echo "\`\`\`"
|
||||
echo ""
|
||||
echo "STDERR"
|
||||
echo ""
|
||||
echo "\`\`\`"
|
||||
cat ${STDERR}
|
||||
echo "\`\`\`"
|
||||
echo ""
|
||||
fi
|
||||
# Clean up
|
||||
rm "${STDOUT}" "${STDERR}"
|
||||
[ "$( echo "${OLD_SETTINGS}" | grep -c 'e')" != "0" ] && set -e
|
||||
[ "$( echo "${OLD_SETTINGS}" | grep -c 'x')" != "0" ] && set -x
|
||||
return ${EXIT_STATUS}
|
||||
fi
|
||||
}
|
||||
|
|
@ -1,58 +0,0 @@
|
|||
# This script is intended to be included by other
|
||||
# scripts and should not be executed directly
|
||||
|
||||
: ${Z3_SRC_DIR?"Z3_SRC_DIR must be specified"}
|
||||
: ${ASAN_BUILD?"ASAN_BUILD must be specified"}
|
||||
: ${UBSAN_BUILD?"UBSAN_BUILD must be specified"}
|
||||
|
||||
if [ "X${ASAN_BUILD}" = "X1" ]; then
|
||||
# Use suppression files
|
||||
export LSAN_OPTIONS="suppressions=${Z3_SRC_DIR}/contrib/suppressions/sanitizers/lsan.txt"
|
||||
# NOTE: If you get bad stacktraces try using `fast_unwind_on_malloc=0`
|
||||
# NOTE: `malloc_context_size` controls size of recorded stacktrace for allocations.
|
||||
# If the reported stacktraces appear incomplete try increasing the value.
|
||||
# leak checking disabled because it doesn't work on unpriviledged docker
|
||||
export ASAN_OPTIONS="malloc_context_size=100,detect_leaks=0,suppressions=${Z3_SRC_DIR}/contrib/suppressions/sanitizers/asan.txt"
|
||||
|
||||
: ${SANITIZER_PRINT_SUPPRESSIONS?"SANITIZER_PRINT_SUPPRESSIONS must be specified"}
|
||||
if [ "X${SANITIZER_PRINT_SUPPRESSIONS}" = "X1" ]; then
|
||||
export LSAN_OPTIONS="${LSAN_OPTIONS},print_suppressions=1"
|
||||
export ASAN_OPTIONS="${ASAN_OPTIONS},print_suppressions=1"
|
||||
else
|
||||
export LSAN_OPTIONS="${LSAN_OPTIONS},print_suppressions=0"
|
||||
export ASAN_OPTIONS="${ASAN_OPTIONS},print_suppressions=0"
|
||||
fi
|
||||
|
||||
#: ${ASAN_SYMBOLIZER_PATH?"ASAN_SYMBOLIZER_PATH must be specified"}
|
||||
|
||||
# Run command without checking for leaks
|
||||
function run_no_lsan() {
|
||||
ASAN_OPTIONS="${ASAN_OPTIONS},detect_leaks=0" "${@}"
|
||||
}
|
||||
|
||||
function run_non_native_binding() {
|
||||
"${@}"
|
||||
}
|
||||
else
|
||||
# In non-ASan build just run directly
|
||||
function run_no_lsan() {
|
||||
"${@}"
|
||||
}
|
||||
function run_non_native_binding() {
|
||||
"${@}"
|
||||
}
|
||||
fi
|
||||
|
||||
if [ "X${UBSAN_BUILD}" = "X1" ]; then
|
||||
# `halt_on_error=1,abort_on_error=1` means that on the first UBSan error
|
||||
# the program will terminate by calling `abort(). Without this UBSan will
|
||||
# allow execution to continue. We also use a suppression file.
|
||||
export UBSAN_OPTIONS="halt_on_error=1,abort_on_error=1,suppressions=${Z3_SRC_DIR}/contrib/suppressions/sanitizers/ubsan.txt"
|
||||
|
||||
: ${SANITIZER_PRINT_SUPPRESSIONS?"SANITIZER_PRINT_SUPPRESSIONS must be specified"}
|
||||
if [ "X${SANITIZER_PRINT_SUPPRESSIONS}" = "X1" ]; then
|
||||
export UBSAN_OPTIONS="${UBSAN_OPTIONS},print_suppressions=1"
|
||||
else
|
||||
export UBSAN_OPTIONS="${UBSAN_OPTIONS},print_suppressions=0"
|
||||
fi
|
||||
fi
|
||||
|
|
@ -1,46 +0,0 @@
|
|||
# This script should is intended to be included by other
|
||||
# scripts and should not be executed directly
|
||||
|
||||
: ${TARGET_ARCH?"TARGET_ARCH must be specified"}
|
||||
: ${ASAN_BUILD?"ASAN_BUILD must be specified"}
|
||||
: ${UBSAN_BUILD?"UBSAN_BUILD must be specified"}
|
||||
: ${CC?"CC must be specified"}
|
||||
: ${CXX?"CXX must be specified"}
|
||||
|
||||
case ${TARGET_ARCH} in
|
||||
x86_64)
|
||||
CXXFLAGS="${CXXFLAGS} -m64"
|
||||
CFLAGS="${CFLAGS} -m64"
|
||||
;;
|
||||
i686)
|
||||
CXXFLAGS="${CXXFLAGS} -m32"
|
||||
CFLAGS="${CFLAGS} -m32"
|
||||
;;
|
||||
*)
|
||||
echo "Unknown arch \"${TARGET_ARCH}\""
|
||||
exit 1
|
||||
esac
|
||||
|
||||
if [ "X${ASAN_BUILD}" = "X1" ]; then
|
||||
CXXFLAGS="${CXXFLAGS} -fsanitize=address -fno-omit-frame-pointer"
|
||||
CFLAGS="${CFLAGS} -fsanitize=address -fno-omit-frame-pointer"
|
||||
fi
|
||||
|
||||
if [ "X${UBSAN_BUILD}" = "X1" ]; then
|
||||
CXXFLAGS="${CXXFLAGS} -fsanitize=undefined"
|
||||
CFLAGS="${CFLAGS} -fsanitize=undefined"
|
||||
fi
|
||||
|
||||
# Report flags
|
||||
echo "CXXFLAGS: ${CXXFLAGS}"
|
||||
echo "CFLAGS: ${CFLAGS}"
|
||||
|
||||
# Report compiler
|
||||
echo "CC: ${CC}"
|
||||
${CC} --version
|
||||
echo "CXX: ${CXX}"
|
||||
${CXX} --version
|
||||
|
||||
# Export the values
|
||||
export CFLAGS
|
||||
export CXXFLAGS
|
||||
|
|
@ -1,20 +0,0 @@
|
|||
# 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"}
|
||||
: ${Z3_VERBOSE_BUILD_OUTPUT?"Z3_VERBOSE_BUILD_OUTPUT must be specified"}
|
||||
|
||||
GENERATOR_ARGS=('--')
|
||||
if [ "${Z3_CMAKE_GENERATOR}" = "Unix Makefiles" ]; then
|
||||
GENERATOR_ARGS+=("-j$(nproc)")
|
||||
if [ "X${Z3_VERBOSE_BUILD_OUTPUT}" = "X1" ]; then
|
||||
GENERATOR_ARGS+=("VERBOSE=1")
|
||||
fi
|
||||
elif [ "${Z3_CMAKE_GENERATOR}" = "Ninja" ]; then
|
||||
if [ "X${Z3_VERBOSE_BUILD_OUTPUT}" = "X1" ]; then
|
||||
GENERATOR_ARGS+=("-v")
|
||||
fi
|
||||
else
|
||||
echo "Unknown CMake generator \"${Z3_CMAKE_GENERATOR}\""
|
||||
exit 1
|
||||
fi
|
||||
|
|
@ -1,24 +0,0 @@
|
|||
#!/bin/bash
|
||||
|
||||
SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )"
|
||||
. ${SCRIPT_DIR}/run_quiet.sh
|
||||
|
||||
set -x
|
||||
set -e
|
||||
set -o pipefail
|
||||
|
||||
: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"}
|
||||
: ${BUILD_DOCS?"BUILD_DOCS must be specified"}
|
||||
|
||||
# Set CMake generator args
|
||||
source ${SCRIPT_DIR}/set_generator_args.sh
|
||||
|
||||
cd "${Z3_BUILD_DIR}"
|
||||
|
||||
# Generate documentation
|
||||
if [ "X${BUILD_DOCS}" = "X1" ]; then
|
||||
# TODO: Make quiet once we've fixed the build
|
||||
run_quiet cmake --build $(pwd) --target api_docs "${GENERATOR_ARGS[@]}"
|
||||
fi
|
||||
|
||||
# TODO: Test or perhaps deploy the built docs?
|
||||
|
|
@ -1,125 +0,0 @@
|
|||
#!/bin/bash
|
||||
|
||||
# This script tests Z3
|
||||
|
||||
SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )"
|
||||
. ${SCRIPT_DIR}/run_quiet.sh
|
||||
|
||||
set -x
|
||||
set -e
|
||||
set -o pipefail
|
||||
: ${Z3_SRC_DIR?"Z3_SRC_DIR must be specified"}
|
||||
: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"}
|
||||
: ${PYTHON_BINDINGS?"PYTHON_BINDINGS must be specified"}
|
||||
: ${PYTHON_EXECUTABLE?"PYTHON_EXECUTABLE must be specified"}
|
||||
: ${DOTNET_BINDINGS?"DOTNET_BINDINGS must be specified"}
|
||||
: ${JAVA_BINDINGS?"JAVA_BINDINGS must be specified"}
|
||||
: ${UBSAN_BUILD?"UBSAN_BUILD must be specified"}
|
||||
: ${RUN_API_EXAMPLES?"RUN_API_EXAMPLES must be specified"}
|
||||
|
||||
if [ "X${RUN_API_EXAMPLES}" = "X0" ]; then
|
||||
echo "Skipping run of API examples"
|
||||
exit 0
|
||||
fi
|
||||
|
||||
# Set compiler flags
|
||||
source ${SCRIPT_DIR}/set_compiler_flags.sh
|
||||
|
||||
# Set CMake generator args
|
||||
source ${SCRIPT_DIR}/set_generator_args.sh
|
||||
|
||||
# Sanitizer environment variables
|
||||
source ${SCRIPT_DIR}/sanitizer_env.sh
|
||||
|
||||
cd "${Z3_BUILD_DIR}"
|
||||
|
||||
# Build and run C example
|
||||
cmake --build $(pwd) --target c_example "${GENERATOR_ARGS[@]}"
|
||||
run_quiet examples/c_example_build_dir/c_example
|
||||
|
||||
# Build and run C++ example
|
||||
cmake --build $(pwd) --target cpp_example "${GENERATOR_ARGS[@]}"
|
||||
run_quiet examples/cpp_example_build_dir/cpp_example
|
||||
|
||||
# Build and run tptp5 example
|
||||
cmake --build $(pwd) --target z3_tptp5 "${GENERATOR_ARGS[@]}"
|
||||
# FIXME: Do something more useful with example
|
||||
run_quiet examples/tptp_build_dir/z3_tptp5 -help
|
||||
|
||||
# Build an run c_maxsat_example
|
||||
cmake --build $(pwd) --target c_maxsat_example "${GENERATOR_ARGS[@]}"
|
||||
# FIXME: It is known that the maxsat example leaks memory and the
|
||||
# the Z3 developers have stated this is "wontfix".
|
||||
# See https://github.com/Z3Prover/z3/issues/1299
|
||||
run_no_lsan \
|
||||
run_quiet \
|
||||
examples/c_maxsat_example_build_dir/c_maxsat_example \
|
||||
${Z3_SRC_DIR}/examples/maxsat/ex.smt
|
||||
|
||||
if [ "X${UBSAN_BUILD}" = "X1" ]; then
|
||||
# FIXME: We really need libz3 to link against a shared UBSan runtime.
|
||||
# Right now we link against the static runtime which breaks all the
|
||||
# non-native language bindings.
|
||||
echo "FIXME: Can't run other examples when building with UBSan"
|
||||
exit 0
|
||||
fi
|
||||
|
||||
|
||||
if [ "X${PYTHON_BINDINGS}" = "X1" ]; then
|
||||
# Run python examples
|
||||
# `all_interval_series.py` produces a lot of output so just throw
|
||||
# away output.
|
||||
# TODO: This example is slow should we remove it from testing?
|
||||
if [ "X${ASAN_BUILD}" = "X1" -a "X${Z3_BUILD_TYPE}" = "XDebug" ]; then
|
||||
# Too slow when doing ASan Debug build
|
||||
echo "Skipping all_interval_series.py under ASan Debug build"
|
||||
else
|
||||
run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/all_interval_series.py
|
||||
fi
|
||||
run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/complex.py
|
||||
run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/example.py
|
||||
# FIXME: `hamiltonian.py` example is disabled because its too slow.
|
||||
#${PYTHON_EXECUTABLE} python/hamiltonian.py
|
||||
run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/marco.py
|
||||
run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/mss.py
|
||||
run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/socrates.py
|
||||
run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/visitor.py
|
||||
run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/z3test.py
|
||||
fi
|
||||
|
||||
if [ "X${DOTNET_BINDINGS}" = "X1" ]; then
|
||||
# Run .NET example
|
||||
if [ "X${ASAN_BUILD}" = "X1" ]; then
|
||||
# The dotnet test get stuck on ASAN
|
||||
# so don't run it for now.
|
||||
echo "Skipping .NET example under ASan build"
|
||||
else
|
||||
run_quiet run_non_native_binding dotnet ${Z3_BUILD_DIR}/dotnet/netcoreapp2.0/dotnet.dll
|
||||
fi
|
||||
fi
|
||||
|
||||
if [ "X${JAVA_BINDINGS}" = "X1" ]; then
|
||||
# Build Java example
|
||||
# FIXME: Move compilation step into CMake target
|
||||
mkdir -p examples/java
|
||||
cp ${Z3_SRC_DIR}/examples/java/JavaExample.java examples/java/
|
||||
javac examples/java/JavaExample.java -classpath com.microsoft.z3.jar
|
||||
# Run Java example
|
||||
if [ "$(uname)" = "Darwin" ]; then
|
||||
# macOS
|
||||
export DYLD_LIBRARY_PATH=$(pwd):${DYLD_LIBRARY_PATH}
|
||||
else
|
||||
# Assume Linux for now
|
||||
export LD_LIBRARY_PATH=$(pwd):${LD_LIBRARY_PATH}
|
||||
fi
|
||||
if [ "X${ASAN_BUILD}" = "X1" ]; then
|
||||
# The JVM seems to crash (SEGV) if we pre-load ASan
|
||||
# so don't run it for now.
|
||||
echo "Skipping JavaExample under ASan build"
|
||||
else
|
||||
run_quiet \
|
||||
run_non_native_binding \
|
||||
java -cp .:examples/java:com.microsoft.z3.jar JavaExample
|
||||
fi
|
||||
fi
|
||||
|
||||
|
|
@ -1,24 +0,0 @@
|
|||
#!/bin/bash
|
||||
|
||||
SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )"
|
||||
|
||||
set -x
|
||||
set -e
|
||||
set -o pipefail
|
||||
|
||||
: ${TEST_INSTALL?"TEST_INSTALL must be specified"}
|
||||
: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"}
|
||||
|
||||
if [ "X${TEST_INSTALL}" != "X1" ]; then
|
||||
echo "Skipping install"
|
||||
exit 0
|
||||
fi
|
||||
|
||||
# Set CMake generator args
|
||||
source ${SCRIPT_DIR}/set_generator_args.sh
|
||||
|
||||
cd "${Z3_BUILD_DIR}"
|
||||
|
||||
sudo cmake --build $(pwd) --target install "${GENERATOR_ARGS[@]}"
|
||||
|
||||
# TODO: Test the installed version in some way
|
||||
|
|
@ -1,70 +0,0 @@
|
|||
#!/bin/bash
|
||||
|
||||
set -x
|
||||
set -e
|
||||
set -o pipefail
|
||||
|
||||
: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"}
|
||||
: ${Z3_BUILD_TYPE?"Z3_BUILD_TYPE must be specified"}
|
||||
: ${RUN_SYSTEM_TESTS?"RUN_SYSTEM_TESTS must be speicifed"}
|
||||
: ${PYTHON_BINDINGS?"PYTHON_BINDINGS must be specified"}
|
||||
: ${PYTHON_EXECUTABLE?"PYTHON_EXECUTABLE must be specified"}
|
||||
: ${Z3_SYSTEM_TEST_DIR?"Z3_SYSTEM_TEST_DIR must be specified"}
|
||||
: ${UBSAN_BUILD?"UBSAN_BUILD must be specified"}
|
||||
|
||||
if [ "X${RUN_SYSTEM_TESTS}" != "X1" ]; then
|
||||
echo "Skipping system tests"
|
||||
exit 0
|
||||
fi
|
||||
|
||||
# Sanitizer environment variables
|
||||
SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )"
|
||||
source ${SCRIPT_DIR}/sanitizer_env.sh
|
||||
|
||||
Z3_EXE="${Z3_BUILD_DIR}/z3"
|
||||
Z3_LIB_DIR="${Z3_BUILD_DIR}"
|
||||
|
||||
# Set value if not already defined externally
|
||||
Z3_SYSTEM_TEST_GIT_URL="${Z3_GIT_URL:-https://github.com/Z3Prover/z3test.git}"
|
||||
|
||||
# Clone repo to destination
|
||||
mkdir -p "${Z3_SYSTEM_TEST_DIR}"
|
||||
git clone "${Z3_SYSTEM_TEST_GIT_URL}" "${Z3_SYSTEM_TEST_DIR}"
|
||||
cd "${Z3_SYSTEM_TEST_DIR}"
|
||||
|
||||
if [ -n "${Z3_SYSTEM_TEST_GIT_REVISION}" ]; then
|
||||
# If a particular revision is requested then check it out.
|
||||
# This is useful for reproducible builds
|
||||
git checkout "${Z3_SYSTEM_TEST_GIT_REVISION}"
|
||||
fi
|
||||
|
||||
###############################################################################
|
||||
# Run system tests
|
||||
###############################################################################
|
||||
|
||||
# SMTLIBv2 tests
|
||||
${PYTHON_EXECUTABLE} scripts/test_benchmarks.py "${Z3_EXE}" regressions/smt2
|
||||
|
||||
${PYTHON_EXECUTABLE} scripts/test_benchmarks.py "${Z3_EXE}" regressions/smt2-extra
|
||||
|
||||
if [ "X${Z3_BUILD_TYPE}" = "XDebug" ]; then
|
||||
${PYTHON_EXECUTABLE} scripts/test_benchmarks.py "${Z3_EXE}" regressions/smt2-debug
|
||||
fi
|
||||
|
||||
if [ "X${PYTHON_BINDINGS}" = "X1" ]; then
|
||||
# Run python binding tests
|
||||
if [ "X${UBSAN_BUILD}" = "X1" ]; then
|
||||
# FIXME: We need to build libz3 with a shared UBSan runtime for the bindings
|
||||
# to work.
|
||||
echo "FIXME: Skipping python binding tests when building with UBSan"
|
||||
elif [ "X${ASAN_BUILD}" = "X1" ]; then
|
||||
# FIXME: The `test_pyscripts.py` doesn't propagate LD_PRELOAD
|
||||
# so under ASan the tests fail to run
|
||||
# to work.
|
||||
echo "FIXME: Skipping python binding tests when building with ASan"
|
||||
else
|
||||
run_non_native_binding ${PYTHON_EXECUTABLE} scripts/test_pyscripts.py "${Z3_LIB_DIR}" regressions/python/
|
||||
fi
|
||||
fi
|
||||
|
||||
# FIXME: Run `scripts/test_cs.py` once it has been modified to support mono
|
||||
|
|
@ -1,47 +0,0 @@
|
|||
#!/bin/bash
|
||||
|
||||
SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )"
|
||||
. ${SCRIPT_DIR}/run_quiet.sh
|
||||
|
||||
set -x
|
||||
set -e
|
||||
set -o pipefail
|
||||
|
||||
: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"}
|
||||
: ${RUN_UNIT_TESTS?"RUN_UNIT_TESTS must be specified"}
|
||||
|
||||
# Set CMake generator args
|
||||
source ${SCRIPT_DIR}/set_generator_args.sh
|
||||
|
||||
# Sanitizer environment variables
|
||||
source ${SCRIPT_DIR}/sanitizer_env.sh
|
||||
|
||||
cd "${Z3_BUILD_DIR}"
|
||||
|
||||
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
|
||||
|
|
@ -1,18 +0,0 @@
|
|||
#!/bin/bash
|
||||
|
||||
SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )"
|
||||
|
||||
set -x
|
||||
set -e
|
||||
set -o pipefail
|
||||
|
||||
: ${TRAVIS_OS_NAME?"TRAVIS_OS_NAME should be set"}
|
||||
|
||||
if [ "${TRAVIS_OS_NAME}" = "osx" ]; then
|
||||
${SCRIPT_DIR}/travis_ci_osx_entry_point.sh
|
||||
elif [ "${TRAVIS_OS_NAME}" = "linux" ]; then
|
||||
${SCRIPT_DIR}/travis_ci_linux_entry_point.sh
|
||||
else
|
||||
echo "Unsupported OS \"${TRAVIS_OS_NAME}\""
|
||||
exit 1
|
||||
fi
|
||||
|
|
@ -1,220 +0,0 @@
|
|||
#!/bin/bash
|
||||
|
||||
SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )"
|
||||
|
||||
set -x
|
||||
set -e
|
||||
set -o pipefail
|
||||
|
||||
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=()
|
||||
# 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
|
||||
|
||||
if [ -n "${Z3_USE_LIBGMP}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "Z3_USE_LIBGMP=${Z3_USE_LIBGMP}")
|
||||
fi
|
||||
|
||||
if [ -n "${BUILD_DOCS}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "BUILD_DOCS=${BUILD_DOCS}")
|
||||
fi
|
||||
|
||||
if [ -n "${PYTHON_EXECUTABLE}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "PYTHON_EXECUTABLE=${PYTHON_EXECUTABLE}")
|
||||
fi
|
||||
|
||||
if [ -n "${PYTHON_BINDINGS}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "PYTHON_BINDINGS=${PYTHON_BINDINGS}")
|
||||
fi
|
||||
|
||||
if [ -n "${DOTNET_BINDINGS}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "DOTNET_BINDINGS=${DOTNET_BINDINGS}")
|
||||
fi
|
||||
|
||||
if [ -n "${JAVA_BINDINGS}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "JAVA_BINDINGS=${JAVA_BINDINGS}")
|
||||
fi
|
||||
|
||||
if [ -n "${USE_LTO}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "USE_LTO=${USE_LTO}")
|
||||
fi
|
||||
|
||||
if [ -n "${Z3_INSTALL_PREFIX}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "Z3_INSTALL_PREFIX=${Z3_INSTALL_PREFIX}")
|
||||
fi
|
||||
|
||||
# TravisCI reserves CC for itself so use a different name
|
||||
if [ -n "${C_COMPILER}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "CC=${C_COMPILER}")
|
||||
fi
|
||||
|
||||
# TravisCI reserves CXX for itself so use a different name
|
||||
if [ -n "${CXX_COMPILER}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "CXX=${CXX_COMPILER}")
|
||||
fi
|
||||
|
||||
if [ -n "${TARGET_ARCH}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "TARGET_ARCH=${TARGET_ARCH}")
|
||||
fi
|
||||
|
||||
if [ -n "${ASAN_BUILD}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "ASAN_BUILD=${ASAN_BUILD}")
|
||||
fi
|
||||
|
||||
if [ -n "${ASAN_DSO}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "ASAN_DSO=${ASAN_DSO}")
|
||||
fi
|
||||
|
||||
if [ -n "${SANITIZER_PRINT_SUPPRESSIONS}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "SANITIZER_PRINT_SUPPRESSIONS=${SANITIZER_PRINT_SUPPRESSIONS}")
|
||||
fi
|
||||
|
||||
if [ -n "${UBSAN_BUILD}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "UBSAN_BUILD=${UBSAN_BUILD}")
|
||||
fi
|
||||
|
||||
if [ -n "${TEST_INSTALL}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "TEST_INSTALL=${TEST_INSTALL}")
|
||||
fi
|
||||
|
||||
if [ -n "${RUN_API_EXAMPLES}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "RUN_API_EXAMPLES=${RUN_API_EXAMPLES}")
|
||||
fi
|
||||
|
||||
if [ -n "${RUN_SYSTEM_TESTS}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "RUN_SYSTEM_TESTS=${RUN_SYSTEM_TESTS}")
|
||||
fi
|
||||
|
||||
if [ -n "${Z3_SYSTEM_TEST_GIT_REVISION}" ]; then
|
||||
BUILD_OPTS+=( \
|
||||
"--build-arg" \
|
||||
"Z3_SYSTEM_TEST_GIT_REVISION=${Z3_SYSTEM_TEST_GIT_REVISION}" \
|
||||
)
|
||||
fi
|
||||
|
||||
if [ -n "${RUN_UNIT_TESTS}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "RUN_UNIT_TESTS=${RUN_UNIT_TESTS}")
|
||||
fi
|
||||
|
||||
if [ -n "${Z3_VERBOSE_BUILD_OUTPUT}" ]; then
|
||||
BUILD_OPTS+=( \
|
||||
"--build-arg" \
|
||||
"Z3_VERBOSE_BUILD_OUTPUT=${Z3_VERBOSE_BUILD_OUTPUT}" \
|
||||
)
|
||||
fi
|
||||
|
||||
if [ -n "${Z3_STATIC_BUILD}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "Z3_STATIC_BUILD=${Z3_STATIC_BUILD}")
|
||||
fi
|
||||
|
||||
if [ -n "${NO_SUPPRESS_OUTPUT}" ]; then
|
||||
BUILD_OPTS+=( \
|
||||
"--build-arg" \
|
||||
"NO_SUPPRESS_OUTPUT=${NO_SUPPRESS_OUTPUT}" \
|
||||
)
|
||||
fi
|
||||
|
||||
if [ -n "${Z3_WARNINGS_AS_ERRORS}" ]; then
|
||||
BUILD_OPTS+=( \
|
||||
"--build-arg" \
|
||||
"Z3_WARNINGS_AS_ERRORS=${Z3_WARNINGS_AS_ERRORS}" \
|
||||
)
|
||||
fi
|
||||
|
||||
case ${LINUX_BASE} in
|
||||
ubuntu_20.04)
|
||||
BASE_DOCKER_FILE="${DOCKER_FILE_DIR}/z3_base_ubuntu_20.04.Dockerfile"
|
||||
BASE_DOCKER_IMAGE_NAME="z3_base_ubuntu:20.04"
|
||||
;;
|
||||
*)
|
||||
echo "Unknown Linux base ${LINUX_BASE}"
|
||||
exit 1
|
||||
;;
|
||||
esac
|
||||
|
||||
# Initially assume that we need to build the base Docker image
|
||||
MUST_BUILD=1
|
||||
|
||||
# Travis CI persistent cache.
|
||||
#
|
||||
# This inspired by http://rundef.com/fast-travis-ci-docker-build .
|
||||
# The idea is to cache the built image for subsequent builds to
|
||||
# reduce build time.
|
||||
if [ -n "${DOCKER_TRAVIS_CI_CACHE_DIR}" ]; then
|
||||
CHECKSUM_FILE="${DOCKER_TRAVIS_CI_CACHE_DIR}/${BASE_DOCKER_IMAGE_NAME}.chksum"
|
||||
CACHED_DOCKER_IMAGE="${DOCKER_TRAVIS_CI_CACHE_DIR}/${BASE_DOCKER_IMAGE_NAME}.gz"
|
||||
if [ -f "${CACHED_DOCKER_IMAGE}" ]; then
|
||||
# There's a cached image to use. Check the checksums of the Dockerfile
|
||||
# match. If they don't that implies we need to build a fresh image.
|
||||
if [ -f "${CHECKSUM_FILE}" ]; then
|
||||
CURRENT_DOCKERFILE_CHECKSUM=$(sha256sum "${BASE_DOCKER_FILE}" | awk '{ print $1 }')
|
||||
CACHED_DOCKERFILE_CHECKSUM=$(cat "${CHECKSUM_FILE}")
|
||||
if [ "X${CURRENT_DOCKERFILE_CHECKSUM}" = "X${CACHED_DOCKERFILE_CHECKSUM}" ]; then
|
||||
# Load the cached image
|
||||
MUST_BUILD=0
|
||||
gunzip --stdout "${CACHED_DOCKER_IMAGE}" | docker load
|
||||
fi
|
||||
fi
|
||||
fi
|
||||
fi
|
||||
|
||||
if [ "${MUST_BUILD}" -eq 1 ]; then
|
||||
# The base image contains all the dependencies we want to build
|
||||
# Z3.
|
||||
docker build -t "${BASE_DOCKER_IMAGE_NAME}" - < "${BASE_DOCKER_FILE}"
|
||||
|
||||
if [ -n "${DOCKER_TRAVIS_CI_CACHE_DIR}" ]; then
|
||||
# Write image and checksum to cache
|
||||
docker save "${BASE_DOCKER_IMAGE_NAME}" | \
|
||||
gzip > "${CACHED_DOCKER_IMAGE}"
|
||||
sha256sum "${BASE_DOCKER_FILE}" | awk '{ print $1 }' > \
|
||||
"${CHECKSUM_FILE}"
|
||||
fi
|
||||
fi
|
||||
|
||||
|
||||
DOCKER_MAJOR_VERSION=$(docker info --format '{{.ServerVersion}}' | sed 's/^\([0-9]\+\)\.\([0-9]\+\).*$/\1/')
|
||||
DOCKER_MINOR_VERSION=$(docker info --format '{{.ServerVersion}}' | sed 's/^\([0-9]\+\)\.\([0-9]\+\).*$/\2/')
|
||||
DOCKER_BUILD_FILE="${DOCKER_FILE_DIR}/z3_build.Dockerfile"
|
||||
|
||||
if [ "${DOCKER_MAJOR_VERSION}${DOCKER_MINOR_VERSION}" -lt 1705 ]; then
|
||||
# Workaround limitation in older Docker versions where the FROM
|
||||
# command cannot be parameterized with an ARG.
|
||||
sed \
|
||||
-e '/^ARG DOCKER_IMAGE_BASE/d' \
|
||||
-e 's/${DOCKER_IMAGE_BASE}/'"${BASE_DOCKER_IMAGE_NAME}/" \
|
||||
"${DOCKER_BUILD_FILE}" > "${DOCKER_BUILD_FILE}.patched"
|
||||
DOCKER_BUILD_FILE="${DOCKER_BUILD_FILE}.patched"
|
||||
else
|
||||
# This feature landed in Docker 17.05
|
||||
# See https://github.com/moby/moby/pull/31352
|
||||
BUILD_OPTS+=( \
|
||||
"--build-arg" \
|
||||
"DOCKER_IMAGE_BASE=${BASE_DOCKER_IMAGE_NAME}" \
|
||||
)
|
||||
fi
|
||||
|
||||
# Now build Z3 and test it using the created base image
|
||||
docker build \
|
||||
-f "${DOCKER_BUILD_FILE}" \
|
||||
"${BUILD_OPTS[@]}" \
|
||||
.
|
||||
|
|
@ -1,51 +0,0 @@
|
|||
#!/bin/bash
|
||||
|
||||
SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )"
|
||||
|
||||
set -x
|
||||
set -e
|
||||
set -o pipefail
|
||||
|
||||
# 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"
|
||||
exit 1
|
||||
fi
|
||||
|
||||
if [ ! -d "${TRAVIS_BUILD_DIR}" ]; then
|
||||
echo "TRAVIS_BUILD_DIR must be a directory"
|
||||
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_SYSTEM_TEST_DIR="${Z3_SRC_DIR}/z3_system_test"
|
||||
|
||||
# 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"
|
||||
Loading…
Reference in a new issue