Bug#906001: marked as done (why3: needs porting to cvc4 version 1.6 )
Your message dated Mon, 05 Nov 2018 20:59:57 +0000
with message-id <E1gJlyX-00092v-Nb@fasolo.debian.org>
and subject line Bug#906001: fixed in why3 1.1.0-1
has caused the Debian Bug report #906001,
regarding why3: needs porting to cvc4 version 1.6
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.)
--
906001: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=906001
Debian Bug Tracking System
Contact owner@bugs.debian.org with problems
--- Begin Message ---
- To: submit@bugs.debian.org
- Subject: why3: needs porting to cvc4 version 1.6
- From: Ralf Treinen <treinen@irif.fr>
- Date: Mon, 13 Aug 2018 00:51:15 +0200
- Message-id: <20180812225115.GD3891@seneca.home.org>
Package: why3
Version: 1.0.0-1
Forwarded: https://gitlab.inria.fr/why3/why3/issues/164
why3 does not yet support version 1.6 of cvc4:
$ why3 config --detect-provers
[..]
warning: Prover CVC4 version 1.6 is not known to be supported.
$ why3 prove -P 'CVC4' minimum.mlw
minimum.mlw Minimum VC minimum: HighFailure (0.00s)
Prover exit status: exited with status 1
Prover output:
(error "Parse Error: /tmp/why_e2c49a_minimum-T-VC_minimum.smt2:8.24: Too many datatypes defined in this block.
(declare-datatypes () ((tuple0 (Tuple0))))
^
")
-Ralf.
--- End Message ---
--- Begin Message ---
Source: why3
Source-Version: 1.1.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 906001@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: Mon, 05 Nov 2018 19:23:56 +0100
Source: why3
Binary: why3 why3-coq libwhy3-ocaml-dev why3-examples why3-doc-html why3-doc-pdf
Architecture: source
Version: 1.1.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: 906001
Changes:
why3 (1.1.0-1) unstable; urgency=medium
.
* New upstream version. Works with cvc4 version 1.6 (closes: #906001)
* Since lablgtk2 does no longer build liblablgtksourceview2-ocaml-dev:
- drop build-dependencies liblablgtk2-ocaml-dev and
liblablgtksourceview2-ocaml-dev
- d/rules: configure with --disable-ide
- note in NEWS that the IDE is dropped.
- drop mention of IDE from why3.1 manpage.
* Dependencies on provers : enforce version >= 2.0.0. for alt-ergo since
upstream has dropped support for older versions. Add an
"skip-not-installable" on the test why3+alt-ergo
* Test why3+cvc4: fix selection of solver cvc4
* d/copyright: update full text of CC license.
* d/rules: remove empty why3shapes.gz files
* Standards-Version 4.2.1 (no change)
Checksums-Sha1:
bc4b811cfa50266a506866a1deaab44c83fc7e5a 2557 why3_1.1.0-1.dsc
8efa3ce01cbad5433d143c1612462d3d81948528 5554169 why3_1.1.0.orig.tar.gz
58b58ae8431ec4d4e6dc75a20acaaff89e4d181a 15968 why3_1.1.0-1.debian.tar.xz
7e772e521890a0a9f5def93345791cbdc3954ef3 12511 why3_1.1.0-1_source.buildinfo
Checksums-Sha256:
8d1f9fd82ceb00bafbc402b14bd0a3f1f3c2fa1fa147faca5d571a295d537c4e 2557 why3_1.1.0-1.dsc
817dde9d68eeef60717a137adfe6b909f82726cac286d68627228f5d118e3fa5 5554169 why3_1.1.0.orig.tar.gz
d1202e17bde890aa23bc169d4f9569475d5fc084d08a286a690153843e331a3f 15968 why3_1.1.0-1.debian.tar.xz
268bea859b26c62ffdbee96e111e7477fd9d98afd8f1b57b3693e210f1f7f194 12511 why3_1.1.0-1_source.buildinfo
Files:
b8ded49f34e6d6c070381c3938a3e16e 2557 math optional why3_1.1.0-1.dsc
650c8d3202d343983d8a0ba3d89bb825 5554169 math optional why3_1.1.0.orig.tar.gz
832b8c2c1362705461a84d39439f742c 15968 math optional why3_1.1.0-1.debian.tar.xz
e3a1a0c2624ec3a05652fc7aa4a42158 12511 math optional why3_1.1.0-1_source.buildinfo
-----BEGIN PGP SIGNATURE-----
iQIzBAEBCAAdFiEEAgVIKeEtDyqOZI5idFxHZtTKzf8FAlvgqQsACgkQdFxHZtTK
zf8exhAAse1VmpzDfrmWid1Lq0MblSKDRmdRoK/IAPQWs34UxKCVqxMoDQ428EOJ
5ni+nnbRLW3Zhf9jutRAZ/Jdg+8h58BHRDwuRwat4XH4NnY+ck2zXaT+6ufcQqCP
Wjxcw8lkr0Xj6OWfP5LP2xHSohuubxuHXdvHLshJRr6l3LPe3CTZKz6W07z3oiav
8E6BpDYZcxWdGwn7KHMO1JUPVkwQCDWNY5GDb2RMnR0EuwwRg3ICvLomWQzdovbk
8GYhIh9kShSIYpe3YF60MsojmnbxFRvJy2fpz9GJZewy5A5r1JpMucMDfSpLk0G2
8Cbg0/JpV1zdDltLBXcrbM/daK29tjWLjRdWQgAR30Mcuy8ptYOZ9FsOSyidxzoB
zvd1QtvlOKOFikGu+XQXnY7YPsC2pPGJkaeCXG8VSeuu4FmivhYE2MyZK7BktQmH
u9TqijeRo952RH7XM/H8755bbh9pKSCkftpVJbLUsWLUXoYD41wq6uKYU62Tuyt7
8NGEkO+xF05xohqyHExYj8nK8ij3Mdu+nL6VupNn0AhRej0aMnrna7Op/Y1E8PnW
Kyqc7bu7CGme9/yumoay1Z/9IuVGjkwDrqycqyk3O6h7qk32zlaTjJVv9m8zKFl8
V4A8oXmWBXUw9+7GcW/7BGFHl28wXDc7ob0P29SIkNxwjGh52wo=
=sZEM
-----END PGP SIGNATURE-----
--- End Message ---
Reply to: