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

Bug#902308: marked as done (why3: autopkgtest depends on cvc3 which is not available in buster)

Your message dated Wed, 27 Jun 2018 21:11:40 +0000
with message-id <E1fYHj2-0005A2-6P@fasolo.debian.org>
and subject line Bug#902308: fixed in why3 1.0.0-1
has caused the Debian Bug report #902308,
regarding why3: autopkgtest depends on cvc3 which is not available in buster
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.)


-- 
902308: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=902308
Debian Bug Tracking System
Contact owner@bugs.debian.org with problems
--- Begin Message --- 
Source: why3
Version: 0.88.3-3
Severity: minor
User: debian-ci@lists.debian.org
Usertags: issue

Dear OCaml maintainers,

Looking through the list of packages that have their autopkgtest pass on
unstable but fail on testing, I noticed that one of your tests depends
on cvc3, which currently isn't available in testing.

cvc3 isn't in testing due to a nearly year old bug 873975 which has a
proposed solution. Could you either help the maintainer to get cvc3 back
into testing, or otherwise drop your test that depends on it?

In the current autopkgtest setup, the package will be installed from
unstable, but that happens in a fall back I'd like to avoid because
everything that is newer in unstable is then allowed to be updated,
causing less than ideal testing and spurious failures.

Testing only with testing currently fails, as it can't find cvc3. This
means that when a reference for migration is created, the baseline set
to FAIL and every next package that is tested against why3 will be
allowed to regress (albeit any PASS will set the baseline to PASS, so
this is "only" an issue for the first package after the reference is set).

Thanks for considering.

Paul

Attachment: signature.asc
Description: OpenPGP digital signature


--- End Message ---
--- Begin Message --- 
Source: why3
Source-Version: 1.0.0-1

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 902308@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: Wed, 27 Jun 2018 22:19:33 +0200
Source: why3
Binary: why3 why3-coq libwhy3-ocaml-dev why3-examples why3-doc-html why3-doc-pdf
Architecture: source
Version: 1.0.0-1
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: 902308
Changes:
 why3 (1.0.0-1) unstable; urgency=medium
 .
   * New upstream version
     - drop patch getopt_long-return-value which has been applied upstream
   * Upstream does no longer build coq-tactic:
     - drop these from why3-coq.install
     - drop mention of these from the long description of why3-coq
   * libwhy3-ocaml-dep: add dependency ${shlibs:Depends}
   * As-installed-tests:
     - adapt the why3 files in d/tests/why to the new syntax of WhyML
     - mark tests with cvc3 and cvc4 as flaky  (closes: #902308)
     - test why3+cvc4: specify 'CVC4 1.5' in the invocation of why3,
       constrain the dependency of the test on cvc4 accordingly.
   * NEWS.Debian: new syntax of WhyML, new location of standard lib
Checksums-Sha1:
 f0bc0b697e247ce76de2dc1c65aa4f7fd0317f7a 2613 why3_1.0.0-1.dsc
 795256c2e5560b5f57953d5df7cc56898f1ddd64 5209657 why3_1.0.0.orig.tar.gz
 62b7202123cc29ae68e1090cd2261559eabd8367 13100 why3_1.0.0-1.debian.tar.xz
 1441c4a9a3a50fbb2d34d84e2236e8521dc1b1d4 12389 why3_1.0.0-1_source.buildinfo
Checksums-Sha256:
 a503ff21d45fac02025959ff8d4a64b4c4592cc3bfc93d999a73e3080384a148 2613 why3_1.0.0-1.dsc
 b65f4c1661ac8a6240778e6fa553c46098a26d029b02e5cf0e05b0c0630300a2 5209657 why3_1.0.0.orig.tar.gz
 891d6af8212be008fbf3afb891bb1dff343378777d31f9249af1914b7cda805c 13100 why3_1.0.0-1.debian.tar.xz
 528e8e9f57d4f6285d6393e34add582f24768d9e54528579e770c72331673333 12389 why3_1.0.0-1_source.buildinfo
Files:
 b6dc69b1594ea6de50fcd1016de24dbb 2613 math optional why3_1.0.0-1.dsc
 3477ce6b826bbba1562117239f0e9f81 5209657 math optional why3_1.0.0.orig.tar.gz
 12f2de99e06d1465f6fea63b8d933baa 13100 math optional why3_1.0.0-1.debian.tar.xz
 7a23dbe5e6374de611a93605b72716d9 12389 math optional why3_1.0.0-1_source.buildinfo

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

iQIzBAEBCAAdFiEEAgVIKeEtDyqOZI5idFxHZtTKzf8FAlsz95EACgkQdFxHZtTK
zf/7ew//SXycKW+D7WEm7Tm5Od6dR1R/EXHSS8VlMOc76RnJYQtxErqHvpToDiT3
Z304kgO4iD705UGxO+rzP6m/h03sz7aK8At49eUnVoLq4iVO9qMRLZJwhVHTIzMZ
e9zIy6FDWzlAdNBY6l9VNJZmlV1gwLAtemtPIovqpTPkpd/S+3FfpIRFhXd42UGv
ymhYn42FAX6Oan2v4vaM7GJALlQJ82B5z0R//oU3xS+tw42mC676yKw5tJvm/00W
bn+9Bi8+bU++iKINcriDPOMpetbbJfhIGzZXUDSHOisj7mExeu7CpWS6/FBB9lri
9GL2dStxbtjzXpkMEh3u3/r2phJagHhqrTcjIGfSpxnrt2wweVC3FNPO/KO1IX/c
JTAFIMLoXIAwhSv/menbQuhv8wobcDPJgQW08cQNdE5HeTKXfaZqjG63gYI565wN
904LSIMX5fnYpAYvmTmv/r/+Nfi2Uavw1KHz2vaqCk6ISviLzRFot2FpDaIjSD1r
mGcE6vfo3unjpJ8n++CcSpGdT2dghUq7ViYTHyaGYQiC02vMo0oMb3ulc2RjEciN
b7MhnXkh2NfLdcJhELs43U+36Xb24TfaKNS7e/c15yf9XQh9uJxdvog+TdnJ1mYf
Pd/MH3ozDqAUe0Us08Ok1mXcHEs38TSO/Ixr3zFUqYrTjLYZtjY=
=11C4
-----END PGP SIGNATURE-----

--- End Message ---
Reply to: