z3/azure-pipelines.yml

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"
  timeoutInMinutes: 90  
  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: "ManylinuxPythonBuildAmd64"
  displayName: "Python bindings (manylinux Centos AMD64) build"
  timeoutInMinutes: 90  
  pool:
    vmImage: "ubuntu-latest"
  container: "quay.io/pypa/manylinux2014_x86_64:latest"
  steps:
  - script: "/opt/python/cp38-cp38/bin/python -m venv $PWD/env"
  - script: 'echo "##vso[task.prependpath]$PWD/env/bin"'
  - script: "pip install build git+https://github.com/rhelmot/auditwheel"
  - script: "cd src/api/python && python -m build && AUDITWHEEL_PLAT= auditwheel repair --best-plat dist/*.whl && cd ../../.."
  - script: "pip install ./src/api/python/wheelhouse/*.whl && python - <src/api/python/z3test.py z3 && python - <src/api/python/z3test.py z3num"

- job: ManyLinuxPythonBuildArm64
  timeoutInMinutes: 90
  displayName: "Python bindings (manylinux Centos ARM64 cross) build"
  variables:
    name: ManyLinux
    python: "/opt/python/cp37-cp37m/bin/python"
  pool:
    vmImage: "ubuntu-latest"
  container: "quay.io/pypa/manylinux2014_x86_64:latest"
  steps:
  - script: curl -L -o /tmp/arm-toolchain.tar.xz 'https://developer.arm.com/-/media/Files/downloads/gnu/11.2-2022.02/binrel/gcc-arm-11.2-2022.02-x86_64-aarch64-none-linux-gnu.tar.xz?rev=33c6e30e5ac64e6dba8f0431f2c35f1b&hash=9918A05BF47621B632C7A5C8D2BB438FB80A4480'
  - script: mkdir -p /tmp/arm-toolchain/
  - script: tar xf /tmp/arm-toolchain.tar.xz -C /tmp/arm-toolchain/ --strip-components=1
  - script: "/opt/python/cp38-cp38/bin/python -m venv $PWD/env"
  - script: 'echo "##vso[task.prependpath]$PWD/env/bin"'
  - script: echo '##vso[task.prependpath]/tmp/arm-toolchain/bin'
  - script: echo '##vso[task.prependpath]/tmp/arm-toolchain/aarch64-none-linux-gnu/libc/usr/bin'
  - script: echo $PATH
  - script: "stat `which aarch64-none-linux-gnu-gcc`"
  - script: "pip install build git+https://github.com/rhelmot/auditwheel"
  - script: "cd src/api/python && CC=aarch64-none-linux-gnu-gcc CXX=aarch64-none-linux-gnu-g++ AR=aarch64-none-linux-gnu-ar LD=aarch64-none-linux-gnu-ld python -m build && AUDITWHEEL_PLAT= auditwheel repair --best-plat dist/*.whl && cd ../../.."

- job: "UbuntuOCaml"
  displayName: "Ubuntu with OCaml"
  timeoutInMinutes: 90  
  pool:
    vmImage: "Ubuntu-latest"
  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: eval `opam config env`; python scripts/mk_make.py --ml
    - script: |
        set -e
        cd build
        eval `opam config env`
        make -j3
        make -j3 examples
        make -j3 test-z3
        cd ..
    - script: eval `opam config env`; ocamlfind install z3 build/api/ml/* -dll build/libz3.*
    - template: scripts/test-z3.yml
    - template: scripts/test-regressions.yml
    - template: scripts/generate-doc.yml


- job: "UbuntuOCamlStatic"
  displayName: "Ubuntu with OCaml on z3-static"
  timeoutInMinutes: 90  
  pool:
    vmImage: "Ubuntu-latest"
  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: eval `opam config env`; 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
        cd ..
    - script: eval `opam config env`; ocamlfind install z3-static build/api/ml/* build/libz3-static.a
    - script: |
        set -e
        cd build
        eval `opam config env`
        make -j3
        make -j3 _ex_ml_example_post_install
        ./ml_example_static.byte
        ./ml_example_static_custom.byte
        ./ml_example_static
        cd ..
    - template: scripts/test-z3.yml
    - template: scripts/test-regressions.yml
    - template: scripts/generate-doc.yml

- job: "LinuxMSan"
  displayName: "Ubuntu build - cmake"
  timeoutInMinutes: 90
  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: "UbuntuCMake"
  displayName: "Ubuntu build - cmake"
  timeoutInMinutes: 90
  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\"))"'
        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: "MacOSPython"
  displayName: "MacOS build"
  timeoutInMinutes: 90  
  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 -cp api/java/classes; JavaExample
        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"
  timeoutInMinutes: 90  
  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\"))"
        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


- job: "MacOSOCaml"
  displayName: "MacOS build with OCaml"
  timeoutInMinutes: 90  
  condition: eq(0,1) 
  pool:
    vmImage: "macOS-latest"
  steps:
    - script: brew install opam
    - script: opam init -y
    - script: eval `opam config env`; opam install zarith ocamlfind -y
    - script: eval `opam config env`; python scripts/mk_make.py --ml
    - script: |
        set -e
        cd build
        eval `opam config env`
        make -j3
        make -j3 examples
        make -j3 test-z3
        cd ..
    - script: eval `opam config env`; ocamlfind install z3 build/api/ml/* -dll build/libz3.*
    - script: |
        set -e
        cd build
        eval `opam config env`
        make -j3
        make -j3 _ex_ml_example_post_install
        # ./ml_example_shared.byte
        # ./ml_example_shared_custom.byte
        # ./ml_example_shared
        cd ..
# Skip as dead-slow in debug mode:
#  - template: scripts/test-z3.yml
    - template: scripts/test-regressions.yml