Build binary wheels with cibuildwheel via the ivpm-build backend - #1
Merged
Conversation
Switch packaging to ivpm-build's PEP 517 backend so CI can produce
self-contained binary wheels (native libs loaded via ctypes; no compiler
needed at install time). With ivpm-build's platform-tagging fix, the wheel is
correctly tagged py3-none-<platform> rather than a pure-Python py3-none-any.
pyproject.toml:
- build-backend = ivpm_build.backend (pinned to git main until a PyPI
release carrying the platform-tag fix is available)
- [tool.ivpm-build]: cmake=true + extra-data staging the three native libs
(dv_solve, dv_solve_dpi, dv_solve_debug) at the package root, the public C
headers into share/include, and the SV package into share/sv
- [tool.cibuildwheel]: build one wheel per platform (cp311-*, since the lib
is interpreter/ABI agnostic), smoke-test that the bundled lib loads, and
install cmake via dnf in the manylinux container (ninja comes from the
backend's build requires)
CMakeLists.txt: install public headers to include/dv_solve (excluding the
vendored kissat fork).
lib.py: search the installed package dir and build/lib(64) (L1), use
platform-correct library names for .so/.dylib/.dll (L2), and raise an
actionable not-found error with searched paths and build instructions (L3);
ctx/bvsat/problem use the shared helper.
__init__.py: get_libs/get_libdirs/get_incdirs/get_deps/get_svdirs/get_dpi_lib
for C and SystemVerilog consumers, resolving wheel vs source-tree layout.
MANIFEST.in: ship CMakeLists.txt, cmake/, src/c, src/sv and tests/ in the
sdist so it builds from source.
.github/workflows/wheels.yml: build wheels across Linux (x86_64 + aarch64,
the two most-recent manylinux baselines 2_34 and 2_28), macOS (x86_64 +
arm64) and Windows, plus an sdist.
Verified locally: project->wheel is py3-none-linux_x86_64 with all libs,
headers and SV bundled; installs into a clean venv and the native lib loads;
sdist is complete and a wheel builds from it.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
cibuildwheel 2.21.x does not recognize the short "manylinux_2_34" alias and passed it to docker as a literal image name, failing every 2_34 job. Use the full quay.io image paths (manylinux_2_28 / manylinux_2_34, x86_64 / aarch64), which are version-independent. The manylinux_2_28 x86_64 build already passed, confirming the packaging itself is correct. Scope the matrix to Linux (the two most-recent manylinux baselines x x86_64 + aarch64). macOS and Windows are dropped for now: the vendored kissat fork does not compile under AppleClang (implicit memset / missing string.h) or MSVC (GCC/Clang-only -W/-std flags). Those are C-portability fixes, separate from packaging, to be addressed before re-adding those platforms. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
cibuildwheel 2.21.3 crashes on the manylinux_2_34 image because it probes the EOL cp38 interpreter the image no longer ships. v4.x dropped Python 3.8, so it builds cleanly against 2_34. Add a concurrency group so superseded emulated runs are cancelled instead of running to completion. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…hon >=3.10
The newer manylinux images (manylinux_2_28/2_34 :latest) ship gcc 14, where
-Wimplicit-function-declaration is a hard error by default (it was only a
warning under the older gcc that cibuildwheel's pinned image digests used, and
likewise an error on AppleClang). Three latent implicit declarations blocked
the wheel build:
- kissat fork internal.c: the custom-allocator init path calls memset() but
the file never included <string.h> (upstream used kissat_calloc here).
- kissat vector.c: bare memcpy/memset/memmove without <string.h>.
- zsp_costguided.c called solver_set_value_selector() with no prototype in
scope; added the declaration to zsp_ctx.h (it was only defined in
zsp_ctx.c).
Verified: the full CMake build (all targets) compiles cleanly under
-Werror=implicit-function-declaration -Werror=implicit-int with gcc 13.
Also bump requires-python to >=3.10: 3.8 is EOL (which is why manylinux_2_34
no longer ships cp38) and 3.9 is nearly so. The wheel is py3-none, so it still
installs on any CPython >= 3.10.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Add a macOS job (macos-13 x86_64 + macos-14 arm64) to confirm the C portability fixes let the wheel build under AppleClang. Linux and sdist jobs are gated off with if: false for fast turnaround; revert this commit to restore the full matrix. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
First attempt at native MSVC Windows wheels. Adds a compat layer under
src/c/compat/win/ rather than editing the kissat/dv-solve sources:
- msvc_compat.h: force-included (/FI) into every TU; maps the GCC builtins
(__builtin_clz*/ctz*/prefetch/alloca and the unsigned add/mul overflow
checks via _Generic + x64 intrinsics) and defines S_ISDIR/S_ISREG.
- unistd.h / sys/time.h / sys/resource.h shims: POSIX I/O aliases
(access/isatty/unlink/getpid/popen...), struct timeval/rusage, and the
R_OK/_SC_* constants.
- win_compat.c: Win32 backings for gettimeofday (GetSystemTimePreciseAsFile-
Time), getrusage (GetProcessTimes + GetProcessMemoryInfo) and sysconf
(GetSystemInfo), compiled into the kissat static lib on MSVC.
CMake:
- kissat.cmake guards the GCC-only flags behind else(); the MSVC branch adds
the compat include dir, /FI, the Win32 defines, win_compat.c and psapi, and
drops the non-existent -lm.
- CMakeLists enables CMAKE_WINDOWS_EXPORT_ALL_SYMBOLS so the ctypes loader
can resolve the DLL's symbols, force-includes the shim for the dv-solve
targets, and adds RUNTIME/ARCHIVE install destinations so the .dll and
import .lib land in build/lib.
CI: temporarily switch the matrix to a single Windows job (Linux + sdist stay
disabled) for fast iteration. Verified the non-MSVC build still configures and
links on Linux.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
MSVC rejects __attribute__((format(...))) / ((always_inline)) in kissat's error.h/format.h. Define __attribute__(x) to nothing in the force-included compat header.
COUNT_RADIX was sized by a const size_t (WIDTH_RADIX = 1<<8); in C that is a VLA, which MSVC rejects. Use the literal bound (256) directly.
zsp_prop_templates.c used unsigned __int128 for one 64x64 mul-mod; MSVC has no __int128. Add zsp_mulmod_u64() using _umul128/_udiv128 on MSVC and __int128 elsewhere (a,b < m precondition keeps _udiv128 in range).
dv-solve timing helpers (zsp_placement/costguided/contradiction/bbsolver) use POSIX clock_gettime(CLOCK_MONOTONIC). Add the macro + a QueryPerformanceCounter (monotonic) / GetSystemTimePreciseAsFileTime (realtime) implementation.
IMPLIED_BY_LEARNT was a ({ ... }) statement expression (GCC/Clang only).
Extract it into a static inline function and make the macro a thin call
wrapper so the call sites are unchanged and it compiles under MSVC.
The dv-solve-smt2 CLI and the C unit-test executables are dev tools, not part of any wheel, and they pull in POSIX setenv/unsetenv and the internal lcg_dbg_bail data symbol (not exported from the DLL). Gate them behind a new DV_SOLVE_BUILD_TOOLS option, forced off on MSVC. The three shared libraries (the wheel payload) still build.
All platforms build now. build_wheels covers Linux (x86_64+aarch64, manylinux 2_34+2_28), macOS arm64 and Windows AMD64 on every run; macOS x86_64 (legacy, slow to schedule) runs only on release tags / manual dispatch; plus sdist.
The platform-tagging fix is now on PyPI (ivpm-build 0.2.0.27908268978), so replace the 'ivpm-build @ git+...@main' build requirement with a versioned PyPI dependency (>= that build). Verified an isolated 'python -m build' resolves it from PyPI, produces a py3-none-linux_x86_64 wheel, and the installed lib loads.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Enables
cibuildwheelto produce self-contained binary wheels fordv-solve. The native solver libraries are loaded via ctypes, so wheels are taggedpy3-none-<platform>(platform-specific but interpreter/ABI agnostic) using the platform-tagging fix landed inivpm-build.Changes
ivpm_build.backend;[tool.ivpm-build]stages the three native libs at the package root, headers intoshare/include, and the SV package intoshare/sv;[tool.cibuildwheel]builds one wheel per platform and smoke-tests that the bundled lib loads.include/dv_solve(excludes the kissat fork).build/lib(64)(L1), platform-correct lib names (L2), actionable not-found error (L3).get_libs/get_libdirs/get_incdirs/get_deps/get_svdirs/get_dpi_libdiscovery helpers.2_34and2_28), macOS (x86_64 + arm64), Windows, plus sdist.Verified locally
dv_solve-0.0.1-py3-none-linux_x86_64.whlwith all libs/headers/SV bundledNotes
ivpm-build @ git+...@mainuntil a PyPI release carrying the platform-tag fix is cut.🤖 Generated with Claude Code