From 04ec450b024053292d2d5493e0c761a95378b938 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Sun, 1 Feb 2026 16:49:41 -0800 Subject: [PATCH] Add workflow to build and cache Z3 for reuse across CI (#8466) * Initial plan * Add Z3 build cache workflow and documentation Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Address code review feedback: improve cache strategy and documentation Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Fix cache restore-keys and update size documentation Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Delete .github/workflows/example-cached-z3.yml --------- 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 --- .github/workflows/README-build-cache.md | 222 ++++++++++++++++++++++++ .github/workflows/build-z3-cache.yml | 79 +++++++++ 2 files changed, 301 insertions(+) create mode 100644 .github/workflows/README-build-cache.md create mode 100644 .github/workflows/build-z3-cache.yml diff --git a/.github/workflows/README-build-cache.md b/.github/workflows/README-build-cache.md new file mode 100644 index 000000000..5c310c5c6 --- /dev/null +++ b/.github/workflows/README-build-cache.md @@ -0,0 +1,222 @@ +# Z3 Build Cache Workflow + +This workflow builds Z3 and caches the built binaries for use by other workflows, eliminating the need for repeated builds and saving significant CI time. + +## Purpose + +The `build-z3-cache.yml` workflow: +1. Builds Z3 from source using the Python build system +2. Caches the built binaries and libraries +3. Can be triggered manually, on schedule, or on pushes to main +4. Can be called as a reusable workflow from other workflows + +## Cache Contents + +The workflow caches: +- `build/z3` - Main Z3 executable +- `build/libz3.so` and `build/libz3.a` - Z3 libraries +- `build/*.so` and `build/*.a` - Additional library files +- `build/python` - Python bindings + +## Cache Key Format + +The cache key is: `z3-build-{OS}-{git-sha}` + +**How it works:** +- Each commit gets its own cache entry based on its git SHA +- When restoring, the `restore-keys` pattern allows falling back to caches from previous commits +- The most recent cache matching the `restore-keys` pattern will be used if an exact key match isn't found +- This means workflows typically restore from a recent build and save a new cache for the current commit + +**Example:** +- A workflow on commit `abc123` will look for `z3-build-Linux-abc123` +- If not found, it falls back to the most recent `z3-build-Linux-*` cache +- After building, it saves a new cache with key `z3-build-Linux-abc123` + +This ensures: +- Caches are OS-specific +- Each new commit can reuse builds from recent commits +- The cache stays relatively up-to-date with the repository + +## Using the Cached Build + +### Option 1: Direct Cache Restore (Recommended) + +Add these steps to your workflow before you need to use Z3: + +```yaml +- name: Checkout code + uses: actions/checkout@v6 + +- name: Setup Python + uses: actions/setup-python@v6 + with: + python-version: '3.x' + +- name: Restore Z3 cache + id: cache-z3 + uses: actions/cache/restore@v4 + with: + path: | + build/z3 + build/libz3.so + build/libz3.a + build/*.so + build/*.a + build/python + key: z3-build-${{ runner.os }}-${{ github.sha }} + restore-keys: | + z3-build-${{ runner.os }}- + +- name: Build Z3 (if not cached) + if: steps.cache-z3.outputs.cache-hit != 'true' + run: | + python scripts/mk_make.py + cd build + make -j$(nproc) + +- name: Verify Z3 is available + run: | + build/z3 --version +``` + +### Option 2: Call as Reusable Workflow + +You can also call this workflow before your job: + +```yaml +jobs: + build-cache: + uses: ./.github/workflows/build-z3-cache.yml + + your-job: + needs: build-cache + runs-on: ubuntu-latest + steps: + - name: Checkout code + uses: actions/checkout@v6 + + - name: Restore Z3 cache + uses: actions/cache/restore@v4 + with: + path: | + build/z3 + build/libz3.so + build/libz3.a + build/*.so + build/*.a + build/python + key: ${{ needs.build-cache.outputs.cache-key }} + + - name: Use Z3 + run: build/z3 --version +``` + +## Benefits + +- **Time Savings**: Eliminates 15-17 minute build time when cache hit +- **Resource Efficiency**: Reduces CI compute usage +- **Reliability**: Ensures consistent Z3 binary across workflow runs +- **Flexibility**: Works with manual triggers, schedules, and pushes + +## Example: Soundness Bug Detector + +The soundness bug detector workflow can now use cached Z3: + +```yaml +name: Soundness Bug Detector + +on: + schedule: + - cron: '0 4 * * *' + +jobs: + detect-bugs: + runs-on: ubuntu-latest + steps: + - name: Checkout code + uses: actions/checkout@v6 + + - name: Setup Python + uses: actions/setup-python@v6 + with: + python-version: '3.x' + + - name: Restore Z3 cache + uses: actions/cache/restore@v4 + with: + path: | + build/z3 + build/libz3.so + build/libz3.a + build/*.so + build/*.a + build/python + key: z3-build-${{ runner.os }}-${{ github.sha }} + restore-keys: | + z3-build-${{ runner.os }}- + + - name: Build Z3 (if not cached) + run: | + if [ ! -f build/z3 ]; then + python scripts/mk_make.py + cd build + make -j$(nproc) + fi + + - name: Test soundness issues + run: | + # Now Z3 is available at build/z3 + build/z3 --version + # ... rest of soundness testing logic +``` + +## Cache Maintenance + +**GitHub Actions Cache Policies:** +- **Retention**: Caches are removed after 7 days without being accessed +- **Repository Limit**: Total cache size per repository is limited to 10GB +- **Eviction**: Least Recently Used (LRU) caches are evicted when the limit is reached +- **Size per Entry**: Each Z3 build cache is approximately 70MB (z3 executable, libz3 libraries, and Python bindings) + +**This Workflow's Strategy:** +- **Daily Schedule**: Runs daily at 2 AM UTC to refresh the cache +- **Push Trigger**: Updates cache on pushes to master/main branches +- **Manual Trigger**: Can be triggered manually via workflow_dispatch + +**Best Practices:** +- The daily schedule ensures at least one cache is always available (within 7-day retention) +- Multiple commits may share the same cache via the `restore-keys` fallback pattern +- If you need guaranteed cache availability for a specific commit, manually trigger the workflow + +## Troubleshooting + +### Cache miss on every run + +If you're getting cache misses, check: +1. The cache key format matches between save and restore +2. The git SHA is consistent (use the same checkout before restore) +3. The runner OS matches + +### Build not working after restore + +After restoring from cache: +1. Verify all library files are present: `ls -la build/` +2. Check library dependencies: `ldd build/z3` +3. Ensure Python bindings are in the correct location + +### Need different build configuration + +If you need a different Z3 build (e.g., with debug symbols), you can: +1. Create a separate cache workflow with a different cache key +2. Or build Z3 directly in your workflow with custom flags + +## Related Workflows + +- `ci.yml` - Main CI workflow (could benefit from caching) +- `soundness-bug-detector.lock.yml` - Automated soundness testing +- `nightly.yml` - Nightly builds (uses its own build process) + +## Implementation Note + +This addresses the recommendation from [GitHub Discussion #8458](https://github.com/Z3Prover/z3/discussions/8458), which identified that the soundness bug detector and other workflows were unable to test properly due to missing Z3 binaries and build tool limitations. diff --git a/.github/workflows/build-z3-cache.yml b/.github/workflows/build-z3-cache.yml new file mode 100644 index 000000000..9b101e739 --- /dev/null +++ b/.github/workflows/build-z3-cache.yml @@ -0,0 +1,79 @@ +name: Build and Cache Z3 + +on: + # Allow manual trigger + workflow_dispatch: + # Run on schedule to keep cache fresh (daily at 2 AM UTC) + schedule: + - cron: '0 2 * * *' + # Run on pushes to main to update cache with latest changes + push: + branches: [ "master", "main" ] + # Make this callable as a reusable workflow + workflow_call: + outputs: + cache-key: + description: "The cache key for the built Z3 binary" + value: ${{ jobs.build-z3.outputs.cache-key }} + +permissions: + contents: read + +jobs: + build-z3: + name: "Build Z3 for caching" + runs-on: ubuntu-latest + timeout-minutes: 90 + outputs: + cache-key: ${{ steps.cache-key.outputs.key }} + + steps: + - name: Checkout code + uses: actions/checkout@v6 + + - name: Setup Python + uses: actions/setup-python@v6 + with: + python-version: '3.x' + + - name: Generate cache key + id: cache-key + run: | + # Create a cache key based on git SHA and relevant source files + echo "key=z3-build-${{ runner.os }}-${{ github.sha }}" >> $GITHUB_OUTPUT + echo "fallback-key=z3-build-${{ runner.os }}-" >> $GITHUB_OUTPUT + + - name: Restore or create cache + id: cache-z3 + uses: actions/cache@v4 + with: + path: | + build/z3 + build/libz3.so + build/libz3.a + build/*.so + build/*.a + build/python + key: ${{ steps.cache-key.outputs.key }} + restore-keys: | + z3-build-${{ runner.os }}- + + - name: Configure Z3 + if: steps.cache-z3.outputs.cache-hit != 'true' + run: python scripts/mk_make.py + + - name: Build Z3 + if: steps.cache-z3.outputs.cache-hit != 'true' + run: | + cd build + make -j$(nproc) + + - name: Display build info + run: | + echo "Cache key: ${{ steps.cache-key.outputs.key }}" + echo "Build directory contents:" + ls -lh build/ || echo "Build directory not found" + if [ -f build/z3 ]; then + echo "Z3 version:" + build/z3 --version + fi