Bug#1086731: z3 FTCBFS: python3 dependency not installable

[Helmut Grohne]

Source: z3
Version: 4.8.12-3.1
Tags: patch
User: debian-cross at 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
-------------- next part --------------
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 <helmut at 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-team at lists.alioth.debian.org>
 Uploaders: Fabian Wolff <fabi.wolff at 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