mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 03:25:43 +00:00
Code Activity

Add local pre-commit hook running z3test regressions

Browse source 
Adds a versioned .githooks/pre-commit that builds z3 and runs the
z3test regression suite (scripts/test_benchmarks.py over
regressions/smt2) as a precondition for every commit. Enable with
'git config core.hooksPath .githooks'.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-06-27 08:45:19 -07:00
parent 6a62a53181
commit d704b289ef
2 changed files with 85 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

27
.githooks/README.md Normal file
View file

@ -0,0 +1,27 @@
# Git hooks
Versioned git hooks for this repository.
## pre-commit
Builds the `z3` binary and runs the [z3test](https://github.com/Z3Prover/z3test)
regression suite (`scripts/test_benchmarks.py` over `regressions/smt2`) locally.
The commit is aborted if the build or any regression fails.
### Enable
```bash
git config core.hooksPath .githooks
```
### Configuration (environment variables)
- `Z3_BUILD_DIR` — build directory to use/create (default: `build/release`).
- `Z3TEST_DIR` — existing `z3test` checkout. If unset, `z3test` is cloned into
`../z3test-precommit` next to the repository.
### Skip for a single commit
```bash
git commit --no-verify
```

58
.githooks/pre-commit Executable file
View file

@ -0,0 +1,58 @@
#!/usr/bin/env bash
#
# Pre-commit hook: build Z3 and run the z3test regression suite locally as a
# precondition for every commit. The commit is aborted if the build or any
# regression test fails.
#
# It builds the `z3` binary, then runs:
# python z3test/scripts/test_benchmarks.py <z3> z3test/regressions/smt2
#
# Enable for this clone with:
# git config core.hooksPath .githooks
#
# Configuration (environment variables):
# Z3_BUILD_DIR Build directory to use/create. Default: build/release
# Z3TEST_DIR Existing z3test checkout. If unset, z3test is cloned into
# a cache dir next to the repo (../z3test-precommit).
#
# Skip the hook for a one-off commit with:
# git commit --no-verify
set -euo pipefail
REPO_ROOT="$(git rev-parse --show-toplevel)"
cd "$REPO_ROOT"
BUILD_DIR="${Z3_BUILD_DIR:-build/release}"
Z3TEST_DIR="${Z3TEST_DIR:-$REPO_ROOT/../z3test-precommit}"
# --- Build the z3 binary -----------------------------------------------------
echo "[pre-commit] Building z3 in '$BUILD_DIR'..."
if [ ! -f "$BUILD_DIR/build.ninja" ] && [ ! -f "$BUILD_DIR/Makefile" ]; then
echo "[pre-commit] Configuring CMake build in '$BUILD_DIR'..."
cmake -G Ninja -S . -B "$BUILD_DIR" -DCMAKE_BUILD_TYPE=Release
fi
cmake --build "$BUILD_DIR" --target z3
Z3_BIN="$BUILD_DIR/z3"
if [ ! -x "$Z3_BIN" ]; then
echo "[pre-commit] ERROR: z3 binary not found at '$Z3_BIN'." >&2
exit 1
fi
# --- Ensure a z3test checkout is available -----------------------------------
if [ ! -d "$Z3TEST_DIR/regressions/smt2" ]; then
if [ -d "$Z3TEST_DIR/.git" ]; then
echo "[pre-commit] Updating z3test checkout in '$Z3TEST_DIR'..."
git -C "$Z3TEST_DIR" pull --ff-only || true
else
echo "[pre-commit] Cloning z3test into '$Z3TEST_DIR'..."
git clone --depth 1 https://github.com/Z3Prover/z3test "$Z3TEST_DIR"
fi
fi
# --- Run the regression suite ------------------------------------------------
echo "[pre-commit] Running regressions on z3test/regressions/smt2..."
python "$Z3TEST_DIR/scripts/test_benchmarks.py" "$Z3_BIN" "$Z3TEST_DIR/regressions/smt2"
echo "[pre-commit] Regressions passed."