Source: z3
Version: 4.8.7-2
Severity: important
Tags: patch
Dear Maintainer,
Please apply the attached patch to fix the FTBFS on riscv64.
Since this is a dependency of libllvm9, we need this in order to port rustc to
riscv64.
Please see also the attached patch to support cross-compiling which I needed in
order to test that the first patch works. You can repeat the build yourself
with an
sbuild invocation like:
/usr/bin/sbuild --no-arch-all \
--add-depends=libstdc++6:riscv64 \
--add-depends=libc6:riscv64 \
--host=riscv64 \
--extra-repository="deb http://ftp.ports.debian.org/debian-ports/ sid main" \
./z3_4.8.7-2.1.dsc
X
-- System Information:
Debian Release: bullseye/sid
APT prefers testing
APT policy: (990, 'testing'), (500, 'unstable-debug'), (500,
'testing-debug'), (500, 'stable'), (300, 'unstable'), (100, 'experimental'),
(1, 'experimental-debug')
Architecture: amd64 (x86_64)
Foreign Architectures: i386
Kernel: Linux 5.3.0-3-amd64 (SMP w/4 CPU cores)
Locale: LANG=en_GB.utf8, LC_CTYPE=en_GB.utf8 (charmap=UTF-8), LANGUAGE=en_GB:en
(charmap=UTF-8)
Shell: /bin/sh linked to /bin/dash
Init: systemd (via /run/systemd/system)
LSM: AppArmor: enabled
>From 83ce6c6b26e8686b9d4786e82a5b82eabec23dec Mon Sep 17 00:00:00 2001
From: Ximin Luo <infini...@debian.org>
Date: Sat, 4 Jan 2020 00:32:15 +0000
Subject: [PATCH 1/3] Link to -latomic on riscv64, fixes FTBFS
---
debian/control | 7 ++++---
debian/rules | 6 ++++++
2 files changed, 10 insertions(+), 3 deletions(-)
diff --git a/debian/control b/debian/control
index c7e4636..5a86bef 100644
--- a/debian/control
+++ b/debian/control
@@ -6,9 +6,10 @@ Uploaders: Fabian Wolff <fabi.wo...@arcor.de>,
Michael Tautschnig <m...@debian.org>
Build-Depends: debhelper-compat (= 12),
dh-python, python3,
- javahelper [!hppa !hurd-i386 !m68k !sh4],
- default-jdk [!hppa !hurd-i386 !m68k !sh4],
- ocaml-nox, dh-ocaml, ocaml-findlib, libzarith-ocaml-dev
+ javahelper [!hppa !hurd-i386 !m68k !sh4 !riscv64],
+ default-jdk [!hppa !hurd-i386 !m68k !sh4 !riscv64],
+ ocaml-nox, dh-ocaml, ocaml-findlib, libzarith-ocaml-dev,
+ libatomic1 [riscv64],
Standards-Version: 4.4.1
Homepage: https://github.com/Z3Prover/z3
Vcs-Git: https://salsa.debian.org/pkg-llvm-team/z3.git
diff --git a/debian/rules b/debian/rules
index 31167b0..ae26173 100755
--- a/debian/rules
+++ b/debian/rules
@@ -3,6 +3,8 @@
# Uncomment this to turn on verbose mode.
# export DH_VERBOSE=1
+include /usr/share/dpkg/architecture.mk
+
export DEB_BUILD_MAINT_OPTIONS = hardening=+all
export DEB_CXXFLAGS_MAINT_APPEND = -fPIC
@@ -29,6 +31,10 @@ override_dh_auto_configure:
python3 scripts/mk_make.py --python
--pypkgdir=$(CURDIR)/debian/tmp/usr/lib/python3/dist-packages --ml
--prefix=$(CURDIR)/debian/tmp/usr; \
fi
sed -i 's/^SLINK_FLAGS=/SLINK_FLAGS=$$(LDFLAGS) -fPIC /' build/config.mk
+ifneq (,$(filter $(DEB_HOST_ARCH), riscv64))
+ sed -i 's/^LINK_EXTRA_FLAGS=/LINK_EXTRA_FLAGS=-latomic /'
build/config.mk
+ sed -i 's/^SLINK_EXTRA_FLAGS=/SLINK_EXTRA_FLAGS=-latomic /'
build/config.mk
+endif
echo 'libz3$$(SO_EXT): SLINK_FLAGS += -Wl,-soname,libz3.so.4' >>
build/Makefile
printf '%%:\n\t$$(MAKE) -C build $$@\n' > Makefile
printf '\nall:\n\t$$(MAKE) -C build $$@\n' >> Makefile
--
2.24.1
>From 445f59f3818d68d7995bb387a67a2920f01e5787 Mon Sep 17 00:00:00 2001
From: Ximin Luo <infini...@debian.org>
Date: Sat, 4 Jan 2020 01:07:50 +0000
Subject: [PATCH 2/3] support cross-compiling
---
debian/control | 5 +++--
debian/rules | 50 +++++++++++++++++++++++++++++++++-----------------
2 files changed, 36 insertions(+), 19 deletions(-)
diff --git a/debian/control b/debian/control
index 5a86bef..7e69bb9 100644
--- a/debian/control
+++ b/debian/control
@@ -5,10 +5,10 @@ Maintainer: LLVM Packaging Team
<pkg-llvm-t...@lists.alioth.debian.org>
Uploaders: Fabian Wolff <fabi.wo...@arcor.de>,
Michael Tautschnig <m...@debian.org>
Build-Depends: debhelper-compat (= 12),
- dh-python, python3,
+ dh-python, python3:any,
javahelper [!hppa !hurd-i386 !m68k !sh4 !riscv64],
default-jdk [!hppa !hurd-i386 !m68k !sh4 !riscv64],
- ocaml-nox, dh-ocaml, ocaml-findlib, libzarith-ocaml-dev,
+ ocaml-nox <!cross>, dh-ocaml <!cross>, ocaml-findlib <!cross>,
libzarith-ocaml-dev <!cross>,
libatomic1 [riscv64],
Standards-Version: 4.4.1
Homepage: https://github.com/Z3Prover/z3
@@ -79,6 +79,7 @@ Package: libz3-ocaml-dev
Section: ocaml
Architecture: any
Depends: libz3-dev (= ${binary:Version}), ${misc:Depends}, ${ocaml:Depends},
${shlibs:Depends}
+Build-Profiles: <!cross>
Recommends: ocaml-findlib
Description: theorem prover from Microsoft Research - OCaml bindings
Z3 is a state-of-the art theorem prover from Microsoft Research. See the z3
diff --git a/debian/rules b/debian/rules
index ae26173..6dfb755 100755
--- a/debian/rules
+++ b/debian/rules
@@ -10,26 +10,38 @@ export DEB_CXXFLAGS_MAINT_APPEND = -fPIC
DEB_HOST_MULTIARCH ?= $(shell dpkg-architecture -qDEB_HOST_MULTIARCH)
+# Support cross-compiling. This wouldn't be necessary with cmake which already
+# has cross-compiling integration in Debian, but we're using upstream's custom
+# Makefiles, so have to set these things ourselves.
+export CXX=$(DEB_HOST_GNU_TYPE)-g++
+export CC=$(DEB_HOST_GNU_TYPE)-gcc
+export AR=$(DEB_HOST_GNU_TYPE)-ar
+
+WITH_DH = python3
+MK_MAKE = --python
--pypkgdir=$(CURDIR)/debian/tmp/usr/lib/python3/dist-packages
+
ifneq (,$(shell dh_listpackages -a | grep libz3-jni))
- WITH_JAVA ?= yes
+ WITH_JAVA := yes
+ WITH_DH := $(WITH_DH),javahelper
+ MK_MAKE += --java
else
- WITH_JAVA ?= no
+ WITH_JAVA := no
+endif
+
+ifeq (,$(filter cross,$(DEB_BUILD_PROFILES)))
+ WITH_OCAML := yes
+ WITH_DH := $(WITH_DH),ocaml
+ MK_MAKE += --ml
+else
+ WITH_OCAML := no
endif
%:
- if [ $(WITH_JAVA) = yes ]; then \
- dh $@ --parallel --with python3,javahelper,ocaml; \
- else \
- dh $@ --parallel --with python3,ocaml; \
- fi
+ dh $@ --parallel --with $(WITH_DH);
override_dh_auto_configure:
sed -i 's/^DOTNET_ENABLED=.*/DOTNET_ENABLED=False/' scripts/mk_util.py;
\
- if [ $(WITH_JAVA) = yes ]; then \
- python3 scripts/mk_make.py --python
--pypkgdir=$(CURDIR)/debian/tmp/usr/lib/python3/dist-packages --java --ml
--prefix=$(CURDIR)/debian/tmp/usr; \
- else \
- python3 scripts/mk_make.py --python
--pypkgdir=$(CURDIR)/debian/tmp/usr/lib/python3/dist-packages --ml
--prefix=$(CURDIR)/debian/tmp/usr; \
- fi
+ python3 scripts/mk_make.py --prefix=$(CURDIR)/debian/tmp/usr $(MK_MAKE)
sed -i 's/^SLINK_FLAGS=/SLINK_FLAGS=$$(LDFLAGS) -fPIC /' build/config.mk
ifneq (,$(filter $(DEB_HOST_ARCH), riscv64))
sed -i 's/^LINK_EXTRA_FLAGS=/LINK_EXTRA_FLAGS=-latomic /'
build/config.mk
@@ -48,7 +60,7 @@ override_dh_clean:
$(RM) Makefile scripts/*.pyc
$(RM) -r build
$(RM) src/api/python/*.pyc
- $(RM) \
+ $(RM) -f \
src/api/api_commands.cpp \
src/api/api_log_macros.cpp \
src/api/api_log_macros.h \
@@ -136,16 +148,20 @@ override_dh_auto_install:
mv debian/tmp/usr/lib/libz3.so debian/tmp/usr/lib/libz3.so.4
ln -s libz3.so.4 debian/tmp/usr/lib/libz3.so
mkdir -p debian/tmp/usr/lib/$(DEB_HOST_MULTIARCH)/jni
- -mv debian/tmp/usr/lib/libz3java.so* \
+ifeq (yes,$(WITH_JAVA))
+ mv debian/tmp/usr/lib/libz3java.so* \
debian/tmp/usr/lib/$(DEB_HOST_MULTIARCH)/jni/
+endif
mv debian/tmp/usr/lib/libz3.so* \
debian/tmp/usr/lib/$(DEB_HOST_MULTIARCH)/
override_dh_install:
dh_install
- -cp build/api/ml/*.cmxa debian/libz3-ocaml-dev/usr/lib/ocaml/z3/
- -cp build/api/ml/*.cmx debian/libz3-ocaml-dev/usr/lib/ocaml/z3/
- -sed -i 's/^linkopts =.*/linkopts = "-cclib -L\/usr\/lib"/'
debian/libz3-ocaml-dev/usr/lib/ocaml/z3/META
+ifeq (yes,$(WITH_OCAML))
+ cp build/api/ml/*.cmxa debian/libz3-ocaml-dev/usr/lib/ocaml/z3/
+ cp build/api/ml/*.cmx debian/libz3-ocaml-dev/usr/lib/ocaml/z3/
+ sed -i 's/^linkopts =.*/linkopts = "-cclib -L\/usr\/lib"/'
debian/libz3-ocaml-dev/usr/lib/ocaml/z3/META
+endif
override_dh_installchangelogs:
dh_installchangelogs RELEASE_NOTES
--
2.24.1
