variables: cmakeJulia: '-DZ3_BUILD_JULIA_BINDINGS=True' cmakeJava: '-DZ3_BUILD_JAVA_BINDINGS=True' cmakeNet: '-DZ3_BUILD_DOTNET_BINDINGS=True' cmakePy: '-DZ3_BUILD_PYTHON_BINDINGS=True' cmakeStdArgs: '-DZ3_BUILD_DOTNET_BINDINGS=True -DZ3_BUILD_JAVA_BINDINGS=True -DZ3_BUILD_PYTHON_BINDINGS=True -G "Ninja" ../' asanEnv: 'CXXFLAGS="${CXXFLAGS} -fsanitize=address -fno-omit-frame-pointer" CFLAGS="${CFLAGS} -fsanitize=address -fno-omit-frame-pointer"' ubsanEnv: 'CXXFLAGS="${CXXFLAGS} -fsanitize=undefined" CFLAGS="${CFLAGS} -fsanitize=undefined"' msanEnv: 'CC=clang LDFLAGS="-L../libcxx/libcxx_msan/lib -lc++abi -Wl,-rpath=../libcxx/libcxx_msan/lib" CXX=clang++ CXXFLAGS="${CXXFLAGS} -stdlib=libc++ -fsanitize-memory-track-origins -fsanitize=memory -fPIE -fno-omit-frame-pointer -g -O2" CFLAGS="${CFLAGS} -stdlib=libc -fsanitize=memory -fsanitize-memory-track-origins -fno-omit-frame-pointer -g -O2"' # TBD: # test python bindings # build documentation # Asan, ubsan, msan # Disabled pending clang dependencies for std::unordered_map jobs: - job: "LinuxPythonDebug" displayName: "Ubuntu build - python make - debug" pool: vmImage: "Ubuntu-latest" strategy: matrix: MT: cmdLine: 'python scripts/mk_make.py -d --java --dotnet' runRegressions: 'True' ST: cmdLine: './configure --single-threaded' runRegressions: 'False' steps: - script: $(cmdLine) - script: | set -e cd build make -j3 make -j3 examples make -j3 test-z3 cd .. - template: scripts/test-z3.yml - ${{if eq(variables['runRegressions'], 'True')}}: - template: scripts/test-regressions.yml - job: "Ubuntu18Python" displayName: "Ubuntu 18 with ocaml" pool: vmImage: "Ubuntu-18.04" steps: - script: sudo apt-get install ocaml opam libgmp-dev - script: opam init -y - script: eval `opam config env`; opam install zarith ocamlfind -y - script: python scripts/mk_make.py --ml --staticlib - script: | set -e cd build eval `opam config env` make -j3 make -j3 examples make -j3 test-z3 ./ml_example cd .. - template: scripts/test-z3.yml - template: scripts/test-regressions.yml - template: scripts/generate-doc.yml - job: "LinuxMSan" displayName: "Ubuntu build - cmake" condition: eq(0,1) pool: vmImage: "Ubuntu-latest" strategy: matrix: msanClang: cmdLine: '$(msanEnv) cmake $(cmakeStdArgs)' runUnitTest: 'True' runExample: 'False' # Examples don't seem to build with MSAN steps: - script: sudo apt-get install ninja-build libc++-dev libc++abi-dev - script: ./scripts/build_libcxx_msan.sh - script: | set -e mkdir build cd build $(cmdLine) ninja ninja test-z3 cd .. - script: | cd build export MSAN_SYMBOLIZER_PATH=/usr/lib/llvm-6.0/bin/llvm-symbolizer ./test-z3 -a cd .. condition: eq(variables['runUnitTest'], 'True') - ${{if eq(variables['runExample'], 'True')}}: - template: scripts/test-examples-cmake.yml # - template: scripts/test-jupyter.yml # - template: scripts/test-java-cmake.yml # - template: scripts/test-regressions.yml - job: "Ubuntu16CMake" displayName: "Ubuntu build - cmake" pool: vmImage: "Ubuntu-latest" strategy: matrix: releaseClang: setupCmd1: '' setupCmd2: '' buildCmd: 'CC=clang CXX=clang++ cmake -DCMAKE_BUILD_TYPE=Release $(cmakeStdArgs)' runTests: 'True' debugClang: setupCmd1: 'julia -e "using Pkg; Pkg.add(PackageSpec(name=\"libcxxwrap_julia_jll\", version=\"0.7.0\"))"' setupCmd2: 'JlCxxDir=$(julia -e "using libcxxwrap_julia_jll; print(dirname(libcxxwrap_julia_jll.libcxxwrap_julia_path))")' buildCmd: 'CC=clang CXX=clang++ cmake -DJlCxx_DIR=$JlCxxDir/cmake/JlCxx $(cmakeJulia) $(cmakeStdArgs)' runTests: 'True' debugGcc: setupCmd1: '' setupCmd2: '' buildCmd: 'CC=gcc CXX=g++ cmake $(cmakeStdArgs)' runTests: 'True' releaseSTGcc: setupCmd1: '' setupCmd2: '' buildCmd: 'CC=gcc CXX=g++ cmake -DCMAKE_BUILD_TYPE=Release -DZ3_SINGLE_THREADED=ON $(cmakeStdArgs)' runTests: 'True' steps: - script: sudo apt-get install ninja-build - script: | set -e mkdir build cd build $(setupCmd1) $(setupCmd2) $(buildCmd) ninja ninja test-z3 cd .. - script: | cd build ./test-z3 -a cd .. condition: eq(variables['runTests'], 'True') - ${{if eq(variables['runTests'], 'True')}}: - template: scripts/test-examples-cmake.yml # - template: scripts/test-jupyter.yml # - template: scripts/test-java-cmake.yml - ${{if eq(variables['runTests'], 'True')}}: - template: scripts/test-regressions.yml - job: "WindowsLatest" displayName: "Windows" pool: vmImage: "windows-latest" strategy: matrix: x86: arch: 'x86' setupCmd1: '' setupCmd2: '' setupCmd3: '' bindings: '$(cmakePy)' runTests: 'False' x64: arch: 'x64' setupCmd1: 'julia -e "using Pkg; Pkg.add(PackageSpec(name=\"libcxxwrap_julia_jll\", version=\"0.7.0\"))"' setupCmd2: 'julia -e "using libcxxwrap_julia_jll; print(dirname(libcxxwrap_julia_jll.libcxxwrap_julia_path))" > tmp.env' setupCmd3: 'set /P JlCxxDir=<tmp.env' bindings: '-DJlCxx_DIR=%JlCxxDir%\..\lib\cmake\JlCxx $(cmakeJava) $(cmakeNet) $(cmakePy) -DCMAKE_BUILD_TYPE=RelWithDebInfo' runTests: 'True' arm64: arch: 'amd64_arm64' setupCmd1: '' setupCmd2: '' setupCmd3: '' bindings: '' runTests: 'False' steps: - script: md build - script: | cd build $(setupCmd1) $(setupCmd2) $(setupCmd3) call "C:\Program Files (x86)\Microsoft Visual Studio\2019\Enterprise\VC\Auxiliary\Build\vcvarsall.bat" $(arch) cmake $(bindings) -G "NMake Makefiles" ../ nmake cd .. - script: | call "C:\Program Files (x86)\Microsoft Visual Studio\2019\Enterprise\VC\Auxiliary\Build\vcvarsall.bat" $(arch) pushd build\python python z3test.py z3 python z3test.py z3num popd pushd build nmake cpp_example examples\cpp_example_build_dir\cpp_example.exe nmake c_example examples\c_example_build_dir\c_example.exe nmake test-z3 test-z3.exe -a popd condition: eq(variables['runTests'], 'True') - script: | git clone https://github.com/z3prover/z3test z3test python z3test\scripts\test_benchmarks.py build\z3.exe z3test\regressions\smt2 condition: eq(variables['runTests'], 'True') - job: "MacOSPython" displayName: "MacOS build" pool: vmImage: "macOS-latest" steps: - script: python scripts/mk_make.py -d --java --dotnet - script: | set -e cd build make -j3 make -j3 examples make -j3 test-z3 ./cpp_example ./c_example ./java_example ./dotnet_example cd .. # Skip as dead-slow in debug mode: # - template: scripts/test-z3.yml - template: scripts/test-regressions.yml - job: "MacOSCMake" displayName: "MacOS build with CMake" pool: vmImage: "macOS-latest" steps: - script: brew install ninja # - script: brew install --cask julia - script: | julia -e "using Pkg; Pkg.add(PackageSpec(name=\"libcxxwrap_julia_jll\", version=\"0.7.0\"))" JlCxxDir=$(julia -e "using libcxxwrap_julia_jll; println(joinpath(dirname(libcxxwrap_julia_jll.libcxxwrap_julia_path), \"cmake\", \"JlCxx\"))") set -e mkdir build cd build cmake -DJlCxx_DIR=$JlCxxDir $(cmakeJulia) $(cmakeJava) $(cmakePy) -DZ3_BUILD_DOTNET_BINDINGS=False -G "Ninja" ../ ninja ninja test-z3 cd .. - template: scripts/test-z3.yml # - template: scripts/test-examples-cmake.yml - template: scripts/test-regressions.yml # - template: scripts/test-java-cmake.yml