Source: z3
Version: 4.8.12-3.1
Tags: patch
User: debian-cr...@lists.debian.org
Usertags: cross-satisfiability
z3 cannot be cross built from source, because its python3 dependency
fails to install. A host architecture Python fails postinst, but it also
is not what z3 needs for building as it wants to run Python during
build.
In a divide and conquer approach, I first looked into adding support for
a nopython build profile such that the separate bindings could be
approached separately. Doing so, I recommend using dh-sequence-*
build-dependencies as they can be conditionalized using build profiles.
Likewise, I recommend installing the documentation symlink using
dh_installdocs --linkdoc, because it also handles build profiles at no
extra effort. While at it, I noticed that the libz3-java -> libz3-dev
dependency is not tight enough for using --linkdoc. Completely removing
Python dependencies happens to break the build, because even with
-DZ3_BUILD_PYTHON_BINDINGS=OFF Python and setuptools are being used, so
we need to depend on those without a profile.
It turns out that a nojava+nopython cross build just works. The z3
Python module is based on ctypes. From a packaging point of view, this
mostly means we can handle it as if it was a pure Python module. Hence,
annotating the python3 dependency with :any or :native is reasonable.
Once doing so, a nojava cross build also succeeds.
Cross building with java is a more distant topic not solved here. The
javahelper package is Arch:all and implicitly M-A:no. Any package
depending on it currently cannot satisfy its cross Build-Depends. This
is a problem that should be solved at the javahelper side rather than
here.
Given all of this, I am attaching a patch fixing all mentioned issues
but the javahelper one. Please let me know if this change is acceptable
or whether I should split it into smaller pieces for the individual
problems.
Helmut
diff --minimal -Nru z3-4.8.12/debian/changelog z3-4.8.12/debian/changelog
--- z3-4.8.12/debian/changelog 2023-02-01 13:06:03.000000000 +0100
+++ z3-4.8.12/debian/changelog 2024-11-04 16:15:47.000000000 +0100
@@ -1,3 +1,16 @@
+z3 (4.8.12-3.2) UNRELEASED; urgency=medium
+
+ * Non-maintainer upload.
+ * Improve cross building. (Closes: #-1)
+ + Multiarchify python3 dependency.
+ * Add nopython build profile.
+ + Conditionalize debhelper addons via Build-Depends.
+ + Let debhelper conditionalize --link-doc based on profiles.
+ + Unconditional python3-setuptools dependency needed even with <!nopython>.
+ * Tighten libz3-java -> libz3-dev dependency for doc linking.
+
+ -- Helmut Grohne <hel...@subdivi.de> Mon, 04 Nov 2024 16:15:47 +0100
+
z3 (4.8.12-3.1) unstable; urgency=medium
* Non-maintainer upload.
diff --minimal -Nru z3-4.8.12/debian/control z3-4.8.12/debian/control
--- z3-4.8.12/debian/control 2023-02-01 13:01:38.000000000 +0100
+++ z3-4.8.12/debian/control 2024-11-04 16:15:47.000000000 +0100
@@ -4,8 +4,9 @@
Maintainer: LLVM Packaging Team <pkg-llvm-t...@lists.alioth.debian.org>
Uploaders: Fabian Wolff <fabi.wo...@arcor.de>
Build-Depends: debhelper-compat (= 13),
- dh-python, python3, cmake, libsimde-dev,
- javahelper [!hppa !hurd-i386 !m68k !sh4] <!nojava>,
+ cmake, libsimde-dev, python3:any, python3-setuptools,
+ dh-sequence-python3 <!nopython>,
+ dh-sequence-javahelper [!hppa !hurd-i386 !m68k !sh4] <!nojava>,
default-jdk [!hppa !hurd-i386 !m68k !sh4] <!nojava>
Standards-Version: 4.6.0
Homepage: https://github.com/Z3Prover/z3
@@ -60,6 +61,7 @@
Package: python3-z3
Section: python
Architecture: any
+Build-Profiles: <!nopython>
Pre-Depends: ${misc:Pre-Depends}
Depends: libz3-dev (= ${binary:Version}),
python3-pkg-resources,
@@ -76,7 +78,7 @@
Build-Profiles: <!nojava>
Section: java
Architecture: amd64 arm64 armel armhf i386 mips mips64el mipsel powerpc
ppc64el s390x alpha kfreebsd-amd64 kfreebsd-i386 powerpcspe riscv64 sparc64 x32
-Depends: libz3-jni (>= ${binary:Version}), libz3-jni (<<
${source:Version}.1~), libz3-dev, ${misc:Depends}, ${java:Depends}
+Depends: libz3-jni (>= ${binary:Version}), libz3-jni (<<
${source:Version}.1~), libz3-dev (= ${binary:Version}), ${misc:Depends},
${java:Depends}
Description: theorem prover from Microsoft Research - java bindings
Z3 is a state-of-the-art theorem prover from Microsoft Research. See the z3
package for a detailed description.
diff --minimal -Nru z3-4.8.12/debian/rules z3-4.8.12/debian/rules
--- z3-4.8.12/debian/rules 2023-02-01 13:04:59.000000000 +0100
+++ z3-4.8.12/debian/rules 2024-11-04 16:15:47.000000000 +0100
@@ -12,30 +12,26 @@
DEB_HOST_MULTIARCH ?= $(shell dpkg-architecture -qDEB_HOST_MULTIARCH)
-ifneq (,$(shell dh_listpackages -a | grep libz3-jni))
- WITH_JAVA ?= ON
- WITH_JAVAHELPER ?= ,javahelper
-else
- WITH_JAVA ?= OFF
- WITH_JAVAHELPER ?=
-endif
+DOPACKAGES := $(shell dh_listpackages)
+WITH_JAVA := $(if $(filter libz3-jni,$(DOPACKAGES)),ON,OFF)
+WITH_PYTHON := $(if $(filter python3-z3,$(DOPACKAGES)),ON,OFF)
export CCACHE_BASEDIR = $(shell pwd)
%:
- dh $@ --with python3$(WITH_JAVAHELPER)
+ dh $@
override_dh_auto_configure:
dh_auto_configure --buildsystem=cmake+makefile -- \
-DCMAKE_INSTALL_PYTHON_PKG_DIR=lib/python3/dist-packages \
-DCMAKE_BUILD_TYPE=RelWithDebInfo \
- -DZ3_BUILD_PYTHON_BINDINGS=ON \
+ -DZ3_BUILD_PYTHON_BINDINGS=$(WITH_PYTHON) \
-DZ3_BUILD_DOTNET_BINDINGS=OFF \
-DZ3_BUILD_JAVA_BINDINGS=$(WITH_JAVA)
+override_dh_installdocs:
+ dh_installdocs -ppython3-z3 -plibz3-java -plibz3-jni
--link-doc=libz3-dev
+ dh_installdocs -Npython3-z3 -Nlibz3-java -Nlibz3-jni
+
override_dh_installchangelogs:
dh_installchangelogs RELEASE_NOTES
- for p in python3-z3 libz3-java libz3-jni ; do \
- $(RM) -rf debian/$$p/usr/share/doc/$$p/ ; \
- ln -s libz3-dev debian/$$p/usr/share/doc/$$p || true ; \
- done
