z3/.github/workflows/README-build-cache.md

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:

- 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:

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:

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, which identified that the soundness bug detector and other workflows were unable to test properly due to missing Z3 binaries and build tool limitations.