mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-20 17:14:43 +00:00
Code Activity
z3/.github/workflows/ci.yml
Nikolaj Bjorner d0d4ba3646
Update manylinux container image in CI workflow
2026-01-18 13:15:16 -08:00

443 lines
13 KiB
YAML
Raw Blame History

name: CI
on:
push:
branches: [ "**" ]
pull_request:
branches: [ "**" ]
workflow_dispatch:
permissions:
contents: read
# This workflow migrates jobs from azure-pipelines.yml to GitHub Actions.
# See .github/workflows/CI_MIGRATION.md for details on the migration.
jobs:
# ============================================================================
# Linux Python Debug Builds
# ============================================================================
linux-python-debug:
name: "Ubuntu build - python make - ${{ matrix.variant }}"
runs-on: ubuntu-latest
timeout-minutes: 90
strategy:
fail-fast: false
matrix:
variant: [MT, ST]
include:
- variant: MT
cmdLine: 'python scripts/mk_make.py -d --java --dotnet'
runRegressions: true
- variant: ST
cmdLine: './configure --single-threaded'
runRegressions: false
steps:
- name: Checkout code
uses: actions/checkout@v4
- name: Setup Python
uses: actions/setup-python@v5
with:
python-version: '3.x'
- name: Configure
run: ${{ matrix.cmdLine }}
- name: Build
run: |
set -e
cd build
make -j3
make -j3 examples
make -j3 test-z3
cd ..
- name: Run unit tests
run: |
cd build
./test-z3 -a
cd ..
- name: Clone z3test
if: matrix.runRegressions
run: git clone https://github.com/z3prover/z3test z3test
- name: Run regressions
if: matrix.runRegressions
run: python z3test/scripts/test_benchmarks.py build/z3 z3test/regressions/smt2
# ============================================================================
# Manylinux Python Builds
# ============================================================================
manylinux-python-amd64:
name: "Python bindings (manylinux Centos AMD64) build"
runs-on: ubuntu-latest
timeout-minutes: 90
container: "quay.io/pypa/manylinux_2_34_x86_64:latest"
steps:
- name: Checkout code
uses: actions/checkout@v4
- name: Setup Python virtual environment
run: "/opt/python/cp38-cp38/bin/python -m venv $PWD/env"
- name: Install build dependencies
run: |
source $PWD/env/bin/activate
pip install build git+https://github.com/rhelmot/auditwheel
- name: Build Python wheel
run: |
source $PWD/env/bin/activate
cd src/api/python
python -m build
AUDITWHEEL_PLAT= auditwheel repair --best-plat dist/*.whl
cd ../../..
- name: Test Python wheel
run: |
source $PWD/env/bin/activate
pip install ./src/api/python/wheelhouse/*.whl
python - <src/api/python/z3test.py z3
python - <src/api/python/z3test.py z3num
manylinux-python-arm64:
name: "Python bindings (manylinux Centos ARM64 cross) build"
runs-on: ubuntu-latest
timeout-minutes: 90
container: quay.io/pypa/manylinux_2_28_x86_64:latest
steps:
- name: Checkout code
uses: actions/checkout@v4
- name: Download ARM toolchain
run: curl -L -o /tmp/arm-toolchain.tar.xz 'https://developer.arm.com/-/media/Files/downloads/gnu/13.3.rel1/binrel/arm-gnu-toolchain-13.3.rel1-x86_64-aarch64-none-linux-gnu.tar.xz'
- name: Extract ARM toolchain
run: |
mkdir -p /tmp/arm-toolchain/
tar xf /tmp/arm-toolchain.tar.xz -C /tmp/arm-toolchain/ --strip-components=1
- name: Setup Python virtual environment
run: "/opt/python/cp38-cp38/bin/python -m venv $PWD/env"
- name: Install build dependencies
run: |
source $PWD/env/bin/activate
pip install build git+https://github.com/rhelmot/auditwheel
- name: Build Python wheel (cross-compile)
run: |
source $PWD/env/bin/activate
export PATH="/tmp/arm-toolchain/bin:/tmp/arm-toolchain/aarch64-none-linux-gnu/libc/usr/bin:$PATH"
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 ../../..
# ============================================================================
# Ubuntu OCaml Builds
# ============================================================================
ubuntu-ocaml:
name: "Ubuntu with OCaml"
runs-on: ubuntu-latest
timeout-minutes: 90
steps:
- name: Checkout code
uses: actions/checkout@v4
- name: Setup OCaml
uses: ocaml/setup-ocaml@v3
with:
ocaml-compiler: '5'
opam-disable-sandboxing: true
- name: Install system dependencies
run: sudo apt-get update && sudo apt-get install -y libgmp-dev
- name: Install OCaml dependencies
run: opam install zarith ocamlfind -y
- name: Configure
run: eval `opam config env`; python scripts/mk_make.py --ml
- name: Build
run: |
set -e
cd build
eval `opam config env`
make -j3
make -j3 examples
make -j3 test-z3
cd ..
- name: Install Z3 OCaml package
run: eval `opam config env`; ocamlfind install z3 build/api/ml/* -dll build/libz3.*
- name: Run unit tests
run: |
cd build
./test-z3 -a
cd ..
- name: Clone z3test
run: git clone https://github.com/z3prover/z3test z3test
- name: Run regressions
run: python z3test/scripts/test_benchmarks.py build/z3 z3test/regressions/smt2
- name: Generate documentation
run: |
cd doc
sudo apt-get install -y doxygen graphviz
python mk_api_doc.py --z3py-package-path=../build/python/z3
cd ..
ubuntu-ocaml-static:
name: "Ubuntu with OCaml on z3-static"
runs-on: ubuntu-latest
timeout-minutes: 90
steps:
- name: Checkout code
uses: actions/checkout@v4
- name: Setup OCaml
uses: ocaml/setup-ocaml@v3
with:
ocaml-compiler: '5'
opam-disable-sandboxing: true
- name: Install system dependencies
run: sudo apt-get update && sudo apt-get install -y libgmp-dev
- name: Install OCaml dependencies
run: opam install zarith ocamlfind -y
- name: Configure
run: eval `opam config env`; python scripts/mk_make.py --ml --staticlib
- name: Build
run: |
set -e
cd build
eval `opam config env`
make -j3
make -j3 examples
make -j3 test-z3
cd ..
- name: Install Z3 OCaml package
run: eval `opam config env`; ocamlfind install z3-static build/api/ml/* build/libz3-static.a
- name: Build and run OCaml examples
run: |
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 ..
- name: Run unit tests
run: |
cd build
./test-z3 -a
cd ..
- name: Clone z3test
run: git clone https://github.com/z3prover/z3test z3test
- name: Run regressions
run: python z3test/scripts/test_benchmarks.py build/z3 z3test/regressions/smt2
- name: Generate documentation
run: |
cd doc
sudo apt-get install -y doxygen graphviz
python mk_api_doc.py --z3py-package-path=../build/python/z3
cd ..
# ============================================================================
# Ubuntu CMake Builds
# ============================================================================
ubuntu-cmake:
name: "Ubuntu build - cmake - ${{ matrix.name }}"
runs-on: ubuntu-latest
timeout-minutes: 90
strategy:
fail-fast: false
matrix:
include:
- name: releaseClang
setupCmd1: ''
setupCmd2: ''
buildCmd: 'CC=clang CXX=clang++ cmake -DCMAKE_BUILD_TYPE=Release -DZ3_BUILD_DOTNET_BINDINGS=True -DZ3_BUILD_JAVA_BINDINGS=True -DZ3_BUILD_PYTHON_BINDINGS=True -G "Ninja" ../'
runTests: true
- name: 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 -DZ3_BUILD_JULIA_BINDINGS=True -DZ3_BUILD_DOTNET_BINDINGS=True -DZ3_BUILD_JAVA_BINDINGS=True -DZ3_BUILD_PYTHON_BINDINGS=True -G "Ninja" ../'
runTests: true
- name: debugGcc
setupCmd1: ''
setupCmd2: ''
buildCmd: 'CC=gcc CXX=g++ cmake -DZ3_BUILD_DOTNET_BINDINGS=True -DZ3_BUILD_JAVA_BINDINGS=True -DZ3_BUILD_PYTHON_BINDINGS=True -G "Ninja" ../'
runTests: true
- name: releaseSTGcc
setupCmd1: ''
setupCmd2: ''
buildCmd: 'CC=gcc CXX=g++ cmake -DCMAKE_BUILD_TYPE=Release -DZ3_SINGLE_THREADED=ON -DZ3_BUILD_DOTNET_BINDINGS=True -DZ3_BUILD_JAVA_BINDINGS=True -DZ3_BUILD_PYTHON_BINDINGS=True -G "Ninja" ../'
runTests: true
steps:
- name: Checkout code
uses: actions/checkout@v4
- name: Setup Python
uses: actions/setup-python@v5
with:
python-version: '3.x'
- name: Install Ninja
run: sudo apt-get update && sudo apt-get install -y ninja-build
- name: Setup Julia (if needed)
if: matrix.name == 'debugClang'
uses: julia-actions/setup-julia@v2
with:
version: '1'
- name: Configure
run: |
set -e
mkdir build
cd build
${{ matrix.setupCmd1 }}
${{ matrix.setupCmd2 }}
${{ matrix.buildCmd }}
- name: Build
run: |
cd build
ninja
ninja test-z3
cd ..
- name: Run unit tests
if: matrix.runTests
run: |
cd build
./test-z3 -a
cd ..
- name: Run examples
if: matrix.runTests
run: |
set -e
cd build
ninja c_example
ninja cpp_example
ninja z3_tptp5
ninja c_maxsat_example
examples/c_example_build_dir/c_example
examples/cpp_example_build_dir/cpp_example
examples/tptp_build_dir/z3_tptp5 -help
examples/c_maxsat_example_build_dir/c_maxsat_example ../examples/maxsat/ex.smt
cd ..
- name: Clone z3test
if: matrix.runTests
run: git clone https://github.com/z3prover/z3test z3test
- name: Run regressions
if: matrix.runTests
run: python z3test/scripts/test_benchmarks.py build/z3 z3test/regressions/smt2
# ============================================================================
# macOS Python Builds
# ============================================================================
macos-python:
name: "MacOS build"
runs-on: macos-latest
timeout-minutes: 90
steps:
- name: Checkout code
uses: actions/checkout@v4
- name: Setup Python
uses: actions/setup-python@v5
with:
python-version: '3.x'
- name: Configure
run: python scripts/mk_make.py -d --java --dotnet
- name: Build
run: |
set -e
cd build
make -j3
make -j3 examples
make -j3 test-z3
./cpp_example
./c_example
cd ..
- name: Clone z3test
run: git clone https://github.com/z3prover/z3test z3test
- name: Run regressions
run: python z3test/scripts/test_benchmarks.py build/z3 z3test/regressions/smt2
# ============================================================================
# macOS CMake Builds
# ============================================================================
macos-cmake:
name: "MacOS build with CMake"
runs-on: macos-latest
timeout-minutes: 90
steps:
- name: Checkout code
uses: actions/checkout@v4
- name: Setup Python
uses: actions/setup-python@v5
with:
python-version: '3.x'
- name: Install dependencies
run: |
brew install ninja
brew install --cask julia
- name: Configure
run: |
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 -DZ3_BUILD_JULIA_BINDINGS=True -DZ3_BUILD_JAVA_BINDINGS=True -DZ3_BUILD_PYTHON_BINDINGS=True -DZ3_BUILD_DOTNET_BINDINGS=False -G "Ninja" ../
cd ..
- name: Build
run: |
cd build
ninja
ninja test-z3
cd ..
- name: Run unit tests
run: |
cd build
./test-z3 -a
cd ..
- name: Clone z3test
run: git clone https://github.com/z3prover/z3test z3test
- name: Run regressions
run: python z3test/scripts/test_benchmarks.py build/z3 z3test/regressions/smt2
View git blame Copy permalink