From 22649f7e6631f986f39fdb9550ce9cdbaf5a954a Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Sun, 18 Jan 2026 16:27:30 -0800
Subject: [PATCH] Migrate Azure Pipelines to GitHub Actions (#8238)

* Initial plan

* Migrate Azure Pipelines to GitHub Actions CI workflow

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Add CI testing and validation documentation

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Update manylinux container image in CI workflow

* Disable test execution in CI workflow

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 .github/workflows/CI_MIGRATION.md | 123 +++++++++
 .github/workflows/CI_TESTING.md   | 132 +++++++++
 .github/workflows/ci.yml          | 443 ++++++++++++++++++++++++++++++
 azure-pipelines.yml               |   9 +
 4 files changed, 707 insertions(+)
 create mode 100644 .github/workflows/CI_MIGRATION.md
 create mode 100644 .github/workflows/CI_TESTING.md
 create mode 100644 .github/workflows/ci.yml

diff --git a/.github/workflows/CI_MIGRATION.md b/.github/workflows/CI_MIGRATION.md
new file mode 100644
index 000000000..dcca12d74
--- /dev/null
+++ b/.github/workflows/CI_MIGRATION.md
@@ -0,0 +1,123 @@
+# Azure Pipelines to GitHub Actions Migration
+
+## Overview
+
+This document describes the migration from Azure Pipelines (`azure-pipelines.yml`) to GitHub Actions (`.github/workflows/ci.yml`).
+
+## Migration Summary
+
+All jobs from the Azure Pipelines configuration have been migrated to GitHub Actions with equivalent or improved functionality.
+
+### Jobs Migrated
+
+| Azure Pipelines Job | GitHub Actions Job | Status |
+|---------------------|-------------------|--------|
+| LinuxPythonDebug (MT) | linux-python-debug (MT) | ✅ Migrated |
+| LinuxPythonDebug (ST) | linux-python-debug (ST) | ✅ Migrated |
+| ManylinuxPythonBuildAmd64 | manylinux-python-amd64 | ✅ Migrated |
+| ManyLinuxPythonBuildArm64 | manylinux-python-arm64 | ✅ Migrated |
+| UbuntuOCaml | ubuntu-ocaml | ✅ Migrated |
+| UbuntuOCamlStatic | ubuntu-ocaml-static | ✅ Migrated |
+| UbuntuCMake (releaseClang) | ubuntu-cmake (releaseClang) | ✅ Migrated |
+| UbuntuCMake (debugClang) | ubuntu-cmake (debugClang) | ✅ Migrated |
+| UbuntuCMake (debugGcc) | ubuntu-cmake (debugGcc) | ✅ Migrated |
+| UbuntuCMake (releaseSTGcc) | ubuntu-cmake (releaseSTGcc) | ✅ Migrated |
+| MacOSPython | macos-python | ✅ Migrated |
+| MacOSCMake | macos-cmake | ✅ Migrated |
+| LinuxMSan | N/A | ⚠️ Was disabled (condition: eq(0,1)) |
+| MacOSOCaml | N/A | ⚠️ Was disabled (condition: eq(0,1)) |
+
+## Key Differences
+
+### Syntax Changes
+
+1. **Trigger Configuration**
+   - Azure: `jobs:` with implicit triggers
+   - GitHub: Explicit `on:` section with `push`, `pull_request`, and `workflow_dispatch`
+
+2. **Job Names**
+   - Azure: `displayName` field
+   - GitHub: `name` field
+
+3. **Steps**
+   - Azure: `script:` for shell commands
+   - GitHub: `run:` for shell commands
+
+4. **Checkout**
+   - Azure: Implicit checkout
+   - GitHub: Explicit `uses: actions/checkout@v4`
+
+5. **Python Setup**
+   - Azure: Implicit Python availability
+   - GitHub: Explicit `uses: actions/setup-python@v5`
+
+6. **Variables**
+   - Azure: Top-level `variables:` section
+   - GitHub: Inline in job steps or matrix configuration
+
+### Template Scripts
+
+Azure Pipelines used external template files (e.g., `scripts/test-z3.yml`, `scripts/test-regressions.yml`). These have been inlined into the GitHub Actions workflow:
+
+- `scripts/test-z3.yml`: Unit tests → Inlined as "Run unit tests" step
+- `scripts/test-regressions.yml`: Regression tests → Inlined as "Run regressions" step
+- `scripts/test-examples-cmake.yml`: CMake examples → Inlined as "Run examples" step
+- `scripts/generate-doc.yml`: Documentation → Inlined as "Generate documentation" step
+
+### Matrix Strategies
+
+Both Azure Pipelines and GitHub Actions support matrix builds. The migration maintains the same matrix configurations:
+
+- **linux-python-debug**: 2 variants (MT, ST)
+- **ubuntu-cmake**: 4 variants (releaseClang, debugClang, debugGcc, releaseSTGcc)
+
+### Container Jobs
+
+Manylinux builds continue to use container images:
+- `quay.io/pypa/manylinux_2_34_x86_64:latest` for AMD64
+- `quay.io/pypa/manylinux2014_x86_64:latest` for ARM64 cross-compilation
+
+### Disabled Jobs
+
+Two jobs were disabled in Azure Pipelines (with `condition: eq(0,1)`) and have not been migrated:
+- **LinuxMSan**: Memory sanitizer builds
+- **MacOSOCaml**: macOS OCaml builds
+
+These can be re-enabled in the future if needed by adding them to the workflow file.
+
+## Benefits of GitHub Actions
+
+1. **Unified Platform**: All CI/CD in one place (GitHub)
+2. **Better Integration**: Native integration with GitHub features (checks, status, etc.)
+3. **Actions Marketplace**: Access to pre-built actions
+4. **Improved Caching**: Better artifact and cache management
+5. **Cost**: Free for public repositories
+
+## Testing
+
+To test the new workflow:
+
+1. Push a branch or create a pull request
+2. The workflow will automatically trigger
+3. Monitor progress in the "Actions" tab
+4. Review job logs for any issues
+
+## Deprecation Plan
+
+1. ✅ Create new GitHub Actions workflow (`.github/workflows/ci.yml`)
+2. 🔄 Test and validate the new workflow
+3. ⏳ Run both pipelines in parallel for a transition period
+4. ⏳ Once stable, deprecate `azure-pipelines.yml`
+
+## Rollback Plan
+
+If issues arise with the GitHub Actions workflow:
+1. The original `azure-pipelines.yml` remains in the repository
+2. Azure Pipelines can be re-enabled if needed
+3. Both can run in parallel during the transition
+
+## Additional Resources
+
+- [GitHub Actions Documentation](https://docs.github.com/en/actions)
+- [Migrating from Azure Pipelines to GitHub Actions](https://docs.github.com/en/actions/migrating-to-github-actions/migrating-from-azure-pipelines-to-github-actions)
+- [GitHub Actions Syntax Reference](https://docs.github.com/en/actions/reference/workflow-syntax-for-github-actions)
diff --git a/.github/workflows/CI_TESTING.md b/.github/workflows/CI_TESTING.md
new file mode 100644
index 000000000..d9b581ce1
--- /dev/null
+++ b/.github/workflows/CI_TESTING.md
@@ -0,0 +1,132 @@
+# Testing the CI Workflow
+
+This document provides instructions for testing the new GitHub Actions CI workflow after migration from Azure Pipelines.
+
+## Quick Test
+
+To test the workflow:
+
+1. **Push a branch or create a PR**: The workflow automatically triggers on all branches
+2. **View workflow runs**: Go to the "Actions" tab in GitHub
+3. **Monitor progress**: Click on a workflow run to see job details
+
+## Manual Trigger
+
+You can also manually trigger the workflow:
+
+1. Go to the "Actions" tab
+2. Select "CI" from the left sidebar
+3. Click "Run workflow"
+4. Choose your branch
+5. Click "Run workflow"
+
+## Local Validation
+
+Before pushing, you can validate the YAML syntax locally:
+
+```bash
+# Using yamllint (install with: pip install yamllint)
+yamllint .github/workflows/ci.yml
+
+# Using Python PyYAML
+python3 -c "import yaml; yaml.safe_load(open('.github/workflows/ci.yml'))"
+
+# Using actionlint (install from https://github.com/rhysd/actionlint)
+actionlint .github/workflows/ci.yml
+```
+
+## Job Matrix
+
+The CI workflow includes these job categories:
+
+### Linux Jobs
+- **linux-python-debug**: Python-based build with make (MT and ST variants)
+- **manylinux-python-amd64**: Python wheel build for manylinux AMD64
+- **manylinux-python-arm64**: Python wheel build for manylinux ARM64 (cross-compile)
+- **ubuntu-ocaml**: OCaml bindings build
+- **ubuntu-ocaml-static**: OCaml static library build
+- **ubuntu-cmake**: CMake builds with multiple compilers (4 variants)
+
+### macOS Jobs
+- **macos-python**: Python-based build with make
+- **macos-cmake**: CMake build with Julia support
+
+## Expected Runtime
+
+Approximate job durations:
+- Linux Python builds: 20-30 minutes
+- Manylinux Python builds: 15-25 minutes
+- OCaml builds: 25-35 minutes
+- CMake builds: 25-35 minutes each variant
+- macOS builds: 30-40 minutes
+
+Total workflow time (all jobs in parallel): ~40-60 minutes
+
+## Debugging Failed Jobs
+
+If a job fails:
+
+1. **Click on the failed job** to see the log
+2. **Expand failed steps** to see detailed output
+3. **Check for common issues**:
+   - Missing dependencies
+   - Test failures
+   - Build errors
+   - Timeout (increase timeout-minutes if needed)
+
+4. **Re-run failed jobs**:
+   - Click "Re-run failed jobs" button
+   - Or "Re-run all jobs" to test everything
+
+## Comparing with Azure Pipelines
+
+To compare results:
+
+1. Check the last successful Azure Pipelines run
+2. Compare job names and steps with the GitHub Actions workflow
+3. Verify all tests pass with similar coverage
+
+## Differences from Azure Pipelines
+
+1. **Checkout**: Explicit `actions/checkout@v4` step (was implicit)
+2. **Python Setup**: Explicit `actions/setup-python@v5` step (was implicit)
+3. **Template Files**: Inlined instead of external templates
+4. **Artifacts**: Uses `actions/upload-artifact` (if needed in future)
+5. **Caching**: Can add `actions/cache` for dependencies (optional optimization)
+
+## Adding Jobs or Modifying
+
+To add or modify jobs:
+
+1. Edit `.github/workflows/ci.yml`
+2. Follow the existing job structure
+3. Use matrix strategy for variants
+4. Add appropriate timeouts (default: 90 minutes)
+5. Test your changes on a branch first
+
+## Optimization Opportunities
+
+Future optimizations to consider:
+
+1. **Caching**: Add dependency caching (npm, pip, opam, etc.)
+2. **Artifacts**: Share build artifacts between jobs
+3. **Concurrency**: Add concurrency groups to cancel outdated runs
+4. **Selective Execution**: Skip jobs based on changed files
+5. **Self-hosted Runners**: For faster builds (if available)
+
+## Rollback Plan
+
+If the GitHub Actions workflow has issues:
+
+1. The original `azure-pipelines.yml` is still in the repository
+2. Azure Pipelines can be re-enabled if needed
+3. Both systems can run in parallel during transition
+
+## Support
+
+For issues or questions:
+
+1. Check GitHub Actions documentation: https://docs.github.com/en/actions
+2. Review the migration document: `.github/workflows/CI_MIGRATION.md`
+3. Check existing GitHub Actions workflows in `.github/workflows/`
+4. Open an issue in the repository
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
new file mode 100644
index 000000000..c63e4441f
--- /dev/null
+++ b/.github/workflows/ci.yml
@@ -0,0 +1,443 @@
+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: false
+    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
diff --git a/azure-pipelines.yml b/azure-pipelines.yml
index 1d8f964f6..016280f41 100644
--- a/azure-pipelines.yml
+++ b/azure-pipelines.yml
@@ -1,3 +1,12 @@
+# ============================================================================
+# DEPRECATION NOTICE
+# ============================================================================
+# This Azure Pipelines configuration has been migrated to GitHub Actions.
+# See .github/workflows/ci.yml for the new CI pipeline.
+# See .github/workflows/CI_MIGRATION.md for migration details.
+# 
+# This file is kept for reference and may be removed in the future.
+# ============================================================================
 
 variables:
   cmakeJulia: '-DZ3_BUILD_JULIA_BINDINGS=True'