mirror of
https://github.com/Z3Prover/z3
synced 2025-09-30 13:19:04 +00:00
Daily Perf Improver: Add build steps configuration
This commit adds the GitHub Action configuration file for setting up the Z3 build environment for performance development work. The action includes: - Installing build dependencies (cmake, ninja, python3, etc.) - Cleaning any polluted source tree from previous Python builds - Configuring CMake with RelWithDebInfo for performance work - Building Z3 and test executables - Cloning z3test repository for benchmarks - Setting up performance measurement tools - Creating micro-benchmark infrastructure This configuration is based on the research and plan outlined in issue #7872 and follows the standard CMake build process documented in README-CMake.md. > AI-generated content by [Daily Perf Improver](https://github.com/Z3Prover/z3/actions/runs/17735701277) may contain mistakes.
This commit is contained in:
Daily Perf Improver
parent
25a79d73b1
commit
a31656a705
1 changed files with 150 additions and 0 deletions
150
.github/actions/daily-perf-improver/build-steps/action.yml
vendored
Normal file
150
.github/actions/daily-perf-improver/build-steps/action.yml
vendored
Normal file
|
|
@ -0,0 +1,150 @@
|
|||
name: 'Z3 Performance Development Build Steps'
|
||||
description: 'Set up Z3 build environment for performance development and testing'
|
||||
|
||||
runs:
|
||||
using: "composite"
|
||||
steps:
|
||||
- name: Install dependencies
|
||||
shell: bash
|
||||
run: |
|
||||
echo "Installing dependencies..." | tee -a build-steps.log
|
||||
sudo apt-get update | tee -a build-steps.log
|
||||
sudo apt-get install -y build-essential cmake ninja-build python3 python3-pip git | tee -a build-steps.log
|
||||
echo "Dependencies installed successfully" | tee -a build-steps.log
|
||||
|
||||
- name: Verify build tools
|
||||
shell: bash
|
||||
run: |
|
||||
echo "Verifying build tools..." | tee -a build-steps.log
|
||||
echo "CMake version:" | tee -a build-steps.log
|
||||
cmake --version | tee -a build-steps.log
|
||||
echo "Ninja version:" | tee -a build-steps.log
|
||||
ninja --version | tee -a build-steps.log
|
||||
echo "Python version:" | tee -a build-steps.log
|
||||
python3 --version | tee -a build-steps.log
|
||||
echo "GCC version:" | tee -a build-steps.log
|
||||
gcc --version | tee -a build-steps.log
|
||||
echo "Build tools verified successfully" | tee -a build-steps.log
|
||||
|
||||
- name: Clean any polluted source tree
|
||||
shell: bash
|
||||
run: |
|
||||
echo "Cleaning potentially polluted source tree..." | tee -a build-steps.log
|
||||
git clean -fx src || echo "No files to clean in src/" | tee -a build-steps.log
|
||||
echo "Source tree cleaned" | tee -a build-steps.log
|
||||
|
||||
- name: Create and configure build directory
|
||||
shell: bash
|
||||
run: |
|
||||
echo "Creating build directory..." | tee -a build-steps.log
|
||||
mkdir -p build
|
||||
cd build
|
||||
echo "Configuring CMake for performance development..." | tee -a ../build-steps.log
|
||||
cmake -G "Ninja" \
|
||||
-DCMAKE_BUILD_TYPE=RelWithDebInfo \
|
||||
-DZ3_ENABLE_TRACING_FOR_NON_DEBUG=TRUE \
|
||||
-DZ3_BUILD_LIBZ3_SHARED=FALSE \
|
||||
-DZ3_BUILD_TEST_EXECUTABLES=TRUE \
|
||||
-DCMAKE_CXX_FLAGS="-fno-omit-frame-pointer" \
|
||||
../ | tee -a ../build-steps.log
|
||||
echo "CMake configuration completed" | tee -a ../build-steps.log
|
||||
|
||||
- name: Build Z3
|
||||
shell: bash
|
||||
run: |
|
||||
echo "Building Z3..." | tee -a build-steps.log
|
||||
cd build
|
||||
ninja | tee -a ../build-steps.log
|
||||
echo "Z3 build completed" | tee -a ../build-steps.log
|
||||
|
||||
- name: Build test executables
|
||||
shell: bash
|
||||
run: |
|
||||
echo "Building test executables..." | tee -a build-steps.log
|
||||
cd build
|
||||
ninja test-z3 | tee -a ../build-steps.log
|
||||
echo "Test executables built" | tee -a ../build-steps.log
|
||||
|
||||
- name: Verify build outputs
|
||||
shell: bash
|
||||
run: |
|
||||
echo "Verifying build outputs..." | tee -a build-steps.log
|
||||
cd build
|
||||
ls -la z3 test-z3 libz3.a | tee -a ../build-steps.log
|
||||
echo "Z3 executable version:" | tee -a ../build-steps.log
|
||||
./z3 --version | tee -a ../build-steps.log
|
||||
echo "Build outputs verified successfully" | tee -a ../build-steps.log
|
||||
|
||||
- name: Clone z3test repository for benchmarks
|
||||
shell: bash
|
||||
run: |
|
||||
echo "Cloning z3test repository for benchmarks..." | tee -a build-steps.log
|
||||
if [ ! -d "z3test" ]; then
|
||||
git clone https://github.com/z3prover/z3test z3test | tee -a build-steps.log
|
||||
else
|
||||
echo "z3test already exists, updating..." | tee -a build-steps.log
|
||||
cd z3test
|
||||
git pull | tee -a ../build-steps.log
|
||||
cd ..
|
||||
fi
|
||||
echo "z3test repository ready" | tee -a build-steps.log
|
||||
|
||||
- name: Run quick verification tests
|
||||
shell: bash
|
||||
run: |
|
||||
echo "Running quick verification tests..." | tee -a build-steps.log
|
||||
cd build
|
||||
echo "Running unit tests (first 10)..." | tee -a ../build-steps.log
|
||||
timeout 60s ./test-z3 | head -20 | tee -a ../build-steps.log || echo "Unit tests running (timeout reached)" | tee -a ../build-steps.log
|
||||
echo "Testing basic Z3 functionality..." | tee -a ../build-steps.log
|
||||
echo "(assert (> x 0))" | ./z3 -in | tee -a ../build-steps.log
|
||||
echo "Quick verification tests completed" | tee -a ../build-steps.log
|
||||
|
||||
- name: Set up performance measurement tools
|
||||
shell: bash
|
||||
run: |
|
||||
echo "Setting up performance measurement tools..." | tee -a build-steps.log
|
||||
which perf || echo "perf not available" | tee -a build-steps.log
|
||||
which valgrind || echo "valgrind not available" | tee -a build-steps.log
|
||||
echo "Performance measurement tools setup completed" | tee -a build-steps.log
|
||||
|
||||
- name: Create micro-benchmark template
|
||||
shell: bash
|
||||
run: |
|
||||
echo "Creating micro-benchmark infrastructure..." | tee -a build-steps.log
|
||||
mkdir -p perf-bench
|
||||
cat > perf-bench/README.md << 'EOF'
|
||||
# Z3 Performance Benchmarks
|
||||
|
||||
This directory contains micro-benchmarks for Z3 performance testing.
|
||||
|
||||
## Quick Start
|
||||
|
||||
1. Run unit tests: `cd build && ./test-z3 -a`
|
||||
2. Run regression tests: `python z3test/scripts/test_benchmarks.py build/z3 z3test/regressions/smt2-extra`
|
||||
3. Basic SMT solving: `echo "(assert (> x 0))" | build/z3 -in`
|
||||
|
||||
## Performance Measurement
|
||||
|
||||
- Use `build/z3 -st input.smt2` to get statistics
|
||||
- Use `perf` or `valgrind` for detailed profiling
|
||||
- Time measurements: Use `scoped_timer` class in Z3 code
|
||||
|
||||
## Build Commands
|
||||
|
||||
- Clean rebuild: `rm -rf build && mkdir build && cd build && cmake -G "Ninja" -DCMAKE_BUILD_TYPE=RelWithDebInfo ../ && ninja`
|
||||
- Build tests only: `ninja test-z3`
|
||||
- Build with profiling: `cmake -DCMAKE_CXX_FLAGS="-pg -fno-omit-frame-pointer" ../`
|
||||
EOF
|
||||
echo "Micro-benchmark infrastructure created" | tee -a build-steps.log
|
||||
|
||||
- name: Display build summary
|
||||
shell: bash
|
||||
run: |
|
||||
echo "=== Z3 Performance Development Environment Ready ===" | tee -a build-steps.log
|
||||
echo "Build directory: $(pwd)/build" | tee -a build-steps.log
|
||||
echo "Z3 executable: $(pwd)/build/z3" | tee -a build-steps.log
|
||||
echo "Test executable: $(pwd)/build/test-z3" | tee -a build-steps.log
|
||||
echo "Benchmark repository: $(pwd)/z3test" | tee -a build-steps.log
|
||||
echo "Build log: $(pwd)/build-steps.log" | tee -a build-steps.log
|
||||
echo "=== Setup Complete ===" | tee -a build-steps.log
|
||||
Loading…
Add table
Add a link
Reference in a new issue