[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

Bug#895104: marked as done (why3: skip cvc4 autopkgtest on architectures without cvc4)

Your message dated Sun, 27 May 2018 12:19:42 +0000
with message-id <E1fMueE-000J04-Q3@fasolo.debian.org>
and subject line Bug#895104: fixed in why3 0.88.3-3
has caused the Debian Bug report #895104,
regarding why3: skip cvc4 autopkgtest on architectures without cvc4
to be marked as done.

This means that you claim that the problem has been dealt with.
If this is not the case it is now your responsibility to reopen the
Bug report if necessary, and/or fix the problem forthwith.

(NB: If you are a system administrator and have no idea what this
message is talking about, this may indicate a serious mail system
misconfiguration somewhere. Please contact owner@bugs.debian.org
immediately.)


-- 
895104: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=895104
Debian Bug Tracking System
Contact owner@bugs.debian.org with problems
--- Begin Message --- 
Package: why3
Version: 0.88.3-1
Severity: minor
Tags: patch
User: ubuntu-devel@lists.ubuntu.com
Usertags: origin-ubuntu bionic ubuntu-patch autopkgtest

Dear Ralf,

In addition to bug #895103, the why3 autopkgtests also fail on non-x86
architectures in Ubuntu because the test dependencies for the why3+cvc4 test
cannot be satisfied.  The attached patch makes the test dependency
architecture-specific and lets it pass as a no-op on architectures without
cvc4.

Cheers,
-- 
Steve Langasek                   Give me a lever long enough and a Free OS
Debian Developer                   to set it on, and I can move the world.
Ubuntu Developer                                    http://www.debian.org/
slangasek@ubuntu.com                                     vorlon@debian.org

diff -Nru why3-0.88.3/debian/tests/control why3-0.88.3/debian/tests/control
--- why3-0.88.3/debian/tests/control	2018-03-22 23:20:30.000000000 -0700
+++ why3-0.88.3/debian/tests/control	2018-04-06 18:31:42.000000000 -0700
@@ -5,7 +5,7 @@
 Depends: why3, cvc3
 
 Tests: why3+cvc4
-Depends: why3, cvc4
+Depends: why3, cvc4 [any-amd64 any-i386 mips mips64el mipsel]
 
 Tests: why3+spass
 Depends:why3, spass
diff -Nru why3-0.88.3/debian/tests/why3+cvc4 why3-0.88.3/debian/tests/why3+cvc4
--- why3-0.88.3/debian/tests/why3+cvc4	2018-01-14 05:52:54.000000000 -0800
+++ why3-0.88.3/debian/tests/why3+cvc4	2018-04-06 18:32:34.000000000 -0700
@@ -2,6 +2,15 @@
 
 set -e
 
+case $(dpkg --print-architecture) in
+    amd64|i386|hurd-i386|kfreebsd-amd64|kfreebsd-i386|mips|mips64el|mipsel)
+        ;;
+    *)
+        echo "SKIPPED cvc4 not available on this architecture"
+        exit 0
+        ;;
+    esac
+
 indir=debian/tests/why
 why3 config --detect-provers > /dev/null 2>&1
 for infile in $indir/*.mlw

--- End Message ---
--- Begin Message --- 
Source: why3
Source-Version: 0.88.3-3

We believe that the bug you reported is fixed in the latest version of
why3, which is due to be installed in the Debian FTP archive.

A summary of the changes between this version and the previous one is
attached.

Thank you for reporting the bug, which will now be closed.  If you
have further comments please address them to 895104@bugs.debian.org,
and the maintainer will reopen the bug report if appropriate.

Debian distribution maintenance software
pp.
Ralf Treinen <treinen@debian.org> (supplier of updated why3 package)

(This message was generated automatically at their request; if you
believe that there is a problem with it please contact the archive
administrators by mailing ftpmaster@ftp-master.debian.org)


-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA256

Format: 1.8
Date: Sun, 27 May 2018 13:37:54 +0200
Source: why3
Binary: why3 why3-coq libwhy3-ocaml-dev why3-examples why3-doc-html why3-doc-pdf
Architecture: source
Version: 0.88.3-3
Distribution: unstable
Urgency: medium
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Changed-By: Ralf Treinen <treinen@debian.org>
Description:
 libwhy3-ocaml-dev - OCaml librariries for why3 (dev)
 why3       - Software verification platform
 why3-coq   - Coq support for the why3 verification platform
 why3-doc-html - HTML Documentation of the why3 verification platform
 why3-doc-pdf - PDF Documentation of the why3 verification platform
 why3-examples - Examples for the why3 verification platform
Closes: 895104 899084
Changes:
 why3 (0.88.3-3) unstable; urgency=medium
 .
   * d/control: update Vcs-* fields to salsa
   * Add build-dependendency texlive-plain-generic to fix FTBFS with
     texlive 2018.20180505-1 (closes: #899084)
   * test why3+cvc4: skip when cvc4 is not available (closes: #895104)
Checksums-Sha1:
 056d25258f2ee8382cb99589afdc14409100d475 2620 why3_0.88.3-3.dsc
 28cbda79cbbeeadfc34f27282250dcf46dbeba6c 13192 why3_0.88.3-3.debian.tar.xz
 14af76ffb323b15c0e2b2b8fe425c3eb9ecd34af 12335 why3_0.88.3-3_source.buildinfo
Checksums-Sha256:
 d8c26aea1d460c9dcd99dea2bdbc2643bd8f83b26bcfd8e39c374768e939ff19 2620 why3_0.88.3-3.dsc
 45c4192092b235f5f9ccef80136b031ee362d1aa23bfc5d1997fe566dca03318 13192 why3_0.88.3-3.debian.tar.xz
 ad0079e8285903eaa3966a45dc0bc5c430579ed961ee512f60ed81ce717f9593 12335 why3_0.88.3-3_source.buildinfo
Files:
 d9fee7588cdc888853f2a60d1da83f1b 2620 math optional why3_0.88.3-3.dsc
 a7e32d57c010e2fcee58893ea3445c05 13192 math optional why3_0.88.3-3.debian.tar.xz
 9b00fcd75105912355227804d022f77e 12335 math optional why3_0.88.3-3_source.buildinfo

-----BEGIN PGP SIGNATURE-----

iQIzBAEBCAAdFiEEAgVIKeEtDyqOZI5idFxHZtTKzf8FAlsKnZIACgkQdFxHZtTK
zf9GUg//YHDbUMRGmHHADRPzM3ElZLGUrWC0Ta+BzH0HpHEqB7wN8YC+4wxe6r6Y
1nzbK2ArtXZ0YUPNCpl0Ubzjyw0ULOcnRqp5889OYGib+c4Gh6jkaXsl+owkKauj
YUORroW4e5GEc9HuJn5QNsqbeuf5TLFJYANQuZ9k2zPSG/ISjnIT1wqb+yIxg9j/
Nj9cX4l5YZtEbbGaQJ4IHXKMJmYhetZxTxhXICGvkUMtJuoY0fnV5JE2A+NFmAAv
IYQOgIHD881/jUe/E9GzTY2Qj4DbP/9an0ZV0FITq80ZtFfucUWCUdcmygCDIsM5
XD/Svseklw1P0gVxCTxZ+k+wAohJPD/lOwnW0dQK+9yFXMeufXh6MKhkYfvI2RtH
j8gfbYw5MrjN1WqBtoXRQwcE1kVhvE+jdB1o7JeU8z3I2ZsdttvA+o+GOR8DY2KU
OpRx7qms+HvylZJdstiLPYRzR8qRb+IxRTq5PUJ74t0TN2jknfyaWjIkseiL0/0W
DokqbfuOYYSfE5Ybp+L4fU2qqOfyZNuFXiCkym5ATQxQWlu/G5l5RJI5L4HSdhl7
tCcQapx+81f+RE9O4+TaKhodwJoKznz6gSjolauNF/0aR8G0+M44fyoyWQT6OG6V
wjxB06rZk+iWfpYdQutSDFiW4pZTRAChjx/2Ev6QknRWIoGrVkg=
=qOu/
-----END PGP SIGNATURE-----

--- End Message ---
Reply to: