Skip to content

BLD: provide CMake option to install only python bindings #8016

@h-vetinari

Description

@h-vetinari

Hi!

I help run conda-forge, a big packaging ecosystem for python and many more languages. For almost a year, we've providing z3 as a package that can be installed also through conda install -c conda-forge z3-solver.

Conda as a paradigm is strictly more powerful than what PyPI and wheels can offer, namely, we can package native C/C++/Fortran libraries and binaries for linux/osx/win just as well as python libraries.

Unsurprisingly, the C++ library underlying z3-solver is independent of the python version being used. This is a very common pattern, and we like to package things in a way that reduces vendoring and other redundancies; in other words, there's a python-independent libz3, which z3-solver can then depend on, and everything works fine.

However, there's a limitation in building the package at the moment; due to the very bespoke python scripts/mk_make.py setup, I've preferred to go with the CMake-based builds; the problem with this is just that we're very inefficiently building the library portion 6 times, rather than once, namely (indentation indicates dependence):

  • libz3 - necessary ✅
    • z3-solver (py3.10) - rebuilds library, discards it because it matches what libz3 provides ❌
    • z3-solver (py3.11) - rebuilds library, discards it because it matches what libz3 provides ❌
    • z3-solver (py3.12) - rebuilds library, discards it because it matches what libz3 provides ❌
    • z3-solver (py3.13) - rebuilds library, discards it because it matches what libz3 provides ❌
    • z3-solver (py3.14) - rebuilds library, discards it because it matches what libz3 provides ❌

If there was an easy way to install just the python bindings on top of an already-installed libz3 (everything for us is happens in one central but relocatable $PREFIX), that would allow us to cut this down to building the library once, and then do only very quick installs for the python bindings. This would cut the build time from 3-5h down to ~1h.

I have enough experience with this that I could probably hack something together (and we do test our packages before publishing), but then it would be me who has to maintain it, and I was hoping that this is a reasonable request that the project would be willing to accommodate. 😅🙃

Metadata

Metadata

Assignees

Labels

No labels
No labels

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions